chore: bump toolchain to v4.29.0-rc1 (#1682)

Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Parth Shastri <31370288+cppio@users.noreply.github.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Sebastian Graf <sgraf1337@gmail.com>
Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
Co-authored-by: Eric Wieser <efw@google.com>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>

Author: 24 people

Batteries/Classes/SatisfiesM.lean

@@ -193,8 +193,8 @@ theorem SatisfiesM_ReaderT_eq [Monad m] :
   (exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm
 
 theorem SatisfiesM_StateRefT_eq [Monad m] :
-    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by
-  simp [SatisfiesM_ReaderT_eq, ReaderT.run]
+    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) :=
+  SatisfiesM_ReaderT_eq
 
 theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
     SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x.run s) := by

Batteries/Control/AlternativeMonad.lean

@@ -197,9 +197,9 @@ instance [AlternativeMonad m] : AlternativeMonad (StateRefT' ω σ m) where
 
 instance [AlternativeMonad m] [LawfulAlternative m] :
     LawfulAlternative (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulAlternative (ReaderT _ _))
+  inferInstanceAs (LawfulAlternative (ReaderT (ST.Ref ω σ) m))
 
 instance [AlternativeMonad m] : LawfulAlternativeLift m (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulAlternativeLift m (ReaderT _ _))
+  inferInstanceAs (LawfulAlternativeLift m (ReaderT (ST.Ref ω σ) m))
 
 end StateRefT'

Batteries/Control/LawfulMonadState.lean

@@ -222,4 +222,4 @@ instance {m σ ρ} [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadSta
 
 instance {m ω σ} [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] :
     LawfulMonadStateOf σ (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulMonadStateOf σ (ReaderT _ _))
+  inferInstanceAs (LawfulMonadStateOf σ (ReaderT (ST.Ref ω σ) m))

Batteries/Data/Array/Basic.lean

@@ -27,100 +27,110 @@ arrays, remove duplicates and then compare them elementwise.
 def equalSet [BEq α] (xs ys : Array α) : Bool :=
   xs.all (ys.contains ·) && ys.all (xs.contains ·)
 
-set_option linter.unusedVariables.funArgs false in
 /--
 Returns the first minimal element among `d` and elements of the array.
-If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+If `start` and `stop` are given, only the subarray `xs[start...stop]` is
 considered (in addition to `d`).
 -/
 @[inline]
-protected def minWith [ord : Ord α]
+protected def rangeMinWith [ord : Ord α]
     (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
   xs.foldl (init := d) (start := start) (stop := stop) fun min x =>
     if compare x min |>.isLT then x else min
 
-set_option linter.unusedVariables.funArgs false in
+@[inherit_doc Array.rangeMinWith, deprecated Array.rangeMinWith (since := "2026-01-08")]
+protected def minWith := @Array.rangeMinWith
+
 /--
 Find the first minimal element of an array. If the array is empty, `d` is
-returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
 considered.
 -/
 @[inline]
-protected def minD [ord : Ord α]
+protected def rangeMinD [ord : Ord α]
     (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
   if h: start < xs.size ∧ start < stop then
-    xs.minWith xs[start] (start + 1) stop
+    xs.rangeMinWith xs[start] (start + 1) stop
   else
     d
 
-set_option linter.unusedVariables.funArgs false in
+@[inherit_doc Array.rangeMinD, deprecated Array.rangeMinD (since := "2026-01-08")]
+protected def minD := @Array.rangeMinD
+
 /--
 Find the first minimal element of an array. If the array is empty, `none` is
-returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
 considered.
 -/
 @[inline]
-protected def min? [ord : Ord α]
+protected def rangeMin? [ord : Ord α]
     (xs : Array α) (start := 0) (stop := xs.size) : Option α :=
   if h : start < xs.size ∧ start < stop then
-    some $ xs.minD xs[start] start stop
+    some $ xs.rangeMinD xs[start] start stop
   else
     none
 
-set_option linter.unusedVariables.funArgs false in
 /--
 Find the first minimal element of an array. If the array is empty, `default` is
-returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
 considered.
 -/
 @[inline]
-protected def minI [ord : Ord α] [Inhabited α]
+protected def rangeMinI [ord : Ord α] [Inhabited α]
     (xs : Array α) (start := 0) (stop := xs.size) : α :=
-  xs.minD default start stop
+  xs.rangeMinD default start stop
+
+@[inherit_doc Array.rangeMinI, deprecated Array.rangeMinI (since := "2026-01-08")]
+protected def minI := @Array.rangeMinI
 
-set_option linter.unusedVariables.funArgs false in
 /--
 Returns the first maximal element among `d` and elements of the array.
-If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+If `start` and `stop` are given, only the subarray `xs[start...stop]` is
 considered (in addition to `d`).
 -/
 @[inline]
-protected def maxWith [ord : Ord α]
+protected def rangeMaxWith [ord : Ord α]
     (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
-  xs.minWith (ord := ord.opposite) d start stop
+  xs.rangeMinWith (ord := ord.opposite) d start stop
+
+@[inherit_doc Array.rangeMaxWith, deprecated Array.rangeMaxWith (since := "2026-01-08")]
+protected def maxWith := @Array.rangeMaxWith
 
-set_option linter.unusedVariables.funArgs false in
 /--
 Find the first maximal element of an array. If the array is empty, `d` is
-returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
 considered.
 -/
 @[inline]
-protected def maxD [ord : Ord α]
+protected def rangeMaxD [ord : Ord α]
     (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
-  xs.minD (ord := ord.opposite) d start stop
+  xs.rangeMinD (ord := ord.opposite) d start stop
+
+@[inherit_doc Array.rangeMaxD, deprecated Array.rangeMaxD (since := "2026-01-08")]
+protected def maxD := @Array.rangeMaxD
 
-set_option linter.unusedVariables.funArgs false in
 /--
 Find the first maximal element of an array. If the array is empty, `none` is
-returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
 considered.
 -/
 @[inline]
-protected def max? [ord : Ord α]
+protected def rangeMax? [ord : Ord α]
     (xs : Array α) (start := 0) (stop := xs.size) : Option α :=
-  xs.min? (ord := ord.opposite) start stop
+  xs.rangeMin? (ord := ord.opposite) start stop
 
-set_option linter.unusedVariables.funArgs false in
 /--
 Find the first maximal element of an array. If the array is empty, `default` is
-returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
 considered.
 -/
 @[inline]
-protected def maxI [ord : Ord α] [Inhabited α]
+protected def rangeMaxI [ord : Ord α] [Inhabited α]
     (xs : Array α) (start := 0) (stop := xs.size) : α :=
-  xs.minI (ord := ord.opposite) start stop
+  xs.rangeMinI (ord := ord.opposite) start stop
+
+@[inherit_doc Array.rangeMaxI, deprecated Array.rangeMaxI (since := "2026-01-08")]
+protected def maxI := @Array.rangeMaxI
 
 @[deprecated set (since := "2026-02-02")]
 alias setN := set

Batteries/Data/Array/Scan.lean

@@ -19,6 +19,7 @@ Prove basic results about `Array.scanl`, `Array.scanr`, `Array.scanlM` and `Arra
 -/
 namespace Array
 
+set_option backward.isDefEq.respectTransparency false in
 theorem scanlM.loop_toList [Monad m] [LawfulMonad m]
     {f : β → α → m β} {stop : Nat} (h : stop ≤ as.size) :
     Array.toList <$> scanlM.loop f init as start stop h acc =

Batteries/Data/ByteArray.lean

@@ -27,9 +27,6 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
 
 /-! ### push -/
 
-@[simp] theorem size_push (a : ByteArray) (b : UInt8) : (a.push b).size = a.size + 1 :=
-  Array.size_push ..
-
 @[simp] theorem get_push_eq (a : ByteArray) (x : UInt8) : (a.push x)[a.size] = x :=
   Array.getElem_push_eq ..
 
@@ -81,7 +78,7 @@ theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start s
 
 @[simp] theorem get_extract {a : ByteArray} {start stop} (h : i < (a.extract start stop).size) :
     (a.extract start stop)[i] = a[start+i]'(get_extract_aux h) := by
-  simp [getElem_eq_data_getElem]
+  simp [getElem_eq_data_getElem]; rfl
 
 /-! ### ofFn -/
 

Batteries/Data/Fin/Fold.lean

@@ -20,6 +20,8 @@ theorem dfoldrM_loop_zero [Monad m] (f : (i : Fin n) → α i.succ → m (α i.c
 theorem dfoldrM_loop_succ [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x) :
     dfoldrM.loop n α f (i+1) h x = f ⟨i, by omega⟩ x >>= dfoldrM.loop n α f i (by omega) := rfl
 
+-- TODO: This proof needs adjustment for lean4#12179 (backward.isDefEq.respectTransparency)
+set_option backward.isDefEq.respectTransparency false in
 theorem dfoldrM_loop [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc))
     (x) : dfoldrM.loop (n+1) α f (i+1) h x =
       dfoldrM.loop n (α ∘ succ) (f ·.succ) i (by omega) x >>= f 0 := by
@@ -77,7 +79,7 @@ theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α
 
 theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) :
     dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by
-  rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq]
+  rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _)]; rfl
 
 @[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x) :
     dfoldlM 0 α f x = pure x := by simp [dfoldlM, dfoldlM.loop]
@@ -93,7 +95,7 @@ theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α
     cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
     rw [dfoldlM_loop_lt _ h]
     congr; funext
-    rw [dfoldlM_loop_eq, dfoldlM_loop_eq]
+    rw [dfoldlM_loop_eq, dfoldlM_loop_eq]; rfl
 
 theorem dfoldlM_succ [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x) :
     dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) :=

Batteries/Data/List/Lemmas.lean

@@ -1373,11 +1373,6 @@ theorem sum_singleton [Add α] [Zero α] [Std.LawfulRightIdentity (α := α) (·
 theorem sum_pair [Add α] [Zero α] [Std.LawfulRightIdentity (α := α) (· + ·) 0] {a b : α} :
   [a, b].sum = a + b := by simp [Std.LawfulRightIdentity.right_id]
 
-@[simp, grind =]
-theorem sum_append [Add α] [Zero α] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
-    [Std.Associative (α := α) (· + ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
-  induction l₁ with simp [Std.LawfulLeftIdentity.left_id, Std.Associative.assoc, *]
-
 theorem sum_concat [Add α] [Zero α] [Std.LawfulIdentity (α := α) (· + ·) 0]
     [Std.Associative (α := α) (· + ·)] {l : List α} {a : α} :
     (l.concat a).sum = l.sum + a := by simp [Std.LawfulRightIdentity.right_id]
@@ -1388,9 +1383,6 @@ theorem sum_flatten [Add α] [Zero α] [Std.LawfulIdentity (α := α) (· + ·)
     l.flatten.sum = (l.map sum).sum := by
   induction l with simp [*]
 
-theorem sum_eq_foldr [Add α] [Zero α] {l : List α} :
-    l.sum = l.foldr (· + ·) 0 := rfl
-
 theorem sum_eq_foldl [Add α] [Zero α] [Std.Associative (α := α) (· + ·)]
     [Std.LawfulIdentity (α := α) (· + ·) 0] {l : List α} :
     l.sum = l.foldl (· + ·) 0 := foldr_eq_foldl ..
@@ -1401,5 +1393,4 @@ theorem take_succ_drop {l : List α} {n stop : Nat}
   rw [← List.take_append_getElem (by simpa [← List.length_drop] using h)]
   simp [List.getElem_drop]
 
-@[simp]
-theorem reverse_singleton {a : α} : [a].reverse = [a] := rfl
+attribute [simp] reverse_singleton

Batteries/Data/String/Lemmas.lean

@@ -182,9 +182,6 @@ end Pos.Raw
 theorem endPos_eq_zero (s : String) : rawEndPos s = 0 ↔ s = "" :=
   rawEndPos_eq_zero_iff
 
-theorem isEmpty_iff (s : String) : isEmpty s ↔ s = "" := by
-  simp [isEmpty]
-
 /--
 Induction along the valid positions in a list of characters.
 (This definition is intended only for specification purposes.)

Batteries/Data/Vector/Lemmas.lean

@@ -100,7 +100,7 @@ theorem get_tail (v : Vector α (n + 1)) (i : Fin n) :
 
 @[simp]
 theorem finIdxOf?_empty [BEq α] (v : Vector α 0) : v.finIdxOf? a = none := by
-  simp [v.eq_empty]
+  simp [v.eq_empty]; rfl
 
 @[simp]
 theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {v : Vector α n} {a : α} :