-- 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₄)
a :
  ∀ (a : P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2),
    Eq (α :=
      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])
      (((((LinearMap.compDer
                      (((AlgebraTensorModule.curry (f₅ ∘ₗ f₂) :
                            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]
                                (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 : 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) :
                    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))
                      (Derivation R
                        (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])
                      (Derivation R
                        (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
                        (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 : Derivation R (P ⧸ RingHom.ker (algebraMap P S) ^ 2) Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) →
                    Derivation R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)
                      (S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]))
                (D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) :
              Derivation R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
                (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 ⧸ RingHom.ker (algebraMap P S) ^ 2) →
              S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
          a :
        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])
      (((((LinearMap.compDer
                      (((AlgebraTensorModule.curry LinearMap.id :
                            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]
                                (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 : 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) :
                    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))
                      (Derivation R
                        (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])
                      (Derivation R
                        (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
                        (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 : Derivation R (P ⧸ RingHom.ker (algebraMap P S) ^ 2) Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) →
                    Derivation R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)
                      (S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]))
                (D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) :
              Derivation R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
                (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 ⧸ RingHom.ker (algebraMap P S) ^ 2) →
              S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
          a :
        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])
⊢ f₅ ∘ₗ f₂ = LinearMap.id

Tactic:
ext a