-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ 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)
have hf₃ : Function.Exact (M := P.H1Cotangent) (N := P.Cotangent) (P := P.CotangentSpace)
  (⇑((↑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 : P.H1Cotangent) → P.Cotangent)
  (⇑((↑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 : P.Cotangent) → P.CotangentSpace)
Tactic: apply Module.Flat.lTensor_exact