-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
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)
have a₁ : Eq (α := P.infinitesimal.CotangentSpace)
  ((CotangentSpace.map P.toInfinitesimal : (a : S ⊗[P.Ring] Ω[P.Ring⁄R]) → P.infinitesimal.CotangentSpace)
      (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a) :
    P.infinitesimal.CotangentSpace)
  (((↑(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]) :
        (a : S ⊗[P.Ring] Ω[P.Ring⁄R]) → P.infinitesimal.CotangentSpace)
      (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a) :
    P.infinitesimal.CotangentSpace)
Tactic: dsimp