-- 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₁ : Eq (α := Unit →ₗ[R] Unit) (0 ∘ₗ 0) (0 ∘ₗ 0)
hc₂ :
  Eq (α := Unit →ₗ[R] Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (0 ∘ₗ 0)
    ((↑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) ∘ₗ
      0)
hc₃ :
  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ι))
hc₄ :
  Eq (α := TensorProduct.{u_1, u_3, u} R T P.Cotangent →ₗ[R] CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (sorry ∘ₗ
      (↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) : T ⊗[R] P.Cotangent →ₗ[R] P.baseChange.Cotangent))
    ((↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T)) :
        T ⊗[R] P.CotangentSpace →ₗ[R] P.baseChange.CotangentSpace) ∘ₗ
      LinearMap.lTensor T
        ((↑R :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u u_2)} →
                  [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.cotangentComplex))
hf₁ :
  Function.Exact (M := Unit) (N := Unit) (P := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (⇑0 : (a : Unit) → Unit)
    (⇑0 : (a : Unit) → T ⊗[R] P.H1Cotangent)
hf₂ :
  Function.Exact (M := Unit) (N := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (P :=
    TensorProduct.{u_1, u_3, u} R T P.Cotangent) (⇑0 : (a : Unit) → T ⊗[R] P.H1Cotangent)
    (⇑(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ι)) :
      (a : T ⊗[R] P.H1Cotangent) → T ⊗[R] P.Cotangent)
hf₃ :
  Function.Exact (M := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (N := TensorProduct.{u_1, u_3, u} R T P.Cotangent)
    (P := T ⊗[R] P.CotangentSpace)
    (⇑(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ι)) :
      (a : T ⊗[R] P.H1Cotangent) → T ⊗[R] P.Cotangent)
    (⇑(LinearMap.lTensor T
          ((↑R :
              {S : Type u_2} →
                {M : Type u} →
                  {M₂ : Type (max u u_2)} →
                    [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.cotangentComplex)) :
      (a : T ⊗[R] P.Cotangent) → T ⊗[R] P.CotangentSpace)
hg₁ :
  Function.Exact (M := Unit) (N := Unit) (P := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑0 : (a : Unit) → Unit) (⇑0 : (a : Unit) → P.baseChange.H1Cotangent)
hg₂ :
  Function.Exact (M := Unit) (N := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (P :=
    Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (⇑0 : (a : Unit) → P.baseChange.H1Cotangent)
    (⇑((↑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ι) :
      (a : P.baseChange.H1Cotangent) → P.baseChange.Cotangent)
hg₃ :
  Function.Exact (M := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (N :=
    Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (P := CotangentSpace (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ι) :
      (a : P.baseChange.H1Cotangent) → P.baseChange.Cotangent)
    (⇑sorry : (a : P.baseChange.Cotangent) → P.baseChange.CotangentSpace)
hi₁ : Function.Surjective (α := Unit) (β := Unit) (⇑0 : (a : Unit) → Unit)
hi₂ : Function.Bijective (α := Unit) (β := Unit) (⇑0 : (a : Unit) → Unit)
hi₄ :
  Function.Bijective (α := TensorProduct.{u_1, u_3, u} R T P.Cotangent) (β :=
    Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑(↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) : T ⊗[R] P.Cotangent →ₗ[R] P.baseChange.Cotangent) :
      (a : T ⊗[R] P.Cotangent) → P.baseChange.Cotangent)
hi₅ :
  Function.Injective (α := T ⊗[R] P.CotangentSpace) (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑(↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T)) :
          T ⊗[R] P.CotangentSpace →ₗ[R] P.baseChange.CotangentSpace) :
      (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace)
apply :
  LinearMap.CompatibleSMul (Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) R (T ⊗[R] S)
⊢ Function.Bijective (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (β :=
    Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑(P.tensorToH1Cotangent T) : (a : T ⊗[R] P.H1Cotangent) → P.baseChange.H1Cotangent)

Tactic:
apply LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective (M₁ := Unit)
      (N₁ := Unit) (M₂ := Unit) (N₂ := Unit)
    -- The row `0 → 0 → T ⊗ H¹(P) → T ⊗ P.Cotangent → T ⊗ P.CotangentSpace`.
    0 0
    ((P.h1Cotangentι.restrictScalars R).lTensor T)
    ((P.cotangentComplex.restrictScalars R).lTensor T)
    -- The row `0 → 0 → H¹(T ⊗ P) → (T ⊗ P).Cotangent → (T ⊗ P).CotangentSpace`.
    0 0
    (h1Cotangentι.restrictScalars R)
    ((P.baseChange (T := T)).cotangentComplex.restrictScalars R)
    -- The vertical maps induced by base change.
    0 0
    ((P.tensorToH1Cotangent T).restrictScalars R)
    ((P.tensorCotangentOfFlat T).restrictScalars R)
    ((P.tensorCotangentSpace T).restrictScalars R)