chore: add/remove set_option backward after moving to v4.29.0-rc3 (leanprover-community#35952)

This PR adds and removes a number of `set_option backward.isDefEq.respectTransparency` that were missed in other cleanups, but are needed/possible after `master` has moved to `v4.29.0-rc3`.

Author: kim-em

Archive/Imo/Imo2001Q5.lean

@@ -178,7 +178,6 @@ lemma key_x_equation :
 
 /-! ### Solving the trigonometric equation -/
 
-set_option backward.isDefEq.respectTransparency false in
 lemma x_eq : s.x = 2 * π / 9 := by
   have work := s.key_x_equation
   rw [Real.sin_add_sin, show 2 * π / 3 - s.x = π - 2 * ((s.x + π / 3) / 2) by ring, Real.sin_pi_sub,

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/Imo2024Q6.lean

@@ -225,6 +225,7 @@ lemma floor_fExample (x : ℚ) :
     rw [Int.floor_eq_iff]
     simp [(Int.fract_nonneg x).lt_of_ne' h, (Int.fract_lt_one x).le]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma card_range_fExample : #(Set.range (fun x ↦ fExample x + fExample (-x))) = 2 := by
   have h : Set.range (fun x ↦ fExample x + fExample (-x)) = {0, -2} := by
     ext x

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -129,7 +129,6 @@ lemma volume_needleSpace : ℙ (needleSpace d) = ENNReal.ofReal (d * π) := by
     ENNReal.ofReal_mul hd.le]
   ring_nf
 
-set_option backward.isDefEq.respectTransparency false in
 lemma measurable_needleCrossesIndicator : Measurable (needleCrossesIndicator l) := by
   unfold needleCrossesIndicator
   refine Measurable.indicator measurable_const (IsClosed.measurableSet (IsClosed.and ?_ ?_)) <;>
@@ -289,7 +288,6 @@ lemma integral_min_eq_two_mul :
       (by ring : -(π / 2) + π = π / 2), two_mul]
   all_goals exact intervalIntegrable_min_const_sin_mul d l _ _
 
-set_option backward.isDefEq.respectTransparency false in
 include hd hl in
 /--
 The first of two adjacent integrals in the long case. In the range `0..(d / l).arcsin`, we

Counterexamples/HeawoodUnitDistance.lean

@@ -126,7 +126,6 @@ lemma injOn_udMap_sextet : Set.InjOn udMap ({0, 7, 10, 5, 2, 9} : Finset (Fin 14
   simp [Fin.forall_fin_succ, f, udMap]
   grind
 
-set_option backward.isDefEq.respectTransparency false in
 /-- `udMap` is injective and thus can be used in a unit-distance embedding. -/
 theorem injective_udMap : udMap.Injective := by
   let s : Finset (Fin 14) := {1, 0, 7, 10, 5, 2, 9}

Counterexamples/InvertibleModuleNotIdeal.lean

@@ -36,7 +36,6 @@ set_option backward.isDefEq.respectTransparency false in
 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`

Counterexamples/NowhereDifferentiable.lean

@@ -247,7 +247,6 @@ theorem weierstrass_slope {a : ℝ} (ha : a ∈ Set.Ioo 0 1) {b : ℕ} (hb : Odd
   rw [sub_mul (2 / 3), mul_sub |seq b x m - x|]
   exact sub_le_sub (weierstrass_remainder ha.1 hb hsum_shift) (weierstrass_partial ha.1 hab x m)
 
-set_option backward.isDefEq.respectTransparency false in
 theorem not_differentiableAt_weierstrass
     {a : ℝ} (ha : a ∈ Set.Ioo 0 1) {b : ℕ} (hb : Odd b) (hab : 3 / 2 * π + 1 < a * b) (x : ℝ) :
     ¬ DifferentiableAt ℝ (weierstrass a b) x := by

Mathlib/Algebra/BigOperators/Expect.lean

@@ -121,7 +121,10 @@ lemma expect_univ [Fintype ι] : 𝔼 i, f i = (∑ i, f i) /ℚ Fintype.card ι
   rw [expect, card_univ]
 
 @[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]
 
 @[congr]
@@ -166,6 +169,7 @@ 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
@@ -251,13 +255,15 @@ 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`. -/
@@ -340,6 +346,7 @@ 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/Category/AlgCat/Limits.lean

@@ -68,7 +68,6 @@ instance limitAlgebra :
   inferInstanceAs <| Algebra R (Shrink (sectionsSubalgebra F))
 
 #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
 /-- `limit.π (F ⋙ forget (AlgCat R)) j` as an `AlgHom`. -/
 def limitπAlgHom (j) :
@@ -155,7 +154,6 @@ instance hasLimits : HasLimits (AlgCat.{w} R) :=
   AlgCat.hasLimitsOfSize.{w, w, u}
 
 #adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
-set_option backward.whnf.reducibleClassField false in
 /-- The forgetful functor from R-algebras to rings preserves all limits.
 -/
 instance forget₂Ring_preservesLimitsOfSize [UnivLE.{v, w}] :

Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean

@@ -151,7 +151,6 @@ def invariants : Action (TopModuleCat R) G ⥤ TopModuleCat R where
 instance : (invariants R G).Linear R where
 instance : (invariants R G).Additive where
 
-set_option backward.isDefEq.respectTransparency false in
 /-- `homogeneousCochains R G` is the functor taking
 an `R`-linear `G`-representation to the complex of homogeneous cochains. -/
 def homogeneousCochains : Action (TopModuleCat R) G ⥤ CochainComplex (TopModuleCat R) ℕ :=
@@ -201,7 +200,6 @@ def kerHomogeneousCochainsZeroEquiv
     (continuous_induced_rng.mpr ((ContinuousLinearMap.const R G).cont.comp continuous_subtype_val))
 
 #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 ShortComplex HomologyData in
 /-- `H⁰_cont(G, X) ≅ Xᴳ`. -/