chore: remove unnecessary set_option lines (leanprover-community#37326)

I removed 458 unnecessary `set_option` line(s) across 165 file(s).

Author: mathlib-nolints[bot]

Archive/Examples/Eisenstein.lean

@@ -25,7 +25,6 @@ namespace Polynomial
 
 open Ideal.Quotient Ideal RingHom
 
-set_option backward.isDefEq.respectTransparency false in
 set_option linter.flexible false in
 example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X]) := by
   -- We will apply the generalized Eisenstein criterion with `q = X ^ 2 + 1` and `K = ZMod 3`.

Counterexamples/DimensionPolynomial.lean

@@ -34,7 +34,6 @@ variable (k : Type*) [Field k]
 noncomputable abbrev A : Subring (RatFunc k)⟦X⟧ :=
   (RatFunc.C (K := k)).range.comap PowerSeries.constantCoeff
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ringKrullDim_A_eq_one : ringKrullDim (A k) = 1 := by
   have h_unit : ∀ (x : (RatFunc k)⟦X⟧) (hx : x ∈ A k), IsUnit x → IsUnit (⟨x, hx⟩ : A k) := by
     intro x ⟨z, hz⟩ ⟨y, hxy⟩
@@ -69,7 +68,6 @@ theorem ringKrullDim_A_eq_one : ringKrullDim (A k) = 1 := by
   · exact ⟨0, by simp [hy_const]⟩
   · simp only [Subring.coe_mul, SubmonoidClass.coe_pow, pow_succ, ← ha, mul_assoc, mul_comm x.val _]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ringKrullDim_polynomial_A_eq_three : ringKrullDim (A k)[X] = 3 := by
   apply le_antisymm (by simpa [ringKrullDim_A_eq_one k] using Polynomial.ringKrullDim_le (R := A k))
   let φ : (A k) →+* k := by

Counterexamples/InvertibleModuleNotIdeal.lean

@@ -19,7 +19,6 @@ variable (R : Type*) [CommRing R]
 R ⊕ ⨁ₘ R⧸m where m ranges over maximal ideals of R. -/
 abbrev SqZeroExtQuotMax := TrivSqZeroExt R (Π₀ m : MaximalSpectrum R, R ⧸ m.1)
 
-set_option backward.isDefEq.respectTransparency false in
 instance : IsFractionRing (SqZeroExtQuotMax R) (SqZeroExtQuotMax R) :=
   IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mpr fun x hx ↦
     TrivSqZeroExt.isUnit_iff_isUnit_fst.mpr <| of_not_not fun hr ↦ by
@@ -31,12 +30,10 @@ instance : IsFractionRing (SqZeroExtQuotMax R) (SqZeroExtQuotMax R) :=
         using (Ideal.Quotient.mk_eq_mk_iff_sub_mem ..).mpr (by simpa)
     simpa using congr(($this).snd)
 
-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.isDefEq.respectTransparency false in
 open CommRing (Pic) in
 /-- If the Picard group of a commutative ring R is nontrivial, then `SqZeroExtQuotMax R`
 has an invertible module (which is the base change of an invertible ideal of R)

Mathlib/Algebra/Algebra/Epi.lean

@@ -76,7 +76,6 @@ section Ring
 
 variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isEpi_iff_surjective_algebraMap_of_finite [Module.Finite R A] :
     Algebra.IsEpi R A ↔ Surjective (algebraMap R A) := by
   refine ⟨fun h ↦ ?_, isEpi_of_surjective_algebraMap R A⟩

Mathlib/Algebra/Category/Grp/Kernels.lean

