-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
l : { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
this :
  ∀ (x y : S ⊗[P] Ω[P⁄R]),
    HMul.hMul (α := P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              x) :
          P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              y) :
          P) =
      0
a :
  (s -
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) s)) :
          P)) *
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
        P) =
    (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
            (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
          ((algebraMap P S : (a : P) → S) s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
      P)
⊢ Eq.{u_2 + 1} (α := P)
    (↑(((((LinearMap.compDer
                      (((AlgebraTensorModule.curry
                              (↑((fun
                                        (g :
                                          { g : S →ₐ[R] P //
                                            AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }) ↦
                                      (Subtype.mk (p :=
                                          fun (l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) ↦
                                          l ∘ₗ kerToTensor R P S = LinearMap.id)
                                          (retractionOfSectionOfKerSqZero (↑g : S →ₐ[R] P) hf' ⋯) ⋯ :
                                        { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) //
                                          l ∘ₗ kerToTensor R P S = LinearMap.id }))
                                    ((fun
                                          (l :
                                            { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) //
                                              l ∘ₗ kerToTensor R P S = LinearMap.id }) ↦
                                        (Subtype.mk (p := fun (g : S →ₐ[R] P) ↦
                                            AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S)
                                            (sectionOfRetractionKerToTensor
                                              (↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) ⋯ hf' hf)
                                            ⋯ :
                                          { g : S →ₐ[R] P //
                                            AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }))
                                      l)) :
                                S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                            S →ₗ[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) :
                          (a : S) → Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S)))
                        ((algebraMap P S : (a : P) → S) s)) :
                    Derivation R P Ω[P⁄R] →ₗ[P] Derivation R P ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) :
                  (a : Derivation R P Ω[P⁄R]) → Derivation R P ↥(RingHom.ker (algebraMap P S)))
                (D R P) :
              Derivation R P ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) :
            (a : P) → ↥(RingHom.ker (algebraMap P S)))
          p) :
      P)
    (↑(((((LinearMap.compDer
                      (((AlgebraTensorModule.curry (↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                            S →ₗ[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) :
                          (a : S) → Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S)))
                        ((algebraMap P S : (a : P) → S) s)) :
                    Derivation R P Ω[P⁄R] →ₗ[P] Derivation R P ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) :
                  (a : Derivation R P Ω[P⁄R]) → Derivation R P ↥(RingHom.ker (algebraMap P S)))
                (D R P) :
              Derivation R P ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) :
            (a : P) → ↥(RingHom.ker (algebraMap P S)))
          p) :
      P)

Tactic:
simp only [AlgebraTensorModule.curry_apply,
      Derivation.coe_comp, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Derivation.coeFn_coe,
      Function.comp_apply, curry_apply, retractionOfSectionOfKerSqZero_tmul_D,
      sectionOfRetractionKerToTensor_algebraMap, ← mul_sub, sub_sub_cancel]

Premises used: mul_sub, LinearMap.coe_restrictScalars, Derivation.coe_comp, TensorProduct.AlgebraTensorModule.curry_apply, sub_sub_cancel, Derivation.coeFn_coe, sectionOfRetractionKerToTensor_algebraMap, LinearMap.coe_comp, TensorProduct.curry_apply, Function.comp_apply, retractionOfSectionOfKerSqZero_tmul_D