[Merged by Bors] - chore: mark Submodule.toAddSubgroup @[reducible]

Archive/Imo/Imo2019Q4.lean

@@ -34,7 +34,6 @@ 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,7 +225,6 @@ 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

Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean

@@ -136,7 +136,6 @@ def complex : CochainComplex (Action (TopModuleCat R) G ⥤ Action (TopModuleCat
 
 end MultiInd
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The functor taking an `R`-linear `G`-representation to its `G`-invariant submodule. -/
 def invariants : Action (TopModuleCat R) G ⥤ TopModuleCat R where
   obj M := .of R

Mathlib/Algebra/Category/ModuleCat/Abelian.lean

@@ -52,7 +52,6 @@ def normalMono (hf : Mono f) : NormalMono f where
               (LinearMap.quotKerEquivRange f.hom ≪≫ₗ
               LinearEquiv.ofEq _ _ (Submodule.ker_mkQ _).symm))) <| by ext; rfl
 
-set_option backward.isDefEq.respectTransparency false in
 /-- In the category of modules, every epimorphism is normal. -/
 def normalEpi (hf : Epi f) : NormalEpi f where
   W := of R (LinearMap.ker f.hom)

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -252,7 +252,6 @@ namespace Free
 
 section
 
-set_option backward.whnf.reducibleClassField false in
 instance : Preadditive (Free R C) where
   homGroup _ _ := Finsupp.instAddCommGroup
   add_comp X Y Z f f' g := by
