chore: bump toolchain to v4.29.0-rc7 (#37034)

This brings the new `inferInstanceAs` implementation.

Author: kim-em

Archive/Imo/Imo1982Q1.lean

@@ -70,6 +70,7 @@ lemma f₃ : f 3 = 1 := by
 
 lemma superadditive {m n : ℕ+} : f m + f n ≤ f (m + n) := by have h := hf.rel m n; grind
 
+set_option backward.isDefEq.respectTransparency false in
 lemma superhomogeneous {m n : ℕ+} : ↑n * f m ≤ f (n * m) := by
   induction n with
   | one => simp
@@ -83,6 +84,7 @@ lemma superhomogeneous {m n : ℕ+} : ↑n * f m ≤ f (n * m) := by
 lemma superlinear {a b c d : ℕ+} : a * f b + c * f d ≤ f (a * b + c * d) :=
   (add_le_add hf.superhomogeneous hf.superhomogeneous).trans hf.superadditive
 
+set_option backward.isDefEq.respectTransparency false in
 lemma le_mul_three_apply (n : ℕ+) : n ≤ f (3 * n) := by
   rw [← mul_one (n : ℕ), ← hf.f₃, mul_comm 3]
   exact hf.superhomogeneous

Counterexamples/SorgenfreyLine.lean

@@ -87,7 +87,6 @@ theorem nhds_basis_Ico_rat (a : ℝₗ) :
   rcases exists_rat_btwn hb with ⟨r, har, hrb⟩
   exact ⟨r, har, Ico_subset_Ico_right hrb.le⟩
 
-set_option backward.isDefEq.respectTransparency false in
 theorem nhds_basis_Ico_inv_pnat (a : ℝₗ) :
     (𝓝 a).HasBasis (fun _ : ℕ+ => True) fun n => Ico a (a + (n : ℝₗ)⁻¹) := by
   refine (nhds_basis_Ico a).to_hasBasis (fun b hb => ?_) fun n hn =>
@@ -101,7 +100,6 @@ theorem nhds_countable_basis_Ico_inv_pnat (a : ℝₗ) :
     (𝓝 a).HasCountableBasis (fun _ : ℕ+ => True) fun n => Ico a (a + (n : ℝₗ)⁻¹) :=
   ⟨nhds_basis_Ico_inv_pnat a, Set.to_countable _⟩
 
-set_option backward.isDefEq.respectTransparency false in
 theorem nhds_antitone_basis_Ico_inv_pnat (a : ℝₗ) :
     (𝓝 a).HasAntitoneBasis fun n : ℕ+ => Ico a (a + (n : ℝₗ)⁻¹) :=
   ⟨nhds_basis_Ico_inv_pnat a, monotone_const.Ico <| Antitone.const_add
@@ -214,7 +212,6 @@ theorem cardinal_antidiagonal (c : ℝₗ) : #{x : ℝₗ × ℝₗ | x.1 + x.2
     fun x ↦ ⟨(toReal.symm x, c - toReal.symm x), by simp⟩,
     fun ⟨x, hx⟩ ↦ by ext <;> simp [← hx.out], fun x ↦ rfl⟩
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Any subset of an antidiagonal `{(x, y) : ℝₗ × ℝₗ| x + y = c}` is a closed set. -/
 theorem isClosed_of_subset_antidiagonal {s : Set (ℝₗ × ℝₗ)} {c : ℝₗ} (hs : ∀ x ∈ s, x.1 + x.2 = c) :
     IsClosed s := by

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -335,7 +335,7 @@ instance _root_.AlgEquiv.subsingleton_right [Subsingleton (Subalgebra R B)] :
   ⟨fun f g => by rw [← f.symm_symm, Subsingleton.elim f.symm g.symm, g.symm_symm]⟩
 
 instance : Unique (Subalgebra R R) :=
-  { inferInstanceAs (Inhabited (Subalgebra R R)) with
+  { (inferInstance : Inhabited (Subalgebra R R)) with
     uniq := by
       intro S
       refine le_antisymm ?_ bot_le

Mathlib/Algebra/Algebra/ZMod.lean

@@ -55,7 +55,7 @@ def algebraOfModule (n : ℕ) (R : Type*) [Ring R] [Module (ZMod n) R] : Algebra
   Algebra.ofModule' (proof · · |>.1) (proof · · |>.2) where
   proof (r : ZMod n) (x : R) : r • 1 * x = r • x ∧ x * r • 1 = r • x := by
     obtain _ | n := n
-    · obtain rfl : (inferInstanceAs (Module ℤ R)) = ‹_› := Subsingleton.elim _ _
+    · obtain rfl : ((inferInstance : Module ℤ R)) = ‹_› := Subsingleton.elim _ _
       simp [ZMod, Int.cast_comm]
     · obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r
       simp [Nat.cast_smul_eq_nsmul, Nat.cast_comm]

Mathlib/Algebra/BigOperators/Expect.lean

@@ -122,7 +122,6 @@ lemma expect_univ [Fintype ι] : 𝔼 i, f i = (∑ i, f i) /ℚ Fintype.card ι
 
 @[simp] lemma expect_empty (f : ι → M) : 𝔼 i ∈ ∅, f i = 0 := by simp [expect]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] lemma expect_singleton (f : ι → M) (i : ι) : 𝔼 j ∈ {i}, f j = f i := by simp [expect]
 
 @[simp] lemma expect_const_zero (s : Finset ι) : 𝔼 _i ∈ s, (0 : M) = 0 := by simp [expect]
@@ -169,7 +168,6 @@ lemma expect_ite_zero (s : Finset ι) (p : ι → Prop) [DecidablePred p]
 section DecidableEq
 variable [DecidableEq ι]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma expect_ite_mem (s t : Finset ι) (f : ι → M) :
     𝔼 i ∈ s, (if i ∈ t then f i else 0) = (#(s ∩ t) / #s : ℚ≥0) • 𝔼 i ∈ s ∩ t, f i := by
   obtain hst | hst := (s ∩ t).eq_empty_or_nonempty
@@ -255,15 +253,13 @@ most arguments. -/
 lemma expect_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
     𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by simp_rw [expect, card_equiv e hst, sum_equiv e hst hfg]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Expectation over a product set equals the expectation of the fiberwise expectations.
 
 For rewriting in the reverse direction, use `Finset.expect_product'`. -/
 lemma expect_product (s : Finset ι) (t : Finset κ) (f : ι × κ → M) :
     𝔼 x ∈ s ×ˢ t, f x = 𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j) := by
   simp only [expect, card_product, sum_product, smul_sum, mul_inv, mul_smul, Nat.cast_mul]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Expectation over a product set equals the expectation of the fiberwise expectations.
 
 For rewriting in the reverse direction, use `Finset.expect_product`. -/
@@ -346,7 +342,6 @@ end Semiring
 section CommSemiring
 variable [CommSemiring M] [Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma expect_pow (s : Finset ι) (f : ι → M) (n : ℕ) :
     (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun _ : Fin n ↦ s, ∏ i, f (p i) := by
   classical

Mathlib/Algebra/BigOperators/Field.lean

@@ -31,26 +31,22 @@ lemma Finset.sum_div (s : Finset ι) (f : ι → K) (a : K) :
 namespace Finset
 variable {α β : Type*} [Fintype β]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma dens_disjiUnion (s : Finset α) (t : α → Finset β) (h) :
     (s.disjiUnion t h).dens = ∑ a ∈ s, (t a).dens := by
   simp [dens, sum_div]
 
 variable {s : Finset α} {t : α → Finset β}
 
-set_option backward.isDefEq.respectTransparency false in
 lemma dens_biUnion [DecidableEq β] (h : (s : Set α).PairwiseDisjoint t) :
     (s.biUnion t).dens = ∑ u ∈ s, (t u).dens := by
   simp [dens, card_biUnion h, sum_div]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma dens_biUnion_le [DecidableEq β] : (s.biUnion t).dens ≤ ∑ a ∈ s, (t a).dens := by
   simp only [dens, ← sum_div]
   gcongr
   exact mod_cast card_biUnion_le
 
-set_option backward.isDefEq.respectTransparency false in
 lemma dens_eq_sum_dens_fiberwise [DecidableEq α] {f : β → α} {t : Finset β}
     (h : (t : Set β).MapsTo f s) : t.dens = ∑ a ∈ s, {b ∈ t | f b = a}.dens := by
   simp [dens, ← sum_div, card_eq_sum_card_fiberwise h]

Mathlib/Algebra/Category/AlgCat/Limits.lean

@@ -153,7 +153,6 @@ lemma hasLimitsOfSize [UnivLE.{v, w}] : HasLimitsOfSize.{t, v} (AlgCat.{w} R) :=
 instance hasLimits : HasLimits (AlgCat.{w} R) :=
   AlgCat.hasLimitsOfSize.{w, w, u}
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 /-- The forgetful functor from R-algebras to rings preserves all limits.
 -/
 instance forget₂Ring_preservesLimitsOfSize [UnivLE.{v, w}] :

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -196,15 +196,15 @@ variable (K : Type u) [Field K]
 
 set_option backward.isDefEq.respectTransparency false in
 instance (V W : FGModuleCat.{v} K) : Module.Finite K (V.obj ⟶ W.obj) :=
-  (inferInstanceAs <| Module.Finite K (V →ₗ[K] W)).equiv ModuleCat.homLinearEquiv.symm
+  ((inferInstance : Module.Finite K (V →ₗ[K] W))).equiv ModuleCat.homLinearEquiv.symm
 
 instance (V W : FGModuleCat.{v} K) : Module.Finite K (V ⟶ W) :=
-  (inferInstanceAs (Module.Finite K (V.obj ⟶ W.obj))).equiv
+  ((inferInstance : Module.Finite K (V.obj ⟶ W.obj))).equiv
     InducedCategory.homLinearEquiv.symm
 
 instance : (ModuleCat.isFG K).IsMonoidalClosed where
   prop_ihom {X Y} (_ : Module.Finite _ _) (_ : Module.Finite _ _) :=
-    (inferInstanceAs <| Module.Finite K (X →ₗ[K] Y)).equiv ModuleCat.homLinearEquiv.symm
+    ((inferInstance : Module.Finite K (X →ₗ[K] Y))).equiv ModuleCat.homLinearEquiv.symm
 
 variable (V W : FGModuleCat K)
 

Mathlib/Algebra/Category/Grp/Limits.lean

@@ -74,6 +74,7 @@ noncomputable instance limitGroup :
 instance : Small.{u} (Functor.sections ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat)) :=
   inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget GrpCat))
 
+set_option backward.inferInstanceAs.wrap false in
 /-- We show that the forgetful functor `GrpCat ⥤ MonCat` creates limits.
 
 All we need to do is notice that the limit point has a `Group` instance available, and then reuse

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -470,6 +470,7 @@ scalar multiplication defined by `s • l := x ↦ l (x • s)` -/
 def obj' : ModuleCat S :=
   of _ ((restrictScalars f).obj (of _ S) →ₗ[R] M)
 
+set_option backward.inferInstanceAs.wrap.data false in
 instance : CoeFun (obj' f M) fun _ => S → M :=
   inferInstanceAs <| CoeFun ((restrictScalars f).obj (of _ S) →ₗ[R] M) _
 
@@ -500,6 +501,7 @@ namespace CoextendScalars
 
 variable {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S)
 
+set_option backward.inferInstanceAs.wrap.data false in
 instance (M : ModuleCat R) : CoeFun ((coextendScalars f).obj M) fun _ => S → M :=
   inferInstanceAs <| CoeFun (CoextendScalars.obj' f M) _
 
@@ -1040,7 +1042,6 @@ lemma extendScalars_id_comp :
   erw [extendScalarsId_hom_app_one_tmul]
   rfl
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid a strange error. -/
 @[reassoc]
 lemma extendScalars_comp_id :
     (extendScalarsComp f₁₂ (RingHom.id R₂)).hom ≫ Functor.whiskerLeft _ (extendScalarsId R₂).hom ≫