-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
hc₃ :
  ∀ (x : T) (x_1 : P.H1Cotangent),
    Eq (α := Ideal.Cotangent (R := Ring (R := T) (S := T ⊗[R] S) P.baseChange) (ker P.baseChange))
      (Cotangent.val
        (((((AlgebraTensorModule.curry
                      ((↑R :
                            {S : Type (max u_2 u_3)} →
                              {M M₂ : Type (max u u_3)} →
                                [inst : Semiring R] →
                                  [inst_6 : Semiring S] →
                                    [inst_7 : AddCommMonoid M] →
                                      [inst_8 : AddCommMonoid M₂] →
                                        [inst_9 : Module R M] →
                                          [inst_10 : Module R M₂] →
                                            [inst_11 : Module S M] →
                                              [inst_12 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                          h1Cotangentι ∘ₗ
                        (↑R :
                            {S : Type u_3} →
                              {M M₂ : Type (max u u_3)} →
                                [inst : Semiring R] →
                                  [inst_6 : Semiring S] →
                                    [inst_7 : AddCommMonoid M] →
                                      [inst_8 : AddCommMonoid M₂] →
                                        [inst_9 : Module R M] →
                                          [inst_10 : Module R M₂] →
                                            [inst_11 : Module S M] →
                                              [inst_12 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                          (P.tensorToH1Cotangent T)) :
                    T →ₗ[R] P.H1Cotangent →ₗ[R] Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) :
                  (a : T) → P.H1Cotangent →ₗ[R] P.baseChange.Cotangent)
                x :
              P.H1Cotangent →ₗ[R] Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : P.H1Cotangent) → P.baseChange.Cotangent)
          x_1))
      (Cotangent.val
        (((((AlgebraTensorModule.curry
                      ((↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) :
                          T ⊗[R] P.Cotangent →ₗ[R] P.baseChange.Cotangent) ∘ₗ
                        LinearMap.lTensor T
                          ((↑R :
                              {S : Type u_2} →
                                {M M₂ : Type u} →
                                  [inst : Semiring R] →
                                    [inst_6 : Semiring S] →
                                      [inst_7 : AddCommMonoid M] →
                                        [inst_8 : AddCommMonoid M₂] →
                                          [inst_9 : Module R M] →
                                            [inst_10 : Module R M₂] →
                                              [inst_11 : Module S M] →
                                                [inst_12 : Module S M₂] →
                                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                            h1Cotangentι)) :
                    T →ₗ[R] P.H1Cotangent →ₗ[R] Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) :
                  (a : T) → P.H1Cotangent →ₗ[R] P.baseChange.Cotangent)
                x :
              P.H1Cotangent →ₗ[R] Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : P.H1Cotangent) → P.baseChange.Cotangent)
          x_1))
⊢ Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent →ₗ[R] Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    ((↑R :
          {S : Type (max u_2 u_3)} →
            {M M₂ : Type (max u u_3)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h1Cotangentι ∘ₗ
      (↑R :
          {S : Type u_3} →
            {M M₂ : Type (max u u_3)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (P.tensorToH1Cotangent T))
    ((↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) : T ⊗[R] P.Cotangent →ₗ[R] P.baseChange.Cotangent) ∘ₗ
      LinearMap.lTensor T
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h1Cotangentι))

Tactic:
ext