-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst_3 : AddCommGroup M₁
inst_4 : AddCommGroup M₂
inst_5 : AddCommGroup M₃
inst_6 : AddCommGroup N₁
inst_7 : AddCommGroup N₂
inst_8 : AddCommGroup N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
inst_15 : Module S N₁
inst_16 : Module S N₂
inst_17 : Module S N₃
inst_18 : IsScalarTower R S N₁
inst_19 : IsScalarTower R S N₂
inst_20 : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ :
  h₂ ∘ₗ f =
    (↑R :
          {S : Type u_2} →
            {M : Type u_6} →
              {M₂ : Type u_7} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f' ∘ₗ
      h₁
comm₂ :
  h₃ ∘ₗ g =
    (↑R :
          {S : Type u_2} →
            {M : Type u_7} →
              {M₂ : Type u_8} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        g' ∘ₗ
      h₂
isb₁ :
  Function.Bijective (α := TensorProduct R S M₁) (β := N₁)
    (⇑(TensorProduct.lift
          ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_3 u_6)} →
                  [inst : Semiring R] →
                    [inst_21 : Semiring S] →
                      [inst_22 : AddCommMonoid M] →
                        [inst_23 : AddCommMonoid M₂] →
                          [inst_24 : Module R M] →
                            [inst_25 : Module R M₂] →
                              [inst_26 : Module S M] →
                                [inst_27 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S)
            (((LinearMap.flip (Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))) :
                  (M₁ →ₗ[R] N₁) →ₗ[S] S →ₗ[S] M₁ →ₗ[R] N₁) :
                (a : M₁ →ₗ[R] N₁) → S →ₗ[S] M₁ →ₗ[R] N₁)
              h₁))) :
      (a : TensorProduct R S M₁) → N₁)
isb₂ :
  Function.Bijective (α := TensorProduct R S M₂) (β := N₂)
    (⇑(TensorProduct.lift
          ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_4 u_7)} →
                  [inst : Semiring R] →
                    [inst_21 : Semiring S] →
                      [inst_22 : AddCommMonoid M] →
                        [inst_23 : AddCommMonoid M₂] →
                          [inst_24 : Module R M] →
                            [inst_25 : Module R M₂] →
                              [inst_26 : Module S M] →
                                [inst_27 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S)
            (((LinearMap.flip (Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))) :
                  (M₂ →ₗ[R] N₂) →ₗ[S] S →ₗ[S] M₂ →ₗ[R] N₂) :
                (a : M₂ →ₗ[R] N₂) → S →ₗ[S] M₂ →ₗ[R] N₂)
              h₂))) :
      (a : TensorProduct R S M₂) → N₂)
exact₁ : Function.Exact.{u_3, u_4, u_5} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃)
surj₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M₂) (β := M₃) (⇑g : (a : M₂) → M₃)
exact₂ : Function.Exact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
surj₂ : Function.Surjective.{u_7 + 1, u_8 + 1} (α := N₂) (β := N₃) (⇑g' : (a : N₂) → N₃)
refine_1 :
  Eq (α := TensorProduct R S M₁ →ₗ[R] N₂)
    ((↑R :
          {S : Type u_2} →
            {M : Type u_6} →
              {M₂ : Type u_7} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f' ∘ₗ
      TensorProduct.lift
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type (max u_3 u_6)} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (S := S)
          (((LinearMap.flip (Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))) :
                (M₁ →ₗ[R] N₁) →ₗ[S] S →ₗ[S] M₁ →ₗ[R] N₁) :
              (a : M₁ →ₗ[R] N₁) → S →ₗ[S] M₁ →ₗ[R] N₁)
            h₁)))
    (TensorProduct.lift
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type (max u_4 u_7)} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (S := S)
          (((LinearMap.flip (Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))) :
                (M₂ →ₗ[R] N₂) →ₗ[S] S →ₗ[S] M₂ →ₗ[R] N₂) :
              (a : M₂ →ₗ[R] N₂) → S →ₗ[S] M₂ →ₗ[R] N₂)
            h₂)) ∘ₗ
      (↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type (max u_2 u_4)} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (LinearMap.baseChange S f))