@@ -264,7 +263,6 @@ instance : Preadditive (Free R C) where
     congr; ext r h
     rw [Finsupp.sum_add_index'] <;> · simp [mul_add]
 
-set_option backward.whnf.reducibleClassField false in
 instance : Linear R (Free R C) where
   homModule _ _ := Finsupp.module _ R
   smul_comp X Y Z r f g := by
@@ -276,7 +274,6 @@ instance : Linear R (Free R C) where
     congr; ext h s
     rw [Finsupp.sum_smul_index] <;> simp [mul_left_comm]
 
-set_option backward.whnf.reducibleClassField false in
 set_option backward.isDefEq.respectTransparency false in
 theorem single_comp_single {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) :
     (single f r ≫ single g s : Free.of R X ⟶ Free.of R Z) = single (f ≫ g) (r * s) := by
@@ -303,7 +300,6 @@ variable {C} {D : Type u} [Category.{v} D] [Preadditive D] [Linear R D]
 
 open Preadditive Linear
 
-set_option backward.whnf.reducibleClassField false in
 set_option backward.isDefEq.respectTransparency false in
 /-- A functor to an `R`-linear category lifts to a functor from its `R`-linear completion.
 -/

Mathlib/Algebra/Category/ModuleCat/EpiMono.lean

@@ -28,7 +28,6 @@ namespace ModuleCat
 variable {R : Type u} [Ring R] {X Y : ModuleCat.{v} R} (f : X ⟶ Y)
 variable {M : Type v} [AddCommGroup M] [Module R M]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ker_eq_bot_of_mono [Mono f] : LinearMap.ker f.hom = ⊥ :=
   LinearMap.ker_eq_bot_of_cancel fun u v h => ModuleCat.hom_ext_iff.mp <|
     (@cancel_mono _ _ _ _ _ f _ (↟u) (↟v)).1 <| ModuleCat.hom_ext_iff.mpr h
@@ -55,7 +54,6 @@ theorem epi_iff_surjective : Epi f ↔ Function.Surjective f := by
 def uniqueOfEpiZero (X) [h : Epi (0 : X ⟶ of R M)] : Unique M :=
   uniqueOfSurjectiveZero X ((ModuleCat.epi_iff_surjective _).mp h)
 
-set_option backward.isDefEq.respectTransparency false in
 instance mono_as_hom'_subtype (U : Submodule R X) : Mono (ModuleCat.ofHom U.subtype) :=
   (mono_iff_ker_eq_bot _).mpr (Submodule.ker_subtype U)
 

Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean

@@ -26,7 +26,6 @@ namespace ModuleCat
 
 variable {R : Type u} [CommRing R]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The exterior power of an object in `ModuleCat R`. -/
 def exteriorPower (M : ModuleCat.{v} R) (n : ℕ) : ModuleCat.{max u v} R :=
   ModuleCat.of R (⋀[R]^n M)
@@ -76,7 +75,6 @@ lemma hom_ext {M : ModuleCat.{v} R} {N : ModuleCat.{max u v} R} {n : ℕ}
   ext : 1
   exact exteriorPower.linearMap_ext h
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The morphism `M.exteriorPower n ⟶ N` induced by an alternating map. -/
 noncomputable def desc {M : ModuleCat.{v} R} {n : ℕ} {N : ModuleCat.{max u v} R}
     (φ : M.AlternatingMap N n) : M.exteriorPower n ⟶ N :=
@@ -88,7 +86,6 @@ lemma desc_mk {M : ModuleCat.{v} R} {n : ℕ} {N : ModuleCat.{max u v} R}
     desc φ (mk x) = φ x := by
   apply exteriorPower.alternatingMapLinearEquiv_apply_ιMulti
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The morphism `M.exteriorPower n ⟶ N.exteriorPower n` induced by a morphism `M ⟶ N`
 in `ModuleCat R`. -/
 noncomputable def map {M N : ModuleCat.{v} R} (f : M ⟶ N) (n : ℕ) :

Mathlib/Algebra/Category/ModuleCat/Images.lean

@@ -33,21 +33,18 @@ attribute [local ext] Subtype.ext
 
 section
 
-set_option backward.isDefEq.respectTransparency false in
 -- implementation details of `HasImage` for ModuleCat; use the API, not these
 /-- The image of a morphism in `ModuleCat R` is just the bundling of `LinearMap.range f` -/
 def image : ModuleCat R :=
   ModuleCat.of R (LinearMap.range f.hom)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The inclusion of `image f` into the target -/
 def image.ι : image f ⟶ H :=
   ofHom (LinearMap.range f.hom).subtype
 
 instance : Mono (image.ι f) :=
   ConcreteCategory.mono_of_injective (image.ι f) Subtype.val_injective
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The corestriction map to the image -/
 def factorThruImage : G ⟶ image f :=
   ofHom f.hom.rangeRestrict
@@ -59,7 +56,6 @@ attribute [local simp] image.fac
 
 variable {f}
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The universal property for the image factorisation -/
 noncomputable def image.lift (F' : MonoFactorisation f) : image f ⟶ F'.I :=
   ofHom
@@ -99,19 +95,16 @@ noncomputable def isImage : IsImage (monoFactorisation f) where
   lift := image.lift
   lift_fac := image.lift_fac
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The categorical image of a morphism in `ModuleCat R` agrees with the linear algebraic range. -/
 noncomputable def imageIsoRange {G H : ModuleCat.{v} R} (f : G ⟶ H) :
     Limits.image f ≅ ModuleCat.of R (LinearMap.range f.hom) :=
   IsImage.isoExt (Image.isImage f) (isImage f)
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, reassoc, elementwise]
 theorem imageIsoRange_inv_image_ι {G H : ModuleCat.{v} R} (f : G ⟶ H) :
     (imageIsoRange f).inv ≫ Limits.image.ι f = ModuleCat.ofHom (LinearMap.range f.hom).subtype :=
   IsImage.isoExt_inv_m _ _
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, reassoc, elementwise]
 theorem imageIsoRange_hom_subtype {G H : ModuleCat.{v} R} (f : G ⟶ H) :
     (imageIsoRange f).hom ≫ ModuleCat.ofHom (LinearMap.range f.hom).subtype = Limits.image.ι f := by

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -29,7 +29,6 @@ section
 
 variable {M N P : ModuleCat.{v} R} (f : M ⟶ N)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The kernel cone induced by the concrete kernel. -/
 def kernelCone : KernelFork f :=
   KernelFork.ofι (ofHom (LinearMap.ker f.hom).subtype) <| by aesop
