-- 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)
g : { g : S →ₐ[R] P // AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }
s : S
a :
  ∀ (s : P),
    Eq.{u_2 + 1} (α := P)
      (((↑((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 }))
                  ((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 }))
                    g)) :
              S →ₐ[R] P) :
            (a : S) → P)
          ((algebraMap P S : (a : P) → S) s : S) :
        P)
      (((↑g : S →ₐ[R] P) : (a : S) → P) ((algebraMap P S : (a : P) → S) s : S) : P)
⊢ Eq.{u_2 + 1} (α := P)
    (((↑((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 }))
                ((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 }))
                  g)) :
            S →ₐ[R] P) :
          (a : S) → P)
        s :
      P)
    (((↑g : S →ₐ[R] P) : (a : S) → P) s : P)

Tactic:
obtain ⟨s, rfl⟩ := hf s

Premises used: rfl