chore: reduce defeq abuse (#35286)

Cherry-picked from #35182, improved

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

Author: urkud

Mathlib/Algebra/Module/SnakeLemma.lean

@@ -48,15 +48,15 @@ such that `f₂` is surjective with a (set-theoretic) section `σ`, `g₁` is in
 (set-theoretic) retraction `ρ`, and that `ι₃` is injective and `π₁` is surjective.
 -/
 
-variable {R} [CommRing R] {M₁ M₂ M₃ N₁ N₂ N₃}
+variable {R : Type*} [CommRing R] {M₁ M₂ M₃ N₁ N₂ N₃ : Type*}
   [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃]
   [AddCommGroup N₁] [Module R N₁] [AddCommGroup N₂] [Module R N₂] [AddCommGroup N₃] [Module R N₃]
   (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃)
   (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (hf : Exact f₁ f₂)
   (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (hg : Exact g₁ g₂)
   (h₁ : g₁.comp i₁ = i₂.comp f₁) (h₂ : g₂.comp i₂ = i₃.comp f₂)
   (σ : M₃ → M₂) (hσ : f₂ ∘ σ = id) (ρ : N₂ → N₁) (hρ : ρ ∘ g₁ = id)
-  {K₂ K₃ C₁ C₂} [AddCommGroup K₂] [Module R K₂] [AddCommGroup K₃] [Module R K₃]
+  {K₂ K₃ C₁ C₂ : Type*} [AddCommGroup K₂] [Module R K₂] [AddCommGroup K₃] [Module R K₃]
   [AddCommGroup C₁] [Module R C₁] [AddCommGroup C₂] [Module R C₂]
   (ι₂ : K₂ →ₗ[R] M₂) (hι₂ : Exact ι₂ i₂) (ι₃ : K₃ →ₗ[R] M₃) (hι₃ : Exact ι₃ i₃)
   (π₁ : N₁ →ₗ[R] C₁) (hπ₁ : Exact i₁ π₁) (π₂ : N₂ →ₗ[R] C₂) (hπ₂ : Exact i₂ π₂)

Mathlib/Algebra/MonoidAlgebra/Grading.lean

@@ -80,11 +80,12 @@ theorem grade_eq_lsingle_range (m : M) :
   Submodule.ext (mem_grade_iff' R m)
 
 theorem single_mem_gradeBy {R} [CommSemiring R] (f : M → ι) (m : M) (r : R) :
-    Finsupp.single m r ∈ gradeBy R f (f m) := by
+    single m r ∈ gradeBy R f (f m) := by
   intro x hx
   rw [Finset.mem_singleton.mp (Finsupp.support_single_subset hx)]
 
-theorem single_mem_grade {R} [CommSemiring R] (i : M) (r : R) : Finsupp.single i r ∈ grade R i :=
+theorem single_mem_grade {R} [CommSemiring R] (i : M) (r : R) :
+    single i r ∈ grade R i :=
   single_mem_gradeBy _ _ _
 
 end

Mathlib/RingTheory/AdjoinRoot.lean

@@ -874,51 +874,69 @@ open Ideal DoubleQuot Polynomial
 
 variable [CommRing R] (I : Ideal R) (f : R[X])
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The natural isomorphism `R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f))` for `α` a root of
 `f : R[X]` and `I : Ideal R`.
 
-See `adjoin_root.quot_map_of_equiv` for the isomorphism with `(R/I)[X] / (f mod I)`. -/
-def quotMapOfEquivQuotMapCMapSpanMk :
+See `AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot`
+for the isomorphism with `(R/I)[X] / (f mod I)`. -/
+def quotMapOfEquivQuotMapCMapMk :
     AdjoinRoot f ⧸ I.map (of f) ≃+*
-      AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span {f})) :=
+      AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (AdjoinRoot.mk f) :=
   Ideal.quotEquivOfEq (by rw [of, AdjoinRoot.mk, Ideal.map_map])
 
+@[deprecated (since := "2026-03-02")]
+alias quotMapOfEquivQuotMapCMapSpanMk := quotMapOfEquivQuotMapCMapMk
+
 @[simp]
-theorem quotMapOfEquivQuotMapCMapSpanMk_mk (x : AdjoinRoot f) :
-    quotMapOfEquivQuotMapCMapSpanMk I f (Ideal.Quotient.mk (I.map (of f)) x) =
+theorem quotMapOfEquivQuotMapCMapMk_mk (x : AdjoinRoot f) :
+    quotMapOfEquivQuotMapCMapMk I f (Ideal.Quotient.mk (I.map (of f)) x) =
       Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (I.map (C : R →+* R[X]))) x := rfl
 
-set_option backward.isDefEq.respectTransparency false in
+@[deprecated (since := "2026-03-02")]
+alias quotMapOfEquivQuotMapCMapSpanMk_mk := quotMapOfEquivQuotMapCMapMk_mk
+
 --this lemma should have the simp tag but this causes a lint issue
-theorem quotMapOfEquivQuotMapCMapSpanMk_symm_mk (x : AdjoinRoot f) :
-    (quotMapOfEquivQuotMapCMapSpanMk I f).symm
+theorem quotMapOfEquivQuotMapCMapMk_symm_mk (x : AdjoinRoot f) :
+    (quotMapOfEquivQuotMapCMapMk I f).symm
         (Ideal.Quotient.mk ((I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span {f}))) x) =
       Ideal.Quotient.mk (I.map (of f)) x := by