@@ -104,7 +103,6 @@ attribute [local instance] hasCokernels_moduleCat
 
 variable {G H : ModuleCat.{v} R} (f : G ⟶ H)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The categorical kernel of a morphism in `ModuleCat`
 agrees with the usual module-theoretical kernel.
 -/
@@ -113,15 +111,13 @@ noncomputable def kernelIsoKer {G H : ModuleCat.{v} R} (f : G ⟶ H) :
     kernel f ≅ ModuleCat.of R (LinearMap.ker f.hom) :=
   limit.isoLimitCone ⟨_, kernelIsLimit f⟩
 
-set_option backward.isDefEq.respectTransparency false in
 -- We now show this isomorphism commutes with the inclusion of the kernel into the source.
 @[simp, elementwise]
     -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation
 theorem kernelIsoKer_inv_kernel_ι : (kernelIsoKer f).inv ≫ kernel.ι f =
     ofHom (LinearMap.ker f.hom).subtype :=
   limit.isoLimitCone_inv_π _ _
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, elementwise]
 theorem kernelIsoKer_hom_ker_subtype :
     -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation

Mathlib/Algebra/Category/ModuleCat/Subobject.lean

@@ -35,7 +35,6 @@ namespace ModuleCat
 
 variable {R : Type u} [Ring R] (M : ModuleCat.{v} R)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The categorical subobjects of a module `M` are in one-to-one correspondence with its
 submodules. -/
 noncomputable def subobjectModule : Subobject M ≃o Submodule R M :=
@@ -81,7 +80,6 @@ noncomputable def toKernelSubobject {M N : ModuleCat.{v} R} {f : M ⟶ N} :
     LinearMap.ker f.hom →ₗ[R] kernelSubobject f :=
   (kernelSubobjectIso f ≪≫ ModuleCat.kernelIsoKer f).inv.hom
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem toKernelSubobject_arrow {M N : ModuleCat R} {f : M ⟶ N} (x : LinearMap.ker f.hom) :
     (kernelSubobject f).arrow (toKernelSubobject x) = x.1 := by

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

@@ -34,17 +34,14 @@ variable {M N : TopModuleCat.{v} R} (φ : M ⟶ N)
 
 section kernel
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Kernel in `TopModuleCat R` is the kernel of the linear map with the subspace topology. -/
 abbrev ker : TopModuleCat R := .of R φ.hom.ker
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The inclusion map from the kernel in `TopModuleCat R`. -/
 def kerι : ker φ ⟶ M := ofHom ⟨Submodule.subtype _, continuous_subtype_val⟩
 
 instance : Mono (kerι φ) := ConcreteCategory.mono_of_injective (kerι φ) <| Subtype.val_injective
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] lemma kerι_comp : kerι φ ≫ φ = 0 := by ext ⟨_, hm⟩; exact hm
 
 @[simp] lemma kerι_apply (x) : kerι φ x = x.1 := rfl

Mathlib/Algebra/DirectSum/LinearMap.lean

@@ -97,7 +97,6 @@ lemma trace_eq_zero_of_mapsTo_ne (h : IsInternal N) [IsNoetherian R M]
     diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne h b σ hσ hf (by simp [s]),
     Pi.zero_apply, Finset.sum_const_zero]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- If `f` and `g` are commuting endomorphisms of a finite, free `R`-module `M`, such that `f`
 is triangularizable, then to prove that the trace of `g ∘ f` vanishes, it is sufficient to prove
 that the trace of `g` vanishes on each generalized eigenspace of `f`. -/
@@ -138,7 +137,6 @@ lemma mapsTo_biSup_of_mapsTo {ι : Type*} {N : ι → Submodule R M}
 
 end IsInternal
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The trace of an endomorphism of a direct sum is the sum of the traces on each component.
 
 Note that it is important the statement gives the user definitional control over `p` since the

Mathlib/Algebra/DirectSum/Module.lean

