-- Mathlib/RingTheory/Flat/Basic.lean
/-- If `M` is flat then `M ⊗ -` is an exact functor. -/
lemma lTensor_exact [Flat R M] ⦃N N' N'' : Type*⦄
    [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [Module R N] [Module R N'] [Module R N'']
    ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄ (exact : Function.Exact f g) :
    Function.Exact (f.lTensor M) (g.lTensor M)

Proof state:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)
exact1 : Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
⊢ Function.Injective ⇑ι

Tactic:
simpa [ι, - Subtype.val_injective] using Subtype.val_injective

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
let ι : N' ⧸ LinearMap.range f →ₗ[R] N'' :=
  Submodule.subtype _ ∘ₗ (LinearMap.quotKerEquivRange g).toLinearMap ∘ₗ
    Submodule.quotEquivOfEq (LinearMap.range f) (LinearMap.ker g)
      (LinearMap.exact_iff.mp exact).symm

Result:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Proof state:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
let π : N' →ₗ[R] N' ⧸ LinearMap.range f := Submodule.mkQ _

Result:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Proof state:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
suffices exact1 : Function.Exact (f.lTensor M) (π.lTensor M) by
  rw [show g = ι.comp π from rfl, lTensor_comp]
  exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
    simpa [ι, - Subtype.val_injective] using Subtype.val_injective) (map_zero _)

Result:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)

Proof state:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)
x : N'
⊢ π x = 0 ↔ x ∈ Set.range ⇑f

Tactic:
simp [π]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)
exact1 : Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
rw [show g = ι.comp π from rfl, lTensor_comp]

Result:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)
exact1 : Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M ι ∘ₗ lTensor M π)

Proof state:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)

Tactic:
exact _root_.lTensor_exact _ (fun x ↦ by simp [π]) Quotient.mk''_surjective

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ
ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)
exact1 : Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M ι ∘ₗ lTensor M π)

Tactic:
exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
  simpa [ι, - Subtype.val_injective] using Subtype.val_injective) (map_zero _)

Result:
no goals