@@ -41,7 +41,6 @@ def cokernelCocone : CokernelCofork f :=
   CokernelCofork.ofπ (Z := of <| H ⧸ f.hom.range) (ofHom (mk' f.hom.range)) <| ext fun x =>
     (eq_zero_iff _).mpr ⟨x, rfl⟩
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The projection onto the quotient is a cokernel in the categorical sense. -/
 def cokernelIsColimit : IsColimit <| cokernelCocone f :=
   Cofork.IsColimit.mk _

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -33,7 +33,6 @@ variable {M N P : ModuleCat.{v} R} (f : M ⟶ N)
 def kernelCone : KernelFork f :=
   KernelFork.ofι (ofHom (LinearMap.ker f.hom).subtype) <| by aesop
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The kernel of a linear map is a kernel in the categorical sense. -/
 def kernelIsLimit : IsLimit (kernelCone f) :=
   Fork.IsLimit.mk _
@@ -72,7 +71,6 @@ def cokernelIsColimit : IsColimit (cokernelCocone f) :=
     apply (cancel_epi (ofHom (LinearMap.range f.hom).mkQ)).1
     exact h
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Construct an `IsColimit` structure of cokernels given `Function.Exact`. -/
 noncomputable
 def isColimitCokernelCofork (f : M ⟶ N) (g : N ⟶ P) (H : Function.Exact f.hom g.hom)

Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean

@@ -32,7 +32,6 @@ variable {R' : Type u'} [CommRing R'] [Small.{v'} R'] (e : R ≃+* R')
 
 variable {M : ModuleCat.{v} R} {N : ModuleCat.{v'} R'}
 
-set_option backward.isDefEq.respectTransparency false in
 attribute [local instance] RingHomInvPair.of_ringEquiv in
 lemma hasProjectiveDimensionLE_of_semiLinearEquiv (e' : M ≃ₛₗ[RingHomClass.toRingHom e] N)
     (n : ℕ) [HasProjectiveDimensionLE M n] : HasProjectiveDimensionLE N n := by

Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean

@@ -46,7 +46,6 @@ instance : Mono (kerι φ) := ConcreteCategory.mono_of_injective (kerι φ) <| S
 
 @[simp] lemma kerι_apply (x) : kerι φ x = x.1 := rfl
 
-set_option backward.isDefEq.respectTransparency false in
 /-- `TopModuleCat.ker` is indeed the kernel in `TopModuleCat R`. -/
 def isLimitKer : IsLimit (KernelFork.ofι (kerι φ) (kerι_comp φ)) :=
   isLimitAux (KernelFork.ofι (kerι φ) (kerι_comp φ))

Mathlib/Algebra/CharP/MixedCharZero.lean

@@ -158,7 +158,6 @@ Note: Property `(2)` is denoted as `EqualCharZero` in the statement names below.
 
 namespace EqualCharZero
 
-set_option backward.isDefEq.respectTransparency false in
 /-- `ℚ`-algebra implies equal characteristic. -/
 private lemma of_algebraRat [Algebra ℚ R] : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I) := by
   intro I hI
@@ -178,7 +177,6 @@ section ConstructionAlgebraRat
 
 variable {R}
 
-set_option backward.isDefEq.respectTransparency false in
 private lemma PNat.isUnit_natCast [h : Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))]
     (n : ℕ+) : IsUnit (n : R) := by
   -- `n : R` is a unit iff `(n)` is not a proper ideal in `R`.

Mathlib/Algebra/CharP/Quotient.lean

@@ -64,12 +64,10 @@ theorem quotient_iff_le_ker_natCast (n : ℕ) [CharP R n] (I : Ideal R) :
 
 end CharP
 
-set_option backward.isDefEq.respectTransparency false in
 lemma Ideal.natCast_mem_of_charP_quotient (p : ℕ) (I : Ideal R) [CharP (R ⧸ I) p] :
     (p : R) ∈ I :=
   Ideal.Quotient.eq_zero_iff_mem.mp <| by simp
 
-set_option backward.isDefEq.respectTransparency false in
 theorem Ideal.Quotient.index_eq_zero (I : Ideal R) : (↑I.toAddSubgroup.index : R ⧸ I) = 0 := by
   rw [AddSubgroup.index, Nat.card_eq]
   split_ifs with hq; swap