-- Mathlib/RingTheory/Smooth/Kaehler.lean
@[simp]
lemma retractionOfSectionOfKerSqZero_tmul_D (s : S) (t : P) :
    retractionOfSectionOfKerSqZero g hf' hg (s ⊗ₜ .D _ _ t) =
      g s * t - g s * g (algebraMap _ _ t)

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
s : S
t : P
this : Algebra S P := g.toAlgebra
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg) (s ⊗ₜ[P] (D R P) t)) = g s * t - g s * g ((algebraMap P S) t)

Tactic:
haveI := isScalarTower_of_section_of_ker_sqZero g hf' hg

Result:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
s : S
t : P
this✝ : Algebra S P := g.toAlgebra
this : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg) (s ⊗ₜ[P] (D R P) t)) = g s * t - g s * g ((algebraMap P S) t)

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
s : S
t : P
this✝ : Algebra S P := g.toAlgebra
this : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg) (s ⊗ₜ[P] (D R P) t)) = g s * t - g s * g ((algebraMap P S) t)

Tactic:
simp only [retractionOfSectionOfKerSqZero, AlgHom.toRingHom_eq_coe, LinearMap.coe_restrictScalars,
  LinearMap.liftBaseChange_tmul, SetLike.val_smul_of_tower]

Result:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
s : S
t : P
this✝ : Algebra S P := g.toAlgebra
this : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))
⊢ s • ↑((derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg).liftKaehlerDifferential ((D R P) t)) =
    g s * t - g s * g ((algebraMap P S) t)

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
s : S
t : P
this✝ : Algebra S P := g.toAlgebra
this : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))
⊢ s • ↑((derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg).liftKaehlerDifferential ((D R P) t)) =
    g s * t - g s * g ((algebraMap P S) t)

Tactic:
erw [Derivation.liftKaehlerDifferential_comp_D]

Result:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
s : S
t : P
this✝ : Algebra S P := g.toAlgebra
this : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))
⊢ s • ↑((derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg) t) =
    g s * t - g s * g ((algebraMap P S) t)

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
s : S
t : P
this✝ : Algebra S P := g.toAlgebra
this : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))
⊢ s • ↑((derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg) t) =
    g s * t - g s * g ((algebraMap P S) t)

Tactic:
exact mul_sub (g s) t (g (algebraMap P S t))

Result:
no goals

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
s : S
t : P
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg) (s ⊗ₜ[P] (D R P) t)) = g s * t - g s * g ((algebraMap P S) t)

Tactic:
letI := g.toRingHom.toAlgebra

Result:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
s : S
t : P
this : Algebra S P := g.toAlgebra
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg) (s ⊗ₜ[P] (D R P) t)) = g s * t - g s * g ((algebraMap P S) t)