refine_2 :
  Eq (α := TensorProduct R S M₂ →ₗ[R] N₃)
    ((↑R :
          {S : Type u_2} →
            {M : Type u_7} →
              {M₂ : Type u_8} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        g' ∘ₗ
      TensorProduct.lift
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type (max u_4 u_7)} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (S := S)
          (((LinearMap.flip (Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))) :
                (M₂ →ₗ[R] N₂) →ₗ[S] S →ₗ[S] M₂ →ₗ[R] N₂) :
              (a : M₂ →ₗ[R] N₂) → S →ₗ[S] M₂ →ₗ[R] N₂)
            h₂)))
    (TensorProduct.lift
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type (max u_5 u_8)} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (S := S)
          (((LinearMap.flip (Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))) :
                (M₃ →ₗ[R] N₃) →ₗ[S] S →ₗ[S] M₃ →ₗ[R] N₃) :
              (a : M₃ →ₗ[R] N₃) → S →ₗ[S] M₃ →ₗ[R] N₃)
            h₃)) ∘ₗ
      (↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_4)} →
              {M₂ : Type (max u_2 u_5)} →
                [inst : Semiring R] →
                  [inst_21 : Semiring S] →
                    [inst_22 : AddCommMonoid M] →
                      [inst_23 : AddCommMonoid M₂] →
                        [inst_24 : Module R M] →
                          [inst_25 : Module R M₂] →
                            [inst_26 : Module S M] →
                              [inst_27 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (LinearMap.baseChange S g))
refine_3 :
  Function.Exact (M := TensorProduct R S M₁) (N := TensorProduct R S M₂) (P := TensorProduct R S M₃)
    (⇑((↑R :
            {S : Type u_2} →
              {M : Type (max u_2 u_3)} →
                {M₂ : Type (max u_2 u_4)} →
                  [inst : Semiring R] →
                    [inst_21 : Semiring S] →
                      [inst_22 : AddCommMonoid M] →
                        [inst_23 : AddCommMonoid M₂] →
                          [inst_24 : Module R M] →
                            [inst_25 : Module R M₂] →
                              [inst_26 : Module S M] →
                                [inst_27 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (LinearMap.baseChange S f)) :
      (a : TensorProduct R S M₁) → TensorProduct R S M₂)
    (⇑((↑R :
            {S : Type u_2} →
              {M : Type (max u_2 u_4)} →
                {M₂ : Type (max u_2 u_5)} →
                  [inst : Semiring R] →
                    [inst_21 : Semiring S] →
                      [inst_22 : AddCommMonoid M] →
                        [inst_23 : AddCommMonoid M₂] →
                          [inst_24 : Module R M] →
                            [inst_25 : Module R M₂] →
                              [inst_26 : Module S M] →
                                [inst_27 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (LinearMap.baseChange S g)) :
      (a : TensorProduct R S M₂) → TensorProduct R S M₃)
refine_4 :
  Function.Surjective (α := TensorProduct R S M₂) (β := TensorProduct R S M₃)
    (⇑((↑R :
            {S : Type u_2} →
              {M : Type (max u_2 u_4)} →
                {M₂ : Type (max u_2 u_5)} →
                  [inst : Semiring R] →
                    [inst_21 : Semiring S] →
                      [inst_22 : AddCommMonoid M] →
                        [inst_23 : AddCommMonoid M₂] →
                          [inst_24 : Module R M] →
                            [inst_25 : Module R M₂] →
                              [inst_26 : Module S M] →
                                [inst_27 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (LinearMap.baseChange S g)) :
      (a : TensorProduct R S M₂) → TensorProduct R S M₃)
⊢ Function.Bijective (α := TensorProduct R S M₃) (β := N₃)
    (⇑(TensorProduct.lift
          ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_5 u_8)} →
                  [inst : Semiring R] →
                    [inst_21 : Semiring S] →
                      [inst_22 : AddCommMonoid M] →
                        [inst_23 : AddCommMonoid M₂] →
                          [inst_24 : Module R M] →
                            [inst_25 : Module R M₂] →
                              [inst_26 : Module S M] →
                                [inst_27 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S)
            (((LinearMap.flip (Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))) :
                  (M₃ →ₗ[R] N₃) →ₗ[S] S →ₗ[S] M₃ →ₗ[R] N₃) :
                (a : M₃ →ₗ[R] N₃) → S →ₗ[S] M₃ →ₗ[R] N₃)
              h₃))) :
      (a : TensorProduct R S M₃) → N₃)

Tactic:
refine LinearMap.bijective_of_surjective_of_bijective_of_right_exact
    ((f.baseChange S).restrictScalars R) ((g.baseChange S).restrictScalars R)
    (f'.restrictScalars R) (g'.restrictScalars R) _ _ _ ?_ ?_ ?_ exact₂ isb₁.2 isb₂ ?_ surj₂

Premises used: LinearMap.baseChange, LinearMap.restrictScalars, And.right, LinearMap.bijective_of_surjective_of_bijective_of_right_exact