-  rw [quotMapOfEquivQuotMapCMapSpanMk, Ideal.quotEquivOfEq_symm]
+  rw [quotMapOfEquivQuotMapCMapMk, Ideal.quotEquivOfEq_symm]
   exact Ideal.quotEquivOfEq_mk _ _
 
+@[deprecated (since := "2026-03-02")]
+alias quotMapOfEquivQuotMapCMapSpanMk_symm_mk := quotMapOfEquivQuotMapCMapMk_symm_mk
+
 /-- The natural isomorphism `R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x])`
   for `α` a root of `f : R[X]` and `I : Ideal R` -/
-def quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk :
-    AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span ({f} : Set R[X]))) ≃+*
+def quotMapCMapSpanMkEquivQuotMapCQuotMapMk :
+    AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (AdjoinRoot.mk f) ≃+*
       (R[X] ⧸ I.map (C : R →+* R[X])) ⧸
         (span ({f} : Set R[X])).map (Ideal.Quotient.mk (I.map (C : R →+* R[X]))) :=
   quotQuotEquivComm (Ideal.span ({f} : Set R[X])) (I.map (C : R →+* R[X]))
 
+@[deprecated (since := "2026-03-02")]
+alias quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk := quotMapCMapSpanMkEquivQuotMapCQuotMapMk
+
 -- This lemma should have the simp tag but this causes a lint issue.
-theorem quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk (p : R[X]) :
-    quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f (Ideal.Quotient.mk _ (mk f p)) =
+theorem quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk (p : R[X]) :
+    quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f (Ideal.Quotient.mk _ (mk f p)) =
       quotQuotMk (I.map C) (span {f}) p :=
   rfl
 
+@[deprecated (since := "2026-03-02")]
+alias quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk := quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk
+
 @[simp]
-theorem quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk (p : R[X]) :
-    (quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f).symm (quotQuotMk (I.map C) (span {f}) p) =
+theorem quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk (p : R[X]) :
+    (quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm (quotQuotMk (I.map C) (span {f}) p) =
       Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (I.map (C : R →+* R[X])))
         (mk f p) :=
   rfl
 
+@[deprecated (since := "2026-03-02")]
+alias quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk :=
+  quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk
+
 /-- The natural isomorphism `(R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x])` where
   `f : R[X]` and `I : Ideal R` -/
 def Polynomial.quotQuotEquivComm :
@@ -951,8 +969,8 @@ theorem Polynomial.quotQuotEquivComm_symm_mk_mk (p : R[X]) :
 def quotAdjoinRootEquivQuotPolynomialQuot :
     AdjoinRoot f ⧸ I.map (of f) ≃+*
     (R ⧸ I)[X] ⧸ span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X]) :=
-  (quotMapOfEquivQuotMapCMapSpanMk I f).trans
-    ((quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f).trans
+  (quotMapOfEquivQuotMapCMapMk I f).trans
+    ((quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).trans
       ((Ideal.quotEquivOfEq (by rw [map_span, Set.image_singleton])).trans
         (Polynomial.quotQuotEquivComm I f).symm))
 
@@ -962,7 +980,6 @@ theorem quotAdjoinRootEquivQuotPolynomialQuot_mk_of (p : R[X]) :
       Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X]))
       (p.map (Ideal.Quotient.mk I)) := rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk (p : R[X]) :
     (quotAdjoinRootEquivQuotPolynomialQuot I f).symm
