-- Module: Mathlib.RingTheory.Etale.Kaehler
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
H : f.toRingHom.FormallyEtale
this_1 : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this_2 : IsScalarTower.{u_1, u, u} R P.Ring Q.Ring
this_3 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_4 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this_5 : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
this : FormallyEtale.{u, u} P.Ring Q.Ring
x_1 : Q.CotangentSpace
a : Q.Ring
x : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]
hx :
  Eq (α := Ω[Q.Ring⁄R])
    ((tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring : (a : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Ω[Q.Ring⁄R]) x :
      Ω[Q.Ring⁄R])
    ((D R Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄R]) a : Ω[Q.Ring⁄R])
e_a :
  Eq (α := Q.CotangentSpace)
    (((↑Q.Ring :
                {S : Type u_3} →
                  {M : Type (max (max u u_2) u_3)} →
                    {M₂ : Type (max u u_3)} →
                      [inst_7 : Semiring Q.Ring] →
                        [inst_8 : Semiring S] →
                          [inst_9 : AddCommMonoid M] →
                            [inst_10 : AddCommMonoid M₂] →
                              [inst_11 : Module Q.Ring M] →
                                [inst_12 : Module Q.Ring M₂] →
                                  [inst_13 : Module S M] →
                                    [inst_14 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ Q.Ring S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[Q.Ring] M₂)
              (LinearMap.liftBaseChange T (CotangentSpace.map f)) ∘ₗ
            LinearMap.liftBaseChange Q.Ring
              ((↑P.Ring :
                    {S_1 : Type u_2} →
                      {M : Type (max u u_2)} →
                        {M₂ : Type (max u_3 u u_2)} →
                          [inst_7 : Semiring P.Ring] →
                            [inst_8 : Semiring S_1] →
                              [inst_9 : AddCommMonoid M] →
                                [inst_10 : AddCommMonoid M₂] →
                                  [inst_11 : Module P.Ring M] →
                                    [inst_12 : Module P.Ring M₂] →
                                      [inst_13 : Module S_1 M] →
                                        [inst_14 : Module S_1 M₂] →
                                          [LinearMap.CompatibleSMul M M₂ P.Ring S_1] →
                                            (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
                  (S := S)
                  ((TensorProduct.mk S T P.CotangentSpace : (a : T) → P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace)
                    1) ∘ₗ
                (TensorProduct.mk P.Ring S Ω[P.Ring⁄R] : (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] S ⊗[P.Ring] Ω[P.Ring⁄R]) 1) :
          (a : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Q.CotangentSpace)
        x :
      Q.CotangentSpace)
    (((TensorProduct.mk Q.Ring T Ω[Q.Ring⁄R] : (a : T) → Ω[Q.Ring⁄R] →ₗ[Q.Ring] T ⊗[Q.Ring] Ω[Q.Ring⁄R]) 1 ∘ₗ
            (↑(tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring) :
              Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[Q.Ring] Ω[Q.Ring⁄R]) :
          (a : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → T ⊗[Q.Ring] Ω[Q.Ring⁄R])
        x :
      TensorProduct.{u, u_3, u} Q.Ring T Ω[Q.Ring⁄R])
⊢ Eq (α := Q.CotangentSpace)
    ((LinearMap.liftBaseChange T (CotangentSpace.map f) : (a : T ⊗[S] P.CotangentSpace) → Q.CotangentSpace)
        ((LinearMap.liftBaseChange Q.Ring
              ((↑P.Ring :
                    {S_1 : Type u_2} →
                      {M : Type (max u u_2)} →
                        {M₂ : Type (max u_3 u u_2)} →
                          [inst_7 : Semiring P.Ring] →
                            [inst_8 : Semiring S_1] →
                              [inst_9 : AddCommMonoid M] →
                                [inst_10 : AddCommMonoid M₂] →
                                  [inst_11 : Module P.Ring M] →
                                    [inst_12 : Module P.Ring M₂] →
                                      [inst_13 : Module S_1 M] →
                                        [inst_14 : Module S_1 M₂] →
                                          [LinearMap.CompatibleSMul M M₂ P.Ring S_1] →
                                            (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
                  (S := S)
                  ((TensorProduct.mk S T P.CotangentSpace : (a : T) → P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace)
                    1) ∘ₗ
                (TensorProduct.mk P.Ring S Ω[P.Ring⁄R] : (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] S ⊗[P.Ring] Ω[P.Ring⁄R]) 1) :
            (a : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → T ⊗[S] P.CotangentSpace)
          x) :
      Q.CotangentSpace)
    (1 ⊗ₜ[Q.Ring]
        (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring : (a : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Ω[Q.Ring⁄R]) x :
      TensorProduct.{u, u_3, u} Q.Ring T Ω[Q.Ring⁄R])

Tactic:
change (((CotangentSpace.map f).liftBaseChange T).restrictScalars Q.Ring ∘ₗ
        LinearMap.liftBaseChange _ _) x = ((TensorProduct.mk _ _ _ 1) ∘ₗ
          (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).toLinearMap) x

Premises used: LinearMap.restrictScalars, Algebra.Extension.CotangentSpace.map, Algebra.Extension.Ring, LinearMap.comp, LinearEquiv.toLinearMap, LinearMap.liftBaseChange, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale, OfNat.ofNat, DFunLike.coe, TensorProduct.mk