Update lean-toolchain for leanprover/lean4#10763

Author: leanprover-community-mathlib4-bot

Batteries/CodeAction/Misc.lean

@@ -299,7 +299,7 @@ def casesExpand : TacticCodeAction := fun _ snap ctx _ node => do
       let targets := discrInfos.map (·.expr)
       match using_ with
       | none =>
-        if Tactic.tactic.customEliminators.get (← getOptions) then
+        if tactic.customEliminators.get (← getOptions) then
           if let some elimName ← getCustomEliminator? targets induction then
             return some (← getElimExprNames (← getConstInfo elimName).type)
         matchConstInduct (← whnf (← inferType discr₀.expr)).getAppFn
@@ -341,7 +341,7 @@ def casesExpand : TacticCodeAction := fun _ snap ctx _ node => do
         (doc.meta.text.utf8PosToLspPos stx'.getTailPos?.get!, "")
       else (endPos, " with")
       let fallback := if let some ⟨startPos, endPos⟩ := fallback then
-        doc.meta.text.source.extract startPos endPos
+        String.Pos.Raw.extract doc.meta.text.source startPos endPos
       else
         "sorry"
       let newText := Id.run do

Batteries/Data/Array/Match.lean

@@ -126,7 +126,8 @@ private def modifyStep [BEq α] (m : Matcher α) [Iterator σ n α]
 instance [Monad n] [BEq α] (m : Matcher α) [Iterator σ n α] :
     Iterator (m.Iterator σ n α) n σ where
   IsPlausibleStep it step := ∃ step', m.modifyStep it step' = step
-  step it := it.internalState.inner.step >>= fun step => pure ⟨m.modifyStep _ _, step, rfl⟩
+  step it := it.internalState.inner.step >>=
+    fun step => pure (.deflate ⟨m.modifyStep _ _, step.inflate, rfl⟩)
 
 private def finitenessRelation [Monad n] [BEq α] (m : Matcher α) [Iterator σ n α] [Finite σ n] :
     FinitenessRelation (m.Iterator σ n α) n where

Batteries/Data/ByteArray.lean

@@ -36,9 +36,6 @@ theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
 
 /-! ### set -/
 
-@[simp] theorem data_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
-    (a.set i v).data = a.data.set i v i.isLt := rfl
-
 @[simp] theorem size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
     (a.set i v).size = a.size :=
   Array.size_set ..

Batteries/Data/String/Basic.lean

@@ -26,11 +26,11 @@ def toAsciiByteArray (s : String) : ByteArray :=
   `loop p out = out ++ toAsciiByteArray ({ s with startPos := p } : Substring)`
   -/
   loop (p : Pos.Raw) (out : ByteArray) : ByteArray :=
-    if h : s.atEnd p then out else
-    let c := s.get p
-    have : utf8ByteSize s - (next s p).byteIdx < utf8ByteSize s - p.byteIdx :=
+    if h : p.atEnd s then out else
+    let c := p.get s
+    have : utf8ByteSize s - (Pos.Raw.next s p).byteIdx < utf8ByteSize s - p.byteIdx :=
       Nat.sub_lt_sub_left (Nat.lt_of_not_le <| mt decide_eq_true h)
         (Nat.lt_add_of_pos_right (Char.utf8Size_pos _))
-    loop (s.next p) (out.push c.toUInt8)
+    loop (p.next s) (out.push c.toUInt8)
     termination_by utf8ByteSize s - p.byteIdx
   loop 0 ByteArray.empty

Batteries/Data/String/Lemmas.lean

@@ -68,7 +68,7 @@ def toStringFull (f : Float) : String :=
       else
         let rem := Nat.repr ((2^e + v' % 2^e) * 5^e)
         let rem := rem.dropRightWhile (· == '0')
-        s!"{intPart}.{rem.extract ⟨1⟩ rem.endPos}"
+        s!"{intPart}.{String.Pos.Raw.extract rem ⟨1⟩ rem.endPos}"
     if v < 0 then s!"-{s}" else s
   else f.toString -- inf, -inf, nan
 

Batteries/Lean/Float.lean

@@ -3,7 +3,7 @@ import Batteries.Tactic.Lemma
 -- lemma disabled by default
 /--
 info: Try this:
-  theorem
+  [apply] theorem
 ---
 error: `lemma` is not supported by default, please use `theorem` instead.
 Use `set_option lang.lemmaCmd true` to enable the use of the `lemma` command in a file.
@@ -19,7 +19,7 @@ lemma test2 : 3 < 7 := by decide
 -- lemma disabled again
 /--
 info: Try this:
-  theorem
+  [apply] theorem
 ---
 error: `lemma` is not supported by default, please use `theorem` instead.
 Use `set_option lang.lemmaCmd true` to enable the use of the `lemma` command in a file.

BatteriesTest/lemma_cmd.lean

@@ -6,7 +6,7 @@ Authors: Kim Morrison
 
 /--
 info: Try this:
-  exact (n, 37)
+  [apply] exact (n, 37)
 -/
 #guard_msgs in example (n : Nat) : Nat × Nat := by
   show_term
@@ -16,15 +16,15 @@ info: Try this:
 
 /--
 info: Try this:
-  refine (?_, ?_)
+  [apply] refine (?_, ?_)
 -/
 #guard_msgs in example : Nat × Nat := by
   show_term constructor
   repeat exact 42
 
 /--
 info: Try this:
-  fun {X} => X
+  [apply] fun {X} => X
 -/
 #guard_msgs in example : {_a : Nat} → Nat :=
   show_term by

BatteriesTest/show_term.lean

@@ -7,13 +7,13 @@ set_option linter.missingDocs false
 
 /--
 info: Try this:
-  simp only [Nat.add_comm]
+  [apply] simp only [Nat.add_comm]
 -/
 #guard_msgs in
 example : x + 1 = 1 + x := by simp? [Nat.add_comm, Nat.mul_comm]
 /--
 info: Try this:
-  dsimp only [Nat.reduceAdd]
+  [apply] dsimp only [Nat.reduceAdd]
 -/
 #guard_msgs in
 example : 1 + 1 = 2 := by dsimp?
@@ -27,10 +27,10 @@ example : 1 + 1 = 2 := by dsimp?
 
 /--
 info: Try this:
-  simp only [foo, bar]
+  [apply] simp only [foo, bar]
 ---
 info: Try this:
-  simp only [foo, baz]
+  [apply] simp only [foo, baz]
 -/
 #guard_msgs in
 example : foo x y = 1 + y := by
@@ -40,7 +40,7 @@ example : foo x y = 1 + y := by
 
 /--
 info: Try this:
-  simp only [foo, bar, baz]
+  [apply] simp only [foo, bar, baz]
 -/
 #guard_msgs in
 example : foo x y = 1 + y := by

BatteriesTest/simp_trace.lean

@@ -96,14 +96,14 @@ example (P : Bool) (h : ¬ ¬ P) : P := by
 
 /--
 info: Try this:
-  simpa only using h
+  [apply] simpa only using h
 -/
 #guard_msgs in
 example (p : Prop) (h : p) : p := by simpa? using h
 
 /--
 info: Try this:
-  simpa only [and_true] using h
+  [apply] simpa only [and_true] using h
 -/
 #guard_msgs in
 example (p : Prop) (h : p ∧ True) : p := by simpa? using h