-- 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 : T ⊗[S] P.CotangentSpace
e_a :
  Eq (α := Derivation R P.Ring (T ⊗[S] P.CotangentSpace))
    (((LinearMap.compDer
              (((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry
                              (LinearMap.liftBaseChange T
                                  (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) ∘ₗ
                                        (↑P.Ring :
                                            {S_1 M : Type u} →
                                              {M₂ : Type (max u_2 u)} →
                                                [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 := P.Ring)
                                          ((TensorProduct.mk P.Ring S Ω[P.Ring⁄R] :
                                              (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] S ⊗[P.Ring] Ω[P.Ring⁄R])
                                            1)) ∘ₗ
                                    (↑(LinearEquiv.symm (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring)) :
                                      Ω[Q.Ring⁄R] →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R])) ∘ₗ
                                LinearMap.liftBaseChange T (CotangentSpace.map f)) :
                            T →ₗ[T] P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace) :
                          (a : T) → P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace)
                        1) :
                    S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] (T ⊗[S] P.CotangentSpace)) :
                  (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] T ⊗[S] P.CotangentSpace)
                1) :
            LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
              (Derivation R P.Ring (T ⊗[S] P.CotangentSpace))) :
          (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring (T ⊗[S] P.CotangentSpace))
        (D R P.Ring) :
      Derivation R P.Ring (T ⊗[S] P.CotangentSpace))
    (((LinearMap.compDer
              (((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry LinearMap.id :
                            T →ₗ[T] P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace) :
                          (a : T) → P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace)
                        1) :
                    S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] (T ⊗[S] P.CotangentSpace)) :
                  (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] T ⊗[S] P.CotangentSpace)
                1) :
            LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
              (Derivation R P.Ring (T ⊗[S] P.CotangentSpace))) :
          (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring (T ⊗[S] P.CotangentSpace))
        (D R P.Ring) :
      Derivation R P.Ring (T ⊗[S] P.CotangentSpace))
⊢ Eq (α := LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] (T ⊗[S] P.CotangentSpace))
    (((AlgebraTensorModule.curry
            (((AlgebraTensorModule.curry
                    (LinearMap.liftBaseChange T
                        (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) ∘ₗ
                              (↑P.Ring :
                                  {S_1 M : Type u} →
                                    {M₂ : Type (max u_2 u)} →
                                      [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 := P.Ring)
                                ((TensorProduct.mk P.Ring S Ω[P.Ring⁄R] :
                                    (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] S ⊗[P.Ring] Ω[P.Ring⁄R])
                                  1)) ∘ₗ
                          (↑(LinearEquiv.symm (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring)) :
                            Ω[Q.Ring⁄R] →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R])) ∘ₗ
                      LinearMap.liftBaseChange T (CotangentSpace.map f)) :
                  T →ₗ[T] P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace) :
                (a : T) → P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace)
              1) :
          S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] (T ⊗[S] P.CotangentSpace)) :
        (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] T ⊗[S] P.CotangentSpace)
      1)
    (((AlgebraTensorModule.curry
            (((AlgebraTensorModule.curry LinearMap.id : T →ₗ[T] P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace) :
                (a : T) → P.CotangentSpace →ₗ[S] T ⊗[S] P.CotangentSpace)
              1) :
          S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] (T ⊗[S] P.CotangentSpace)) :
        (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] T ⊗[S] P.CotangentSpace)
      1)

Tactic:
refine Derivation.liftKaehlerDifferential_unique
        (R := R) (S := P.Ring) (M := T ⊗[S] P.CotangentSpace) _ _ ?_

Premises used: Derivation.liftKaehlerDifferential_unique