-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this_1 : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1 P, algebraMap := map_toInfinitesimal_bijective._aux_2 P,
    commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower.{u, u, u_3} P.Ring P.infinitesimal.Ring S
a :
  ∀ (x : S) (a : P.Ring),
    Eq (α := P.infinitesimal.CotangentSpace)
      (((((LinearMap.compDer
                      (((AlgebraTensorModule.curry
                              ((↑P.Ring :
                                  {S_1 : Type u_3} →
                                    {M M₂ : Type (max u u_3)} →
                                      [inst_3 : Semiring P.Ring] →
                                        [inst_4 : Semiring S_1] →
                                          [inst_5 : AddCommMonoid M] →
                                            [inst_6 : AddCommMonoid M₂] →
                                              [inst_7 : Module P.Ring M] →
                                                [inst_8 : Module P.Ring M₂] →
                                                  [inst_9 : Module S_1 M] →
                                                    [inst_10 : Module S_1 M₂] →
                                                      [LinearMap.CompatibleSMul M M₂ P.Ring S_1] →
                                                        (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
                                (CotangentSpace.map P.toInfinitesimal)) :
                            LinearMap (R := P.Ring) (RingHom.id P.Ring) S
                              (LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R]
                                P.infinitesimal.CotangentSpace)) :
                          (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] P.infinitesimal.CotangentSpace)
                        x) :
                    LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
                      (Derivation R P.Ring P.infinitesimal.CotangentSpace)) :
                  (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring P.infinitesimal.CotangentSpace)
                (D R P.Ring) :
              Derivation R P.Ring P.infinitesimal.CotangentSpace) :
            (a : P.Ring) → P.infinitesimal.CotangentSpace)
          a :
        P.infinitesimal.CotangentSpace)
      (((((LinearMap.compDer
                      (((AlgebraTensorModule.curry
                              ((↑P.Ring :
                                  {S_1 : Type u_3} →
                                    {M M₂ : Type (max u u_3)} →
                                      [inst_3 : Semiring P.Ring] →
                                        [inst_4 : Semiring S_1] →
                                          [inst_5 : AddCommMonoid M] →
                                            [inst_6 : AddCommMonoid M₂] →
                                              [inst_7 : Module P.Ring M] →
                                                [inst_8 : Module P.Ring M₂] →
                                                  [inst_9 : Module S_1 M] →
                                                    [inst_10 : Module S_1 M₂] →
                                                      [LinearMap.CompatibleSMul M M₂ P.Ring S_1] →
                                                        (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
                                (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
                                  S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
                                    S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2]
                                      Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])) :
                            LinearMap (R := P.Ring) (RingHom.id P.Ring) S
                              (LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R]
                                P.infinitesimal.CotangentSpace)) :
                          (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] P.infinitesimal.CotangentSpace)
                        x) :
                    LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
                      (Derivation R P.Ring P.infinitesimal.CotangentSpace)) :
                  (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring P.infinitesimal.CotangentSpace)
                (D R P.Ring) :
              Derivation R P.Ring P.infinitesimal.CotangentSpace) :
            (a : P.Ring) → P.infinitesimal.CotangentSpace)
          a :
        P.infinitesimal.CotangentSpace)
⊢ Eq (α := LinearMap (R := P.Ring) (RingHom.id P.Ring) P.CotangentSpace P.infinitesimal.CotangentSpace)
    ((↑P.Ring :
        {S_1 : Type u_3} →
          {M M₂ : Type (max u u_3)} →
            [inst_3 : Semiring P.Ring] →
              [inst_4 : Semiring S_1] →
                [inst_5 : AddCommMonoid M] →
                  [inst_6 : AddCommMonoid M₂] →
                    [inst_7 : Module P.Ring M] →
                      [inst_8 : Module P.Ring M₂] →
                        [inst_9 : Module S_1 M] →
                          [inst_10 : Module S_1 M₂] →
                            [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
      (CotangentSpace.map P.toInfinitesimal))
    ((↑P.Ring :
        {S_1 : Type u_3} →
          {M M₂ : Type (max u u_3)} →
            [inst_3 : Semiring P.Ring] →
              [inst_4 : Semiring S_1] →
                [inst_5 : AddCommMonoid M] →
                  [inst_6 : AddCommMonoid M₂] →
                    [inst_7 : Module P.Ring M] →
                      [inst_8 : Module P.Ring M₂] →
                        [inst_9 : Module S_1 M] →
                          [inst_10 : Module S_1 M₂] →
                            [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
      (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
        S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
          S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]))

Tactic:
ext x a