-- 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 }
a :
  ∀ (s : S) (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)))
                          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)))
                          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)
⊢ (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) =
    l

Tactic:
ext s p