Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact

Goal state before:
pp: case refine_1
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : 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✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : 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 f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ ↑R f' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)) =
    TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)) ∘ₗ
      ↑R (LinearMap.baseChange S f)

pp: case refine_2
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : 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✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : 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 f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ ↑R g' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)) =
    TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))).flip h₃)) ∘ₗ
      ↑R (LinearMap.baseChange S g)

pp: case refine_3
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : 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✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : 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 f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ Function.Exact ⇑(↑R (LinearMap.baseChange S f)) ⇑(↑R (LinearMap.baseChange S g))

pp: case refine_4
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : 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✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : 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 f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ Function.Surjective ⇑(↑R (LinearMap.baseChange S g))

Tactic:
· ext s m
    simpa using congr(s • ($comm₁ m)).symm

Goal state after:
case refine_2
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : 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✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : 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 f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ ↑R g' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)) =
    TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))).flip h₃)) ∘ₗ
      ↑R (LinearMap.baseChange S g)

case refine_3
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : 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✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : 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 f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ Function.Exact ⇑(↑R (LinearMap.baseChange S f)) ⇑(↑R (LinearMap.baseChange S g))

case refine_4
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : 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✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : 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 f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ Function.Surjective ⇑(↑R (LinearMap.baseChange S g))