chore: bump toolchain to v4.29.0-rc3 (#35942)

Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>

Author: 3 people

Archive/Imo/Imo2001Q4.lean

@@ -35,7 +35,6 @@ variable {n : ℕ} {c : Fin n → ℤ}
 rather than `Icc 1 n`, and as such contains `+ 1` to compensate. -/
 def S (c : Fin n → ℤ) (a : Perm (Fin n)) : ℤ := ∑ i, c i * (a i + 1)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Assuming the opposite of what is to be proved, the sum of `S` over all permutations is
 congruent to the sum of all residues modulo `n!`, i.e. `n! * (n! - 1) / 2`. -/
 lemma sum_range_modEq_sum_of_contra (hS : ¬∃ a b, a ≠ b ∧ (n ! : ℤ) ∣ S c a - S c b) :

Archive/Imo/Imo2019Q4.lean

@@ -34,6 +34,7 @@ open Finset
 
 namespace Imo2019Q4
 
+set_option backward.isDefEq.respectTransparency false in
 theorem upper_bound {k n : ℕ} (hk : k > 0)
     (h : (k ! : ℤ) = ∏ i ∈ range n, ((2 : ℤ) ^ n - (2 : ℤ) ^ i)) : n < 6 := by
   have h2 : ∑ i ∈ range n, i < k := by

Archive/Imo/Imo2024Q2.lean

@@ -27,7 +27,6 @@ open scoped Nat
 def Condition (a b : ℕ) : Prop :=
   0 < a ∧ 0 < b ∧ ∃ g N : ℕ, 0 < g ∧ 0 < N ∧ ∀ n : ℕ, N ≤ n → Nat.gcd (a ^ n + b) (b ^ n + a) = g
 
-set_option backward.isDefEq.respectTransparency false in
 lemma dvd_pow_iff_of_dvd_sub {a b d n : ℕ} {z : ℤ} (ha : a.Coprime d)
     (hd : (φ d : ℤ) ∣ (n : ℤ) - z) :
     d ∣ a ^ n + b ↔ (((ZMod.unitOfCoprime _ ha) ^ z : (ZMod d)ˣ) : ZMod d) + b = 0 := by

Archive/Kuratowski.lean

@@ -98,7 +98,6 @@ theorem mem_theFourteen_iff_isObtainable {s t : Set X} :
       exact IsObtainable.base
   mpr := (·.mem_theFourteen)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- **Kuratowski's closure-complement theorem**: the number of obtainable sets via closure and
 complement operations from a single set `s` is at most 14. -/
 theorem ncard_isObtainable_le_fourteen (s : Set X) : {t | IsObtainable s t}.ncard ≤ 14 := by

Counterexamples/InvertibleModuleNotIdeal.lean

@@ -35,6 +35,8 @@ set_option backward.isDefEq.respectTransparency false in
 /-- R as an algebra over `SqZeroExtQuotMax R`. -/
 abbrev SqZeroExtQuotMax.algebraBase : Algebra (SqZeroExtQuotMax R) R := TrivSqZeroExt.algebraBase ..
 
+#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
+set_option backward.whnf.reducibleClassField false in
 set_option backward.isDefEq.respectTransparency false in
 open CommRing (Pic) in
 /-- If the Picard group of a commutative ring R is nontrivial, then `SqZeroExtQuotMax R`

Mathlib/Algebra/AffineMonoid/Irreducible.lean

@@ -63,7 +63,6 @@ end CommMonoid
 section CancelCommMonoid
 variable [CancelCommMonoid M] [Subsingleton Mˣ]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- A finitely generated cancellative monoid with a single unit is generated by its (finitely many)
 irreducible elements. -/
 @[to_additive (attr := simp)

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -507,7 +507,6 @@ theorem adjoin_iUnion {α : Type*} (s : α → Set A) :
     adjoin R (Set.iUnion s) = ⨆ i : α, adjoin R (s i) :=
   (@Algebra.gc R A _ _ _).l_iSup
 
-set_option backward.isDefEq.respectTransparency false in
 theorem adjoin_attach_biUnion [DecidableEq A] {α : Type*} {s : Finset α} (f : s → Finset A) :
     adjoin R (s.attach.biUnion f : Set A) = ⨆ x, adjoin R (f x) := by simp [adjoin_iUnion]
 

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -486,7 +486,6 @@ theorem prod_extend_by_one [DecidableEq ι] (s : Finset ι) (f : ι → M) :
     ∏ i ∈ s, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i :=
   (prod_congr rfl) fun _i hi => if_pos hi
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Also see `Finset.prod_ite_mem_eq` -/
 @[to_additive /-- Also see `Finset.sum_ite_mem_eq` -/]
 theorem prod_eq_prod_extend (f : s → M) : ∏ x, f x = ∏ x ∈ s, Subtype.val.extend f 1 x := by

Mathlib/Algebra/BigOperators/Group/Finset/Indicator.lean

@@ -21,7 +21,6 @@ variable {ι κ α β : Type*} [CommMonoid β]
 
 open Set
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Consider a product of `g i (f i)` over a finset.  Suppose `g` is a function such as
 `n ↦ (· ^ n)`, which maps a second argument of `1` to `1`. Then if `f` is replaced by the
 corresponding multiplicative indicator function, the finset may be replaced by a possibly larger

Mathlib/Algebra/BigOperators/Group/Finset/Piecewise.lean

@@ -64,7 +64,6 @@ theorem prod_ite {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f g : ι 
     ∏ x ∈ s, (if p x then f x else g x) = (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, g x := by
   simp [prod_apply_ite _ _ fun x => x]
 
-set_option backward.isDefEq.respectTransparency false in
 @[to_additive]
 lemma prod_dite_of_false {p : ι → Prop} [DecidablePred p] (h : ∀ i ∈ s, ¬ p i)
     (f : ∀ i, p i → M) (g : ∀ i, ¬ p i → M) :
@@ -104,7 +103,6 @@ theorem prod_ite_mem [DecidableEq ι] (s t : Finset ι) (f : ι → M) :
     ∏ i ∈ s, (if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i := by
   rw [← Finset.prod_filter, Finset.filter_mem_eq_inter]
 
-set_option backward.isDefEq.respectTransparency false in
 @[to_additive]
 lemma prod_attach_eq_prod_dite [Fintype ι] (s : Finset ι) (f : s → M) [DecidablePred (· ∈ s)] :
     ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1 := by