@@ -496,7 +496,6 @@ theorem isInternal_ne_bot_iff {A : ι → Submodule R M} :
     IsInternal (fun i : {i // A i ≠ ⊥} ↦ A i) ↔ IsInternal A := by
   simp [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isInternal_biSup_submodule_of_iSupIndep {A : ι → Submodule R M} (s : Set ι)
     (h : iSupIndep <| fun i : s ↦ A i) :
     IsInternal <| fun (i : s) ↦ (A i).comap (⨆ i ∈ s, A i).subtype := by

Mathlib/Algebra/DualQuaternion.lean

@@ -96,7 +96,6 @@ theorem imK_snd_dualNumberEquiv (q : Quaternion (DualNumber R)) :
     (dualNumberEquiv q).snd.imK = q.imK.snd :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem fst_re_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) :
     (dualNumberEquiv.symm d).re.fst = d.fst.re :=

Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean

@@ -282,7 +282,6 @@ lemma leftUnshift_add {n' a : ℤ} (γ₁ γ₂ : Cochain (K⟦a⟧) L n') (n :
   change (leftShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _
   apply map_add
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma rightShift_smul (a n' : ℤ) (hn' : n' + a = n) (x : R) :
     (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn' := by

Mathlib/Algebra/Homology/HomotopyCofiber.lean

@@ -458,7 +458,6 @@ noncomputable def nullHomotopicMap : K.cylinder ⟶ K.cylinder :=
 noncomputable def nullHomotopy : Homotopy (nullHomotopicMap K) 0 :=
   Homotopy.nullHomotopy' _
 
-set_option backward.isDefEq.respectTransparency false in
 lemma inlX_nullHomotopy_f (i j : ι) (hij : c.Rel j i) :
     inlX K i j hij ≫ (nullHomotopicMap K).f j =
       inlX K i j hij ≫ (π K ≫ ι₀ K - 𝟙 _).f j := by

Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean

@@ -206,14 +206,12 @@ variable {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N
 
 open CategoryTheory
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Given a linear map `f : M → N`, we can obtain a short complex `0 → ker(f) → M → N`. -/
 abbrev LinearMap.shortComplexKer (f : M →ₗ[R] N) : ShortComplex (ModuleCat.{v} R) where
   f := ModuleCat.ofHom.{v} (LinearMap.ker f).subtype
   g := ModuleCat.ofHom.{v} f
   zero := by ext; simp
 
-set_option backward.isDefEq.respectTransparency false in
 theorem LinearMap.shortExact_shortComplexKer {f : M →ₗ[R] N} (h : Function.Surjective f) :
     f.shortComplexKer.ShortExact where
   exact := (ShortComplex.ShortExact.moduleCat_exact_iff_function_exact _).mpr

Mathlib/Algebra/Lie/TraceForm.lean

@@ -217,7 +217,6 @@ open TensorProduct
 
 variable [LieRing.IsNilpotent L] [IsDomain R]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma traceForm_eq_sum_genWeightSpaceOf [IsPrincipalIdealRing R]
     [Module.IsTorsionFree R M] [IsNoetherian R M] [IsTriangularizable R L M] (z : L) :
     traceForm R L M =
@@ -408,7 +407,6 @@ namespace LieModule
 variable [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M]
 variable [LieRing.IsNilpotent L] [LinearWeights K L M] [IsTriangularizable K L M]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma traceForm_eq_sum_finrank_nsmul_mul (x y : L) :
     traceForm K L M x y = ∑ χ : Weight K L M, finrank K (genWeightSpace M χ) • (χ x * χ y) := by
   have hxy : ∀ χ : Weight K L M, MapsTo (toEnd K L M x ∘ₗ toEnd K L M y)

Mathlib/Algebra/Lie/Weights/Chain.lean

@@ -203,7 +203,6 @@ lemma trace_toEnd_genWeightSpaceChain_eq_zero
   | add => simp_all
   | smul => simp_all
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Given a (potential) root `α` relative to a Cartan subalgebra `H`, if we restrict to the ideal
 `I = corootSpace α` of `H` (informally, `I = ⁅H(α), H(-α)⁆`), we may find an
 integral linear combination between `α` and any weight `χ` of a representation.

Mathlib/Algebra/Lie/Weights/Killing.lean

@@ -100,7 +100,6 @@ variable [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra]
 section
 variable [IsTriangularizable K H L]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- For any `α` and `β`, the corresponding root spaces are orthogonal with respect to the Killing
 form, provided `α + β ≠ 0`. -/
 lemma killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero {α β : H → K} {x y : L}

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -210,7 +210,6 @@ lemma Module.FinitePresentation.fg_ker_iff [Module.FinitePresentation R M]
     Submodule.FG (LinearMap.ker l) ↔ Module.FinitePresentation R N :=
   ⟨finitePresentation_of_surjective l hl, fun _ ↦ fg_ker l hl⟩
 
-set_option backward.isDefEq.respectTransparency false in
 lemma Module.finitePresentation_of_ker [Module.FinitePresentation R N]
     (l : M →ₗ[R] N) (hl : Function.Surjective l) [Module.FinitePresentation R (LinearMap.ker l)] :
     Module.FinitePresentation R M := by
@@ -285,7 +284,6 @@ instance (priority := 900) of_subsingleton [Subsingleton M] :
     Module.FinitePresentation R M :=
   .of_equiv (default : (Fin 0 → R) ≃ₗ[R] M)
 
-set_option backward.isDefEq.respectTransparency false in
 variable (M N) in
 instance prod [Module.FinitePresentation R M] [Module.FinitePresentation R N] :
     Module.FinitePresentation R (M × N) := by
@@ -330,7 +328,6 @@ lemma Module.FinitePresentation.trans (S : Type*) [CommRing S] [Algebra R S]
     simp only [f, LinearMap.ker_restrictScalars, ← Module.Finite.iff_fg]
     exact Module.Finite.trans S _
 
-set_option backward.isDefEq.respectTransparency false in
 open TensorProduct in
 instance {A} [CommRing A] [Algebra R A] [Module.FinitePresentation R M] :
     Module.FinitePresentation A (A ⊗[R] M) := by

Mathlib/Algebra/Module/Injective.lean

@@ -402,7 +402,6 @@ protected theorem injective (h : Module.Baer R Q) : Module.Injective R Q where
     obtain ⟨h, H⟩ := Module.Baer.extension_property h i hi f
     exact ⟨h, DFunLike.congr_fun H⟩
 
-set_option backward.isDefEq.respectTransparency false in
 protected theorem of_injective [Small.{v} R] (inj : Module.Injective R Q) : Module.Baer R Q := by
   intro I g
   let eI := Shrink.linearEquiv R I

Mathlib/Algebra/Module/Lattice.lean

@@ -134,7 +134,6 @@ lemma _root_.Submodule.span_range_eq_top_of_injective_of_rank_le {M N : Type u}
 
 variable (K) {V : Type*} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Any basis of an `R`-lattice in `V` defines a `K`-basis of `V`. -/
 noncomputable def _root_.Module.Basis.extendOfIsLattice [IsFractionRing R K] {κ : Type*}
     {M : Submodule R V} [IsLattice K M] (b : Basis κ R M) :
@@ -157,7 +156,6 @@ lemma _root_.Module.Basis.extendOfIsLattice_apply [IsFractionRing R K] {κ : Typ
 
 variable [IsDomain R]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- A finitely-generated `R`-submodule of `V` of rank at least the `K`-rank of `V`
 is a lattice. -/
 lemma of_rank_le [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V}
@@ -168,7 +166,6 @@ lemma of_rank_le [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V}
 
 variable [IsPrincipalIdealRing R]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Any lattice over a PID is a free `R`-module.
 Note that under our conditions, `Module.IsTorsionFree R K` simply says that `algebraMap R K` is
 injective. -/
@@ -194,7 +191,6 @@ lemma finrank_of_pi {ι : Type*} [Fintype ι] [IsFractionRing R K] (M : Submodul
     [IsLattice K M] : Module.finrank R M = Fintype.card ι :=
   Module.finrank_eq_of_rank_eq (IsLattice.rank_of_pi K M)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The intersection of two lattices is a lattice. -/
 instance inf [Module.Finite K V] [IsFractionRing R K] (M N : Submodule R V)
     [IsLattice K M] [IsLattice K N] : IsLattice K (M ⊓ N) where