-- 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
inst_7 : Algebra.FormallyEtale S T
h :
  ∀ (x : T) (a : S),
    Eq.{u_3 + 1} (α := Ω[T⁄R])
      (((((LinearMap.compDer
                      (((AlgebraTensorModule.curry
                              (lift
                                ((↑S :
                                    {S_1 M : Type u_3} →
                                      {M₂ : Type (max u_2 u_3)} →
                                        [inst : Semiring S] →
                                          [inst_8 : Semiring S_1] →
                                            [inst_9 : AddCommMonoid M] →
                                              [inst_10 : AddCommMonoid M₂] →
                                                [inst_11 : Module S M] →
                                                  [inst_12 : Module S M₂] →
                                                    [inst_13 : Module S_1 M] →
                                                      [inst_14 : Module S_1 M₂] →
                                                        [LinearMap.CompatibleSMul M M₂ S S_1] →
                                                          (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                                  (S := T)
                                  (((LinearMap.flip
                                          (Algebra.linearMap T
                                            (Module.End T
                                              (LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]))) :
                                        LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R] →ₗ[T]
                                          T →ₗ[T] LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) :
                                      (a : Ω[S⁄R] →ₗ[S] Ω[T⁄R]) → T →ₗ[T] Ω[S⁄R] →ₗ[S] Ω[T⁄R])
                                    (map R R S T)))) :
                            T →ₗ[S] LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) :
                          (a : T) → Ω[S⁄R] →ₗ[S] Ω[T⁄R])
                        x) :
                    Derivation R S Ω[S⁄R] →ₗ[S] Derivation.{u_1, u_2, u_3} R S Ω[T⁄R]) :
                  (a : Derivation R S Ω[S⁄R]) → Derivation R S Ω[T⁄R])
                (D R S) :
              Derivation.{u_1, u_2, u_3} R S Ω[T⁄R]) :
            (a : S) → Ω[T⁄R])
          a :
        Ω[T⁄R])
      (((((LinearMap.compDer
                      (((AlgebraTensorModule.curry
                              ((↑S :
                                  {S_1 : Type u_3} →
                                    {M : Type (max u_2 u_3)} →
                                      {M₂ : Type u_3} →
                                        [inst : Semiring S] →
                                          [inst_8 : Semiring S_1] →
                                            [inst_9 : AddCommMonoid M] →
                                              [inst_10 : AddCommMonoid M₂] →
                                                [inst_11 : Module S M] →
                                                  [inst_12 : Module S M₂] →
                                                    [inst_13 : Module S_1 M] →
                                                      [inst_14 : Module S_1 M₂] →
                                                        [LinearMap.CompatibleSMul M M₂ S S_1] →
                                                          (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                                (↑(tensorKaehlerEquivOfFormallyEtale R S T) : T ⊗[S] Ω[S⁄R] →ₗ[T] Ω[T⁄R])) :
                            T →ₗ[S] LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) :
                          (a : T) → Ω[S⁄R] →ₗ[S] Ω[T⁄R])
                        x) :
                    Derivation R S Ω[S⁄R] →ₗ[S] Derivation.{u_1, u_2, u_3} R S Ω[T⁄R]) :
                  (a : Derivation R S Ω[S⁄R]) → Derivation R S Ω[T⁄R])
                (D R S) :
              Derivation.{u_1, u_2, u_3} R S Ω[T⁄R]) :
            (a : S) → Ω[T⁄R])
          a :
        Ω[T⁄R])
⊢ Eq (α := T ⊗[S] Ω[S⁄R] →ₗ[S] Ω[T⁄R])
    (lift
      ((↑S :
          {S_1 M : Type u_3} →
            {M₂ : Type (max u_2 u_3)} →
              [inst : Semiring S] →
                [inst_8 : Semiring S_1] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module S M] →
                        [inst_12 : Module S M₂] →
                          [inst_13 : Module S_1 M] →
                            [inst_14 : Module S_1 M₂] →
                              [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (S := T)
        (((LinearMap.flip
                (Algebra.linearMap T (Module.End T (LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]))) :
              LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R] →ₗ[T]
                T →ₗ[T] LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) :
            (a : Ω[S⁄R] →ₗ[S] Ω[T⁄R]) → T →ₗ[T] Ω[S⁄R] →ₗ[S] Ω[T⁄R])
          (map R R S T))))
    ((↑S :
        {S_1 : Type u_3} →
          {M : Type (max u_2 u_3)} →
            {M₂ : Type u_3} →
              [inst : Semiring S] →
                [inst_8 : Semiring S_1] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module S M] →
                        [inst_12 : Module S M₂] →
                          [inst_13 : Module S_1 M] →
                            [inst_14 : Module S_1 M₂] →
                              [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
      (↑(tensorKaehlerEquivOfFormallyEtale R S T) : T ⊗[S] Ω[S⁄R] →ₗ[T] Ω[T⁄R]))

Tactic:
ext