@@ -973,8 +990,8 @@ theorem quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk (p : R[X]) :
     RingEquiv.symm_trans_apply, RingEquiv.symm_trans_apply, RingEquiv.symm_symm,
     Polynomial.quotQuotEquivComm_mk, Ideal.quotEquivOfEq_symm, Ideal.quotEquivOfEq_mk, ←
     RingHom.comp_apply, ← DoubleQuot.quotQuotMk,
-    quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk,
-    quotMapOfEquivQuotMapCMapSpanMk_symm_mk]
+    quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk,
+    quotMapOfEquivQuotMapCMapMk_symm_mk]
 
 /-- Promote `AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot` to an alg_equiv. -/
 @[simps!]

Mathlib/RingTheory/Kaehler/Basic.lean

@@ -175,6 +175,9 @@ instance KaehlerDifferential.isScalarTower' : IsScalarTower R (S ⊗[R] S) Ω[S
 def KaehlerDifferential.fromIdeal : KaehlerDifferential.ideal R S →ₗ[S ⊗[R] S] Ω[S⁄R] :=
   (KaehlerDifferential.ideal R S).toCotangent
 
+theorem KaehlerDifferential.fromIdeal_surjective : Function.Surjective (fromIdeal R S) :=
+  Ideal.toCotangent_surjective _
+
 /-- (Implementation) The underlying linear map of the derivation into `Ω[S⁄R]`. -/
 def KaehlerDifferential.DLinearMap : S →ₗ[R] Ω[S⁄R] :=
   ((KaehlerDifferential.fromIdeal R S).restrictScalars R).comp
@@ -219,13 +222,14 @@ theorem KaehlerDifferential.span_range_derivation :
     Submodule.span S (Set.range <| KaehlerDifferential.D R S) = ⊤ := by
   rw [_root_.eq_top_iff]
   rintro x -
-  obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
-  have : x ∈ (KaehlerDifferential.ideal R S).restrictScalars S := hx
-  rw [← KaehlerDifferential.submodule_span_range_eq_ideal] at this
-  suffices ∃ hx, (KaehlerDifferential.ideal R S).toCotangent ⟨x, hx⟩ ∈
-      Submodule.span S (Set.range <| KaehlerDifferential.D R S) by
-    exact this.choose_spec
-  refine Submodule.span_induction ?_ ?_ ?_ ?_ this
+  obtain ⟨⟨x, hx⟩, rfl⟩ := fromIdeal_surjective R S x
+  rw [← Submodule.restrictScalars_mem S, ← KaehlerDifferential.submodule_span_range_eq_ideal] at hx
+  suffices ∃ hx,
+      fromIdeal R S ⟨x, hx⟩ ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) from
+    this.snd
+  -- TODO: this proof looks like we're reinventing `Submodule.span_le`.
+  -- I'm not sure what's the RHS here though.
+  refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
   · rintro _ ⟨x, rfl⟩
     refine ⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩
     apply Submodule.subset_span

Mathlib/RingTheory/KrullDimension/Polynomial.lean

@@ -58,7 +58,8 @@ private lemma height_eq_height_add_one_of_isMaximal (p : Ideal R) [p.IsMaximal]
   let _ : Field (R ⧸ p) := Quotient.field p
   suffices h : (P.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p))).height = 1 by
     rw [height_eq_height_add_of_liesOver_of_hasGoingDown p, h]
-  let e : (R[X] ⧸ (p.map C)) ≃+* (R ⧸ p)[X] := (polynomialQuotientEquivQuotientPolynomial p).symm
+  let e : (R[X] ⧸ (p.map (algebraMap R R[X]))) ≃+* (R ⧸ p)[X] :=
+    (polynomialQuotientEquivQuotientPolynomial p).symm
   let P' : Ideal (R ⧸ p)[X] := Ideal.map e <| P.map (Ideal.Quotient.mk <| p.map (algebraMap R R[X]))
   have : (P.map (Ideal.Quotient.mk <| p.map (algebraMap R R[X]))).IsMaximal := by
     refine .map_of_surjective_of_ker_le Quotient.mk_surjective ?_