chore(RingTheory/Derivation/Basic): generalize `Derivation.compAlgebr…

…aMap` to semirings (#8151)

Also adds a `simps` configuration so we get nice lemmas names with `@[simps]` and shuffles the variable order to put all the types first

Mathlib/RingTheory/Derivation/Basic.lean

@@ -40,8 +40,9 @@ equality. We also require that `D 1 = 0`. See `Derivation.mk'` for a constructor
 assumption from the Leibniz rule when `M` is cancellative.
 
 TODO: update this when bimodules are defined. -/
-structure Derivation (R : Type*) (A : Type*) [CommSemiring R] [CommSemiring A] [Algebra R A]
-    (M : Type*) [AddCommMonoid M] [Module A M] [Module R M] extends A →ₗ[R] M where
+structure Derivation (R : Type*) (A : Type*) (M : Type*)
+    [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M]
+    extends A →ₗ[R] M where
   protected map_one_eq_zero' : toLinearMap 1 = 0
   protected leibniz' (a b : A) : toLinearMap (a * b) = a • toLinearMap b + b • toLinearMap a
 #align derivation Derivation
@@ -53,11 +54,11 @@ namespace Derivation
 
 section
 
-variable {R : Type*} [CommSemiring R]
+variable {R : Type*} {A : Type*} {B : Type*} {M : Type*}
+variable [CommSemiring R] [CommSemiring A] [CommSemiring B] [AddCommMonoid M]
+variable [Algebra R A] [Algebra R B]
+variable [Module A M] [Module B M] [Module R M]
 
-variable {A : Type*} [CommSemiring A] [Algebra R A]
-
-variable {M : Type*} [AddCommMonoid M] [Module A M] [Module R M]
 
 variable (D : Derivation R A M) {D1 D2 : Derivation R A M} (r : R) (a b : A)
 
@@ -77,6 +78,11 @@ theorem toFun_eq_coe : D.toFun = ⇑D :=
   rfl
 #align derivation.to_fun_eq_coe Derivation.toFun_eq_coe
 
+/-- See Note [custom simps projection] -/
+def Simps.apply (D : Derivation R A M) : A → M := D
+
+initialize_simps_projections Derivation (toFun → apply)
+
 attribute [coe] toLinearMap
 
 instance hasCoeToLinearMap : Coe (Derivation R A M) (A →ₗ[R] M) :=
@@ -325,6 +331,17 @@ def _root_.LinearEquiv.compDer : Derivation R A M ≃ₗ[R] Derivation R A N :=
 
 end PushForward
 
+variable (A) in
+/-- For a tower `R → A → B` and an `R`-derivation `B → M`, we may compose with `A → B` to obtain an
+`R`-derivation `A → M`. -/
+@[simps!]
+def compAlgebraMap [Algebra A B] [IsScalarTower R A B] [IsScalarTower A B M]
+    (d : Derivation R B M) : Derivation R A M where
+  map_one_eq_zero' := by simp
+  leibniz' a b := by simp
+  toLinearMap := d.toLinearMap.comp (IsScalarTower.toAlgHom R A B).toLinearMap
+#align derivation.comp_algebra_map Derivation.compAlgebraMap
+
 section RestrictScalars
 
 variable {S : Type*} [CommSemiring S]
@@ -461,4 +478,5 @@ end
 
 end
 
+
 end Derivation

Mathlib/RingTheory/Kaehler.lean

@@ -635,18 +635,6 @@ variable (A B : Type*) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
 
 variable [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B]
 
-variable {R B}
-
-/-- For a tower `R → A → B` and an `R`-derivation `B → M`, we may compose with `A → B` to obtain an
-`R`-derivation `A → M`. -/
-def Derivation.compAlgebraMap [Module A M] [Module B M] [IsScalarTower A B M]
-    (d : Derivation R B M) : Derivation R A M where
-  map_one_eq_zero' := by simp
-  leibniz' a b := by simp
-  toLinearMap := d.toLinearMap.comp (IsScalarTower.toAlgHom R A B).toLinearMap
-#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