chore: forward-port leanprover-community/mathlib#19234 (#5879)

Unfortunately I was not able to forward port the addition of a partially-explicit type to `kaehler_differential.End_equiv_derivation'`, as Lean 4 no longer allows metavariables in instance arguments.

Mathlib/RingTheory/Ideal/Cotangent.lean

@@ -9,7 +9,7 @@ import Mathlib.Algebra.Ring.Idempotents
 import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.RingTheory.Ideal.LocalRing
 
-#align_import ring_theory.ideal.cotangent from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
+#align_import ring_theory.ideal.cotangent from "leanprover-community/mathlib"@"4b92a463033b5587bb011657e25e4710bfca7364"
 
 /-!
 # The module `I ⧸ I ^ 2`
@@ -47,16 +47,12 @@ instance Cotangent.moduleOfTower : Module S I.Cotangent :=
   Submodule.Quotient.module' _
 #align ideal.cotangent.module_of_tower Ideal.Cotangent.moduleOfTower
 
-instance Cotangent.isScalarTower : IsScalarTower S S' I.Cotangent := by
-  delta Cotangent
-  constructor
-  intro s s' x
-  rw [← @IsScalarTower.algebraMap_smul S' R, ← @IsScalarTower.algebraMap_smul S' R, ← smul_assoc, ←
-    IsScalarTower.toAlgHom_apply S S' R, map_smul]
-  rfl
+instance Cotangent.isScalarTower : IsScalarTower S S' I.Cotangent :=
+  Submodule.Quotient.isScalarTower _ _
 #align ideal.cotangent.is_scalar_tower Ideal.Cotangent.isScalarTower
 
-instance [IsNoetherian R I] : IsNoetherian R I.Cotangent := by delta Cotangent; infer_instance
+instance [IsNoetherian R I] : IsNoetherian R I.Cotangent :=
+  Submodule.Quotient.isNoetherian _
 
 /-- The quotient map from `I` to `I ⧸ I ^ 2`. -/
 @[simps!] --  (config := lemmasOnly) apply -- Porting note: this option does not exist anymore

Mathlib/RingTheory/Kaehler.lean

@@ -7,7 +7,7 @@ import Mathlib.RingTheory.Derivation.ToSquareZero
 import Mathlib.RingTheory.Ideal.Cotangent
 import Mathlib.RingTheory.IsTensorProduct
 
-#align_import ring_theory.kaehler from "leanprover-community/mathlib"@"b608348ffaeb7f557f2fd46876037abafd326ff3"
+#align_import ring_theory.kaehler from "leanprover-community/mathlib"@"4b92a463033b5587bb011657e25e4710bfca7364"
 
 /-!
 # The module of kaehler differentials
@@ -157,28 +157,27 @@ notation:100 "Ω[" S "⁄" R "]" => KaehlerDifferential R S
 
 instance : Nonempty (Ω[S⁄R]) := ⟨0⟩
 
-instance KaehlerDifferential.module' {R' : Type _} [CommRing R'] [Algebra R' S] :
+set_option synthInstance.maxHeartbeats 40000 in
+instance KaehlerDifferential.module' {R' : Type _} [CommRing R'] [Algebra R' S]
+  [SMulCommClass R R' S] :
     Module R' (Ω[S⁄R]) :=
-  (Module.compHom (KaehlerDifferential.ideal R S).Cotangent (algebraMap R' S) : _)
+  Submodule.Quotient.module' _
 #align kaehler_differential.module' KaehlerDifferential.module'
 
 instance : IsScalarTower S (S ⊗[R] S) (Ω[S⁄R]) :=
   Ideal.Cotangent.isScalarTower _
 
+set_option synthInstance.maxHeartbeats 40000 in
 instance KaehlerDifferential.isScalarTower_of_tower {R₁ R₂ : Type _} [CommRing R₁] [CommRing R₂]
-    [Algebra R₁ S] [Algebra R₂ S] [Algebra R₁ R₂] [IsScalarTower R₁ R₂ S] :
-    IsScalarTower R₁ R₂ (Ω[S⁄R]) := by
-  convert RestrictScalars.isScalarTower R₁ R₂ (Ω[S⁄R]) using 1
-  ext (x m)
-  show algebraMap R₁ S x • m = algebraMap R₂ S (algebraMap R₁ R₂ x) • m
-  rw [← IsScalarTower.algebraMap_apply]
+    [Algebra R₁ S] [Algebra R₂ S] [SMul R₁ R₂]
+    [SMulCommClass R R₁ S] [SMulCommClass R R₂ S] [IsScalarTower R₁ R₂ S] :
+    IsScalarTower R₁ R₂ (Ω[S⁄R]) :=
+  Submodule.Quotient.isScalarTower _ _
+
 #align kaehler_differential.is_scalar_tower_of_tower KaehlerDifferential.isScalarTower_of_tower
 
-instance KaehlerDifferential.isScalarTower' : IsScalarTower R (S ⊗[R] S) (Ω[S⁄R]) := by
-  convert RestrictScalars.isScalarTower R (S ⊗[R] S) (Ω[S⁄R]) using 1
-  ext (x m)
-  show algebraMap R S x • m = algebraMap R (S ⊗[R] S) x • m
-  simp_rw [IsScalarTower.algebraMap_apply R S (S ⊗[R] S), IsScalarTower.algebraMap_smul]
+instance KaehlerDifferential.isScalarTower' : IsScalarTower R (S ⊗[R] S) (Ω[S⁄R]) :=
+  Submodule.Quotient.isScalarTower _ _
 #align kaehler_differential.is_scalar_tower' KaehlerDifferential.isScalarTower'
 
 /-- The quotient map `I → Ω[S⁄R]` with `I` being the kernel of `S ⊗[R] S → S`. -/
@@ -207,7 +206,7 @@ set_option linter.uppercaseLean3 false in
 set_option maxHeartbeats 300000 in -- Porting note: Added to prevent timeout
 /-- The universal derivation into `Ω[S⁄R]`. -/
 def KaehlerDifferential.D : Derivation R S (Ω[S⁄R]) :=
-  { KaehlerDifferential.DLinearMap R S with
+  { toLinearMap := KaehlerDifferential.DLinearMap R S
     map_one_eq_zero' := by
       dsimp [KaehlerDifferential.DLinearMap_apply]
       congr
@@ -582,7 +581,7 @@ variable [Algebra A B] [IsScalarTower R S B] [IsScalarTower R A B]
 
 -- The map `(A →₀ A) →ₗ[A] (B →₀ B)`
 local macro "finsupp_map" : term =>
-  `((Finsupp.mapRange.linearMap (Algebra.ofId A B).toLinearMap).comp
+  `((Finsupp.mapRange.linearMap (Algebra.linearMap A B)).comp
     (Finsupp.lmapDomain A A (algebraMap A B)))
 
 set_option maxHeartbeats 400000 in
@@ -597,7 +596,7 @@ theorem KaehlerDifferential.kerTotal_map (h : Function.Surjective (algebraMap A
   simp_rw [Set.image_union, Submodule.span_union, ← Set.image_univ, Set.image_image, Set.image_univ,
     LinearMap.map_sub, LinearMap.map_add]
   simp only [LinearMap.comp_apply, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single,
-    Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, AlgHom.toLinearMap_apply,
+    Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply,
     map_one, map_add, map_mul]
   simp_rw [sup_assoc, ← (h.Prod_map h).range_comp]
   congr 3
@@ -634,6 +633,7 @@ def Derivation.compAlgebraMap [Module A M] [Module B M] [IsScalarTower A B M]
 #align derivation.comp_algebra_map Derivation.compAlgebraMap
 
 variable (R B)
+variable [SMulCommClass S A B]
 
 /-- The map `Ω[A⁄R] →ₗ[A] Ω[B⁄R]` given a square
 A --→ B