chore: adaptations for nightly-2026-02-21

Archive/Imo/Imo2010Q5.lean

@@ -86,7 +86,7 @@ lemma push {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 5) :
     · simp_rw [single_eq_of_ne hk, tsub_zero]
       rcases eq_or_ne k (i + 1) with rfl | hk'
       · simp_rw [single_eq_same, single_succ]; grind
-      · simp_rw [single_eq_of_ne hk']
+      · simp_rw [single_eq_of_ne hk', add_zero]
 termination_by B i
 
 /-- `(0, 0, 5, 11, 0, 0)` is reachable. -/
@@ -118,13 +118,14 @@ lemma double {B : Fin 6 → ℕ} {i : Fin 6}
   ext k; simp only [comp_apply, add_apply, sub_apply]
   have (j : Fin 6) : j + 1 + 1 = j + 2 := by grind
   rcases eq_or_ne k i with rfl | hk
-  · rw [swap_apply_of_ne_of_ne (by simp) (by simp), single_succ, this, single_add_two]
+  · rw [swap_apply_of_ne_of_ne (by simp) (by simp), single_succ, this, single_add_two, Nat.sub_zero]
   · rcases eq_or_ne k (i + 1) with rfl | hk'
     · grind [swap_apply_left, single_eq_same]
     · rw [single_eq_of_ne hk']
       rcases eq_or_ne k (i + 2) with rfl | hk''
       · grind [swap_apply_right, single_eq_same, single_succ]
-      · rw [swap_apply_of_ne_of_ne hk' hk'', single_eq_of_ne hk', this, single_eq_of_ne hk'']
+      · rw [swap_apply_of_ne_of_ne hk' hk'', single_eq_of_ne hk', this, single_eq_of_ne hk'',
+          tsub_zero]
 
 set_option backward.isDefEq.respectTransparency false in
 /-- `double` as many times as possible, emptying $B_i$ and doubling $B_{i+1}$ that many times. -/
@@ -142,7 +143,7 @@ lemma doubles {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (z
     · simp_rw [update_of_ne hk', sub_apply, add_apply, single_eq_of_ne hk', add_zero]
       rcases eq_or_ne k i with rfl | hk
       · simp_rw [single_eq_same, tsub_self]
-      · simp_rw [single_eq_of_ne hk]
+      · simp_rw [single_eq_of_ne hk, tsub_zero]
 termination_by B i
 
 set_option backward.isDefEq.respectTransparency false in
@@ -161,7 +162,7 @@ lemma exp {B : Fin 6 → ℕ} {i : Fin 6}
   · simp only [update_of_ne hk', sub_apply, add_apply, single_eq_of_ne hk', add_zero]
     rcases eq_or_ne k i with rfl | hk
     · simp_rw [single_eq_same, tsub_self]
-    · simp_rw [single_eq_of_ne hk]
+    · simp_rw [single_eq_of_ne hk, tsub_zero]
 
 /-- From `(0, 0, k+1, n, 0, 0)` with `n > 0` we can reach `(0, 0, k, 2^n, 0, 0)`. -/
 lemma exp_mid {k n : ℕ} (h : Reachable (single 2 (k + 1) + single 3 n)) (hn : 0 < n) :

Archive/MiuLanguage/DecisionNec.lean

@@ -78,7 +78,7 @@ theorem count_equiv_one_or_two_mod3_of_derivable (en : Miustr) :
     apply mod3_eq_1_or_mod3_eq_2 h_ih; left
     rw [count_append, count_append, count_append]
     simp_rw [count_cons_self, count_nil, count_cons, beq_iff_eq, reduceCtorEq, ite_false,
-      add_right_comm, add_mod_right]
+      add_right_comm, add_mod_right, add_zero]
   | r4 _ h_ih =>
     apply mod3_eq_1_or_mod3_eq_2 h_ih; left
     rw [count_append, count_append, count_append]

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -78,7 +78,6 @@ theorem disc_eq_regionBetween :
 theorem measurableSet_disc : MeasurableSet (disc r) := by
   apply measurableSet_lt <;> fun_prop
 
-set_option backward.isDefEq.respectTransparency false in
 /-- **Area of a Circle**: The area of a disc with radius `r` is `π * r ^ 2`. -/
 theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by
   let f x := sqrt (r ^ 2 - x ^ 2)

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -181,7 +181,6 @@ lemma integrable_needleCrossesIndicator :
       neg_div, sub_neg_eq_add, add_halves, sub_zero, ← ENNReal.ofReal_mul hd.le,
       ENNReal.ofReal_lt_top]
 
-set_option backward.isDefEq.respectTransparency false in
 include hd hB hBₘ in
 /--
 This is a common step in both the short and the long case to simplify the expectation of the
@@ -328,7 +327,6 @@ lemma integral_arcsin_to_pi_div_two_min (h : d ≤ l) :
     simp_rw [min_eq_left ((div_le_iff₀ hl).mp ((Real.arcsin_le_iff_le_sin' hθ_mem).mp hθ₁))]
   rw [intervalIntegral.integral_congr this, intervalIntegral.integral_const, smul_eq_mul]
 
-set_option backward.isDefEq.respectTransparency false in
 set_option linter.style.whitespace false in
 include hd hBₘ hB hl in
 /-- Buffon's Needle, the long case (`d ≤ l`) -/

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -986,7 +986,6 @@ theorem coe_iSup_of_directed [Nonempty ι] {S : ι → NonUnitalSubalgebra R A}
     (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
   this.symm ▸ rfl
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Define an algebra homomorphism on a directed supremum of non-unital subalgebras by defining
 it on each non-unital subalgebra, and proving that it agrees on the intersection of
 non-unital subalgebras. -/

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -858,7 +858,6 @@ lemma algebraMap_apply {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra
     (S : Subalgebra R A) (x : S) : algebraMap S A x = x :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem rangeS_algebraMap {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
     (S : Subalgebra R A) : (algebraMap S A).rangeS = S.toSubsemiring := by

Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

@@ -40,7 +40,6 @@ theorem coe_iSup_of_directed (dir : Directed (· ≤ ·) K) : ↑(iSup K) = ⋃
 
 variable (K)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Define an algebra homomorphism on a directed supremum of subalgebras by defining
 it on each subalgebra, and proving that it agrees on the intersection of subalgebras. -/
 noncomputable def iSupLift (dir : Directed (· ≤ ·) K) (f : ∀ i, K i →ₐ[R] B)
@@ -101,7 +100,6 @@ theorem iSupLift_mk {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
   dsimp [iSupLift, inclusion]
   rw [Set.iUnionLift_mk]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem iSupLift_of_mem {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
     {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
     {T : Subalgebra R A} {hT : T ≤ iSup K} {i : ι} (x : T) (hx : (x : A) ∈ K i) :

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -152,11 +152,12 @@ theorem sum_Ico_reflect {δ : Type*} [AddCommMonoid δ] (f : ℕ → δ) (k : 
     (h : m ≤ n + 1) : (∑ j ∈ Ico k m, f (n - j)) = ∑ j ∈ Ico (n + 1 - m) (n + 1 - k), f j :=
   @prod_Ico_reflect (Multiplicative δ) _ f k m n h
 
+set_option backward.isDefEq.respectTransparency false in
 theorem prod_range_reflect (f : ℕ → M) (n : ℕ) :
     (∏ j ∈ range n, f (n - 1 - j)) = ∏ j ∈ range n, f j := by
   cases n
   · simp
-  · simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub]
+  · simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]
     rw [prod_Ico_reflect _ _ le_rfl]
     simp
 

Mathlib/Algebra/BigOperators/NatAntidiagonal.lean

@@ -31,7 +31,6 @@ theorem sum_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → N} :
     (∑ p ∈ antidiagonal (n + 1), f p) = f (0, n + 1) + ∑ p ∈ antidiagonal n, f (p.1 + 1, p.2) :=
   @prod_antidiagonal_succ (Multiplicative N) _ _ _
 
-set_option backward.isDefEq.respectTransparency false in
 @[to_additive]
 theorem prod_antidiagonal_swap {n : ℕ} {f : ℕ × ℕ → M} :
     ∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p := by

Mathlib/Algebra/Category/CommBialgCat.lean

@@ -200,7 +200,6 @@ instance {A : Type u} [CommRing A] [Bialgebra R A] [IsCocomm R A] :
     IsCommMonObj (Opposite.op <| CommAlgCat.of R A) where
   mul_comm := by ext; exact comm_comul R _
 
-set_option backward.isDefEq.respectTransparency false in
 instance {A B : Type u} [CommRing A] [Bialgebra R A] [CommRing B] [Bialgebra R B]
     (f : A →ₐc[R] B) : IsMonHom (CommAlgCat.ofHom (f : A →ₐ[R] B)).op where
 

Mathlib/Algebra/Category/Grp/FiniteGrp.lean

@@ -26,14 +26,14 @@ open CategoryTheory
 @[pp_with_univ]
 structure FiniteGrp where
   /-- A group that is finite -/
-  toGrp : GrpCat
+  toGrp : GrpCat.{u}
   [isFinite : Finite toGrp]
 
 /-- The category of finite additive groups. -/
 @[pp_with_univ]
 structure FiniteAddGrp where
   /-- An additive group that is finite -/
-  toAddGrp : AddGrpCat
+  toAddGrp : AddGrpCat.{u}
   [isFinite : Finite toAddGrp]
 
 attribute [to_additive] FiniteGrp

Mathlib/Algebra/Category/Grp/ZModuleEquivalence.lean

@@ -27,7 +27,6 @@ universe u
 
 namespace ModuleCat
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The forgetful functor from `ℤ` modules to `AddCommGrpCat` is full. -/
 instance forget₂_addCommGroup_full : (forget₂ (ModuleCat ℤ) AddCommGrpCat.{u}).Full where
   map_surjective {A B}

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -110,7 +110,6 @@ variable [CommRing R]
 
 namespace FreeMonoidal
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The canonical isomorphism `𝟙_ (ModuleCat R) ≅ (free R).obj (𝟙_ (Type u))`.
 (This should not be used directly: it is part of the implementation of the
 monoidal structure on the functor `free R`.) -/
@@ -129,7 +128,6 @@ def εIso : 𝟙_ (ModuleCat R) ≅ (free R).obj (𝟙_ (Type u)) where
 @[simp]
 lemma εIso_hom_one : (εIso R).hom 1 = freeMk PUnit.unit := rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma εIso_inv_freeMk (x : PUnit) : (εIso R).inv (freeMk x) = 1 := by
   dsimp [εIso, freeMk]

Mathlib/Algebra/Category/Ring/Adjunctions.lean

@@ -85,7 +85,6 @@ set_option backward.isDefEq.respectTransparency false in
 def coyonedaUnique {n : Type v} [Unique n] : coyoneda.obj (op n) ≅ 𝟭 CommRingCat.{max u v} :=
   NatIso.ofComponents (fun X ↦ (RingEquiv.piUnique _).toCommRingCatIso) (fun f ↦ by ext; simp)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The monoid algebra functor `CommGrpCat ⥤ R-Alg` given by `G ↦ R[G]`. -/
 @[simps]
 def monoidAlgebra (R : CommRingCat.{max u v}) : CommMonCat.{v} ⥤ Under R where

Mathlib/Algebra/CharP/Invertible.lean

@@ -62,7 +62,6 @@ def invertibleOfCoprime {n : ℕ} (h : n.Coprime p) :
   invOf_mul_self := by rw [CharP.natCast_gcdA_mul_intCast_eq_gcd, h, Nat.cast_one]
   mul_invOf_self := by rw [CharP.intCast_mul_natCast_gcdA_eq_gcd, h, Nat.cast_one]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem invOf_eq_of_coprime {n : ℕ} [Invertible (n : R)] (h : n.Coprime p) :
     ⅟(n : R) = n.gcdA p := by
   letI : Invertible (n : R) := invertibleOfCoprime h

Mathlib/Algebra/Group/Defs.lean

@@ -523,7 +523,7 @@ theorem npowRec'_two_mul {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
     match k' with
     | 0 => rfl
     | 1 => simp [npowRec']
-    | k + 2 => simp [npowRec', ← mul_assoc, Nat.mul_add, ← ih]
+    | k + 2 => simp [npowRec', ← mul_assoc, ← ih]
 
 @[to_additive]
 theorem npowRec'_mul_comm {M : Type*} [Semigroup M] [One M] {k : ℕ} (k0 : k ≠ 0) (m : M) :

Mathlib/Algebra/Group/NatPowAssoc.lean

@@ -76,7 +76,7 @@ theorem npow_mul_comm (m n : ℕ) (x : M) :
 
 theorem npow_mul (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ m) ^ n := by
   induction n with
-  | zero => rw [npow_zero, npow_zero]
+  | zero => rw [npow_zero, mul_zero, npow_zero]
   | succ n ih => rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
 
 theorem npow_mul' (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ n) ^ m := by

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -111,7 +111,6 @@ theorem subtype_comp_rangeRestrict (f : G →* N) : f.range.subtype.comp f.range
 theorem rangeRestrict_surjective (f : G →* N) : Function.Surjective f.rangeRestrict :=
   fun ⟨_, g, rfl⟩ => ⟨g, rfl⟩
 
-set_option backward.isDefEq.respectTransparency false in
 @[to_additive (attr := simp)]
 lemma rangeRestrict_injective_iff {f : G →* N} : Injective f.rangeRestrict ↔ Injective f := by
   convert Set.injective_codRestrict _

Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean

@@ -306,7 +306,6 @@ lemma comp_mk₀_id (α : Ext X Y n) :
     α.comp (mk₀ (𝟙 Y)) (add_zero n) = α := by
   letI := HasDerivedCategory.standard C; ext; simp
 
-set_option backward.isDefEq.respectTransparency false in
 variable (X Y) in
 @[simp]
 lemma mk₀_zero : mk₀ (0 : X ⟶ Y) = 0 := by

Mathlib/Algebra/Homology/Functor.lean

@@ -37,7 +37,6 @@ namespace HomologicalComplex
 
 variable [HasZeroMorphisms V] {ι : Type*} {c : ComplexShape ι}
 
-set_option backward.isDefEq.respectTransparency false in
 /-- A complex of functors gives a functor to complexes. -/
 @[simps]
 def asFunctor (C : HomologicalComplex (T ⥤ V) c) :

Mathlib/Algebra/Homology/Homotopy.lean

@@ -472,7 +472,6 @@ def mkInductiveAux₁ :
 
 section
 
-set_option backward.isDefEq.respectTransparency false in
 /-- An auxiliary construction for `mkInductive`.
 -/
 def mkInductiveAux₂ :
@@ -488,7 +487,6 @@ def mkInductiveAux₂ :
       ⟨0, zero ≫ (Q.xPrevIso rfl).inv, by simpa using comm_zero⟩ :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem mkInductiveAux₂_add_one (n) :
     mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1) =
       letI I := mkInductiveAux₁ e zero one comm_one succ n

Mathlib/Algebra/Lie/Engel.lean

@@ -182,7 +182,6 @@ theorem LieEquiv.isEngelian_iff (e : L ≃ₗ⁅R⁆ L₂) :
     LieAlgebra.IsEngelian.{u₁, u₂, u₄} R L ↔ LieAlgebra.IsEngelian.{u₁, u₃, u₄} R L₂ :=
   ⟨e.surjective.isEngelian, e.symm.surjective.isEngelian⟩
 
-set_option backward.isDefEq.respectTransparency false in
 theorem LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer {K : LieSubalgebra R L}
     (hK₁ : LieAlgebra.IsEngelian.{u₁, u₂, u₄} R K) (hK₂ : K < K.normalizer) :
     ∃ (K' : LieSubalgebra R L), LieAlgebra.IsEngelian.{u₁, u₂, u₄} R K' ∧ K < K' := by

Mathlib/Algebra/Lie/EngelSubalgebra.lean

@@ -99,7 +99,6 @@ lemma normalizer_engel (x : L) : normalizer (engel R x) = engel R x := by
 
 variable {R}
 
-set_option backward.isDefEq.respectTransparency false in
 open Filter in
 /-- A Lie-subalgebra of an Artinian Lie algebra is self-normalizing
 if it contains an Engel subalgebra.

Mathlib/Algebra/Lie/Quotient.lean

@@ -127,7 +127,6 @@ instance lieQuotientHasBracket : Bracket (L ⧸ I) (L ⧸ I) :=
 theorem mk_bracket (x y : L) : mk ⁅x, y⁆ = ⁅(mk x : L ⧸ I), (mk y : L ⧸ I)⁆ :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 instance lieQuotientLieRing : LieRing (L ⧸ I) where
   add_lie := by
     intro x' y' z'; refine Quotient.inductionOn₃' x' y' z' ?_; intro x y z
@@ -158,7 +157,6 @@ instance lieQuotientLieRing : LieRing (L ⧸ I) where
       | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
     apply congr_arg; apply leibniz_lie
 
-set_option backward.isDefEq.respectTransparency false in
 instance lieQuotientLieAlgebra : LieAlgebra R (L ⧸ I) where
   lie_smul := by
     intro t x' y'; refine Quotient.inductionOn₂' x' y' ?_; intro x y

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -235,7 +235,6 @@ instance lieRingModule : LieRingModule L' M where
 
 variable [Module R M]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Given a Lie algebra `L` containing a Lie subalgebra `L' ⊆ L`, together with a Lie module `M` of
 `L`, we may regard `M` as a Lie module of `L'` by restriction. -/
 instance lieModule [LieModule R L M] : LieModule R L' M where

Mathlib/Algebra/Lie/Submodule.lean

@@ -778,12 +778,10 @@ theorem mem_map_of_mem {m : M} (h : m ∈ N) : f m ∈ N.map f :=
 theorem mem_comap {m : M} : m ∈ comap f N' ↔ f m ∈ N' :=
   Iff.rfl
 
-set_option backward.isDefEq.respectTransparency false in
 theorem comap_incl_eq_top : N₂.comap N.incl = ⊤ ↔ N ≤ N₂ := by
   rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
     LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_toSubmodule]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem comap_incl_eq_bot : N₂.comap N.incl = ⊥ ↔ N ⊓ N₂ = ⊥ := by
   simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, bot_toSubmodule,
     inf_toSubmodule]
@@ -932,13 +930,11 @@ variable (N : LieSubmodule R L M)
 @[simp]
 theorem ker_incl : N.incl.ker = ⊥ := (LieModuleHom.ker_eq_bot N.incl).mpr <| injective_incl N
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem range_incl : N.incl.range = N := by
   simp only [← toSubmodule_inj, LieModuleHom.toSubmodule_range, incl_coe]
   rw [Submodule.range_subtype]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem comap_incl_self : comap N.incl N = ⊤ := by
   simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, top_toSubmodule]

Mathlib/Algebra/Lie/TraceForm.lean

@@ -323,7 +323,6 @@ lemma traceForm_eq_of_le_idealizer :
   rw [N.trace_eq_trace_restrict_of_le_idealizer I h x hy]
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 include h hy in
 /-- Note that this result is slightly stronger than it might look at first glance: we only assume
 that `N` is trivial over `I` rather than all of `L`. This means that it applies in the important

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -328,7 +328,6 @@ theorem exists_genWeightSpace_zero_le_ker_of_isNoetherian
     ∃ k : ℕ, genWeightSpace M (0 : L → R) ≤ LinearMap.ker (toEnd R L M x ^ k) := by
   simpa using exists_genWeightSpace_le_ker_of_isNoetherian M (0 : L → R) x
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isNilpotent_toEnd_sub_algebraMap [IsNoetherian R M] (χ : L → R) (x : L) :
     _root_.IsNilpotent <| toEnd R L (genWeightSpace M χ) x - algebraMap R _ (χ x) := by
   have : toEnd R L (genWeightSpace M χ) x - algebraMap R _ (χ x) =

Mathlib/Algebra/Lie/Weights/Cartan.lean

@@ -189,7 +189,6 @@ theorem le_zeroRootSubalgebra : H ≤ zeroRootSubalgebra R L H := by
     coe_zeroRootSubalgebra, LieSubmodule.toSubmodule_le_toSubmodule]
   exact toLieSubmodule_le_rootSpace_zero R L H
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem zeroRootSubalgebra_normalizer_eq_self :
     (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H := by
@@ -270,7 +269,6 @@ lemma mem_corootSpace {x : H} :
     {x | ∃ (a : rootSpace H α) (b : rootSpace H (-α)), ⁅(a : L), (b : L)⁆ = x} ↔ _
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 lemma mem_corootSpace' {x : H} :
     x ∈ corootSpace α ↔
     x ∈ Submodule.span R ({⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} : Set H) := by

Mathlib/Algebra/Lie/Weights/IsSimple.lean

@@ -177,7 +177,6 @@ private theorem chi_not_in_q_aux (h_chi_not_in_q : ↑χ ∉ q) :
 
 end
 
-set_option backward.isDefEq.respectTransparency false in
 include hq hx_χ hαq in
 private theorem invtSubmoduleToLieIdeal_aux (hm_α : m_α ∈ sl2SubmoduleOfRoot hα₀) :
     ⁅x_χ, m_α⁆ ∈ ⨆ α : {α : Weight K H L // ↑α ∈ q ∧ α.IsNonZero}, sl2SubmoduleOfRoot α.2.2 := by

Mathlib/Algebra/Lie/Weights/Killing.lean

@@ -570,7 +570,6 @@ lemma exists_isSl2Triple_of_weight_isNonZero {α : Weight K H L} (hα : α.IsNon
     rw [lie_smul, lie_smul, smul_lie, this]
     simp [← smul_assoc, f, hh, mul_comm _ (2 * (α h)⁻¹)]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma _root_.IsSl2Triple.h_eq_coroot {α : Weight K H L} (hα : α.IsNonZero)
     {h e f : L} (ht : IsSl2Triple h e f) (heα : e ∈ rootSpace H α) (hfα : f ∈ rootSpace H (-α)) :
     h = coroot α := by
@@ -626,7 +625,6 @@ noncomputable def sl2SubalgebraOfRoot {α : Weight K H L} (hα : α.IsNonZero) :
   choose h e f t ht using exists_isSl2Triple_of_weight_isNonZero hα
   exact t.toLieSubalgebra K
 
-set_option backward.isDefEq.respectTransparency false in
 lemma mem_sl2SubalgebraOfRoot_iff {α : Weight K H L} (hα : α.IsNonZero) {h e f : L}
     (t : IsSl2Triple h e f) (hte : e ∈ rootSpace H α) (htf : f ∈ rootSpace H (-α)) {x : L} :
     x ∈ sl2SubalgebraOfRoot hα ↔ ∃ c₁ c₂ c₃ : K, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ := by
@@ -679,7 +677,6 @@ This represents the image of the coroot space under the inclusion `H ↪ L`. -/
 noncomputable abbrev corootSubmodule (α : Weight K H L) : LieSubmodule K H L :=
   LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
 
-set_option backward.isDefEq.respectTransparency false in
 open Submodule in
 lemma sl2SubmoduleOfRoot_eq_sup (α : Weight K H L) (hα : α.IsNonZero) :
     sl2SubmoduleOfRoot hα = genWeightSpace L α ⊔ genWeightSpace L (-α) ⊔ corootSubmodule α := by

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -163,7 +163,6 @@ instance : Module.FinitePresentation R R := Module.finitePresentation_of_project
 instance : Module.FinitePresentation R (ι →₀ R) := Module.finitePresentation_of_projective _ _
 instance : Module.FinitePresentation R (ι → R) := Module.finitePresentation_of_projective _ _
 
-set_option backward.isDefEq.respectTransparency false in
 lemma Module.finitePresentation_of_surjective [h : Module.FinitePresentation R M] (l : M →ₗ[R] N)
     (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
     Module.FinitePresentation R N := by