-- 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 : P
⊢ 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])
        ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
            (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
          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])
        ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
            (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
          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])

Tactic:
simp [f₁, f₂, f₃, f₄, f₅]