-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
h₂ : HPow.hPow (α := Ideal P') (β := ℕ) (RingHom.ker (F := P' →+* S) (algebraMap P' S)) 2 = ⊥
e₁ : Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) ≃ₗ[P]
  ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) :=
  Ideal.cotangentEquivIdeal (RingHom.ker (F := P →+* S) (algebraMap P S)) ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq
        (Ideal.cotangentIdeal (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))))
        (RingHom.ker (F :=
          RingHom.{u_2, u_3}
            (P ⧸
              HPow.hPow (α := Ideal P) (β := ℕ)
                (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2)
            S)
          (AlgHom.toRingHom (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S))))
        ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H :
  kerCotangentToTensor R P S =
    (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) ∘ₗ
      (↑P :
            {S M : Type u_2} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring P] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module P M] →
                          [inst_11 : Module P M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
          (kerToTensor R P' S) ∘ₗ
        (↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S)))
f :
  { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
    l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
⊢ (fun
          (x :
            { l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
              l ∘ₗ kerToTensor R P' S = LinearMap.id }) ↦
        (match (motive :=
            { l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
                l ∘ₗ kerToTensor R P' S = LinearMap.id } →
              { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
                l ∘ₗ kerCotangentToTensor R P S = LinearMap.id })
            x with
          | ⟨l, hl⟩ =>
            Subtype.mk (p :=
              fun (l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S))) ↦
              l ∘ₗ kerCotangentToTensor R P S = LinearMap.id)
              ((↑e₁.symm : ↥(RingHom.ker (algebraMap P' S)) →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent) ∘ₗ
                (↑P :
                      {S : Type u_2} →
                        {M : Type (max u_2 u_3)} →
                          {M₂ : Type u_2} →
                            [inst : Semiring P] →
                              [inst_7 : Semiring S] →
                                [inst_8 : AddCommMonoid M] →
                                  [inst_9 : AddCommMonoid M₂] →
                                    [inst_10 : Module P M] →
                                      [inst_11 : Module P M₂] →
                                        [inst_12 : Module S M] →
                                          [inst_13 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
                    l ∘ₗ
                  (↑e₂.symm : S ⊗[P] Ω[P⁄R] →ₗ[P] S ⊗[P'] Ω[P'⁄R]))
              ⋯ :
          { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
            l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }))
      ((fun
            (x :
              { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
                l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }) ↦
          (match (motive :=
              { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
                  l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } →
                { l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
                  l ∘ₗ kerToTensor R P' S = LinearMap.id })
              x with
            | ⟨l, hl⟩ =>
              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)
                {
                  toAddHom :=
                    (↑((↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S))) ∘ₗ
                          l ∘ₗ (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R])) :
                      S ⊗[P'] Ω[P'⁄R] →ₙ+ ↥(RingHom.ker (algebraMap P' S))),
                  map_smul' := ⋯ }
                ⋯ :
            { l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
              l ∘ₗ kerToTensor R P' S = LinearMap.id }))
        f) =
    f
have refine_4 : ∀ (x : S) (a : P),
  Eq (α := Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)))
    (((((LinearMap.compDer
                    (((AlgebraTensorModule.curry
                            (↑((fun
                                      (x :
                                        { l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
                                          l ∘ₗ kerToTensor R P' S = LinearMap.id }) ↦
                                    (match (motive :=
                                        { l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
                                            l ∘ₗ kerToTensor R P' S = LinearMap.id } →
                                          { l :
                                            S ⊗[P] Ω[P⁄R] →ₗ[P]
                                              Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
                                            l ∘ₗ kerCotangentToTensor R P S = LinearMap.id })
                                        x with
                                      | ⟨l, hl⟩ =>
                                        Subtype.mk (p :=
                                          fun
                                            (l :
                                              S ⊗[P] Ω[P⁄R] →ₗ[P]
                                                Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S))) ↦
                                          l ∘ₗ kerCotangentToTensor R P S = LinearMap.id)
                                          ((↑e₁.symm :
                                              ↥(RingHom.ker (algebraMap P' S)) →ₗ[P]
                                                (RingHom.ker (algebraMap P S)).Cotangent) ∘ₗ
                                            (↑P :
                                                  {S : Type u_2} →
                                                    {M : Type (max u_2 u_3)} →
                                                      {M₂ : Type u_2} →
                                                        [inst : Semiring P] →
                                                          [inst_7 : Semiring S] →
                                                            [inst_8 : AddCommMonoid M] →
                                                              [inst_9 : AddCommMonoid M₂] →
                                                                [inst_10 : Module P M] →
                                                                  [inst_11 : Module P M₂] →
                                                                    [inst_12 : Module S M] →
                                                                      [inst_13 : Module S M₂] →
                                                                        [LinearMap.CompatibleSMul M M₂ P S] →
                                                                          (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
                                                l ∘ₗ
                                              (↑e₂.symm : S ⊗[P] Ω[P⁄R] →ₗ[P] S ⊗[P'] Ω[P'⁄R]))
                                          sorry :
                                      { l :
                                        S ⊗[P] Ω[P⁄R] →ₗ[P]
                                          Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
                                        l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }))
                                  ((fun
                                        (x :
                                          { l :
                                            S ⊗[P] Ω[P⁄R] →ₗ[P]
                                              Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
                                            l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }) ↦
                                      (match (motive :=
                                          { l :
                                              S ⊗[P] Ω[P⁄R] →ₗ[P]
                                                Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
                                              l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } →
                                            { l :
                                              S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
                                              l ∘ₗ kerToTensor R P' S = LinearMap.id })
                                          x with
                                        | ⟨l, hl⟩ =>
                                          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)
                                            {
                                              toAddHom :=
                                                (↑((↑e₁ :
                                                        (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P]
                                                          ↥(RingHom.ker (algebraMap P' S))) ∘ₗ
                                                      l ∘ₗ (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R])) :
                                                  S ⊗[P'] Ω[P'⁄R] →ₙ+ ↥(RingHom.ker (algebraMap P' S))),
                                              map_smul' := sorry }
                                            sorry :
                                        { l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
                                          l ∘ₗ kerToTensor R P' S = LinearMap.id }))
                                    f)) :
                              S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent) :
                          S →ₗ[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S))) :
                        (a : S) → Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent)
                      x) :
                  Derivation R P Ω[P⁄R] →ₗ[P]
                    Derivation R P (Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)))) :
                (a : Derivation R P Ω[P⁄R]) → Derivation R P (RingHom.ker (algebraMap P S)).Cotangent)
              (D R P) :
            Derivation R P (Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)))) :
          (a : P) → (RingHom.ker (algebraMap P S)).Cotangent)
        a :
      Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)))
    (((((LinearMap.compDer
                    (((AlgebraTensorModule.curry (↑f : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent) :
                          S →ₗ[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S))) :
                        (a : S) → Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent)
                      x) :
                  Derivation R P Ω[P⁄R] →ₗ[P]
                    Derivation R P (Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)))) :
                (a : Derivation R P Ω[P⁄R]) → Derivation R P (RingHom.ker (algebraMap P S)).Cotangent)
              (D R P) :
            Derivation R P (Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)))) :
          (a : P) → (RingHom.ker (algebraMap P S)).Cotangent)
        a :
      Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)))
Tactic: ext x