-- 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)
f₁ : LinearMap (R := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
  (RingHom.id (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
  Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R] (S ⊗[P] Ω[P⁄R]) :=
  Derivation.liftKaehlerDifferential (R := R) (S :=
    P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) (M := S ⊗[P] Ω[P⁄R])
    (derivationQuotKerSq R P S)
f₂ : TensorProduct.{u_2, u_3, u_2}
    (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) S
    Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R] →ₗ[S]
  S ⊗[P] Ω[P⁄R] :=
  AlgebraTensorModule.lift
    ((LinearEquiv.symm
          (LinearMap.ringLmapEquivSelf S S
            (LinearMap (R := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
              (RingHom.id (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
              Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R]
              (S ⊗[P] Ω[P⁄R]))) :
        (a : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R]) →
          S →ₗ[S] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R])
      f₁)
f₃ : Ω[P⁄R] →ₗ[P] Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R] :=
  KaehlerDifferential.map R R P (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
f₄ : Ω[P⁄R] →ₗ[P]
  TensorProduct.{u_2, u_3, u_2} (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
    S Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R] :=
  (↑P :
        {S M : Type u_2} →
          {M₂ : Type (max u_3 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₂)
      (S := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
      ((mk (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) S
            Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R] :
          (a : S) →
            Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
              S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
        1) ∘ₗ
    f₃
f₅ : S ⊗[P] Ω[P⁄R] →ₗ[S]
  TensorProduct.{u_2, u_3, u_2} (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
    S Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R] :=
  AlgebraTensorModule.lift
    ((LinearEquiv.symm
          (LinearMap.ringLmapEquivSelf S S
            (Ω[P⁄R] →ₗ[P]
              TensorProduct.{u_2, u_3, u_2}
                (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) S
                Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R])) :
        (a : Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) →
          S →ₗ[S] Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
      f₄)
suffices : f₅ ∘ₗ f₂ = LinearMap.id
⊢ Function.LeftInverse
    (⇑f₅ : (a : S ⊗[P] Ω[P⁄R]) → S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
    f₂.toFun

Tactic:
suffices f₅.comp f₂ = LinearMap.id from LinearMap.congr_fun this