-- Mathlib/Algebra/Exact.lean
/-- When we have a commutative diagram from a sequence of two maps to another,
such that the left vertical map is surjective, the middle vertical map is bijective and the right
vertical map is injective, then the upper row is exact iff the lower row is.
See `ShortComplex.exact_iff_of_epi_of_isIso_of_mono` in the file
`Algebra.Homology.ShortComplex.Exact` for the categorical version of this result. -/
lemma exact_iff_of_surjective_of_bijective_of_injective
  {M₁ M₂ M₃ N₁ N₂ N₃ : Type*} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃]
  [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃]
  (f : M₁ →+ M₂) (g : M₂ →+ M₃) (f' : N₁ →+ N₂) (g' : N₂ →+ N₃)
  (τ₁ : M₁ →+ N₁) (τ₂ : M₂ →+ N₂) (τ₃ : M₃ →+ N₃)
  (comm₁₂ : f'.comp τ₁ = τ₂.comp f)
  (comm₂₃ : g'.comp τ₂ = τ₃.comp g)
  (h₁ : Function.Surjective τ₁) (h₂ : Function.Bijective τ₂) (h₃ : Function.Injective τ₃) :
    Exact f g ↔ Exact f' g'

Proof state:
case mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f' ⇑g'
x₂ : M₂
⊢ g x₂ = 0 ↔ x₂ ∈ Set.range ⇑f

Tactic:
constructor

Result:
case mpr.mp
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f' ⇑g'
x₂ : M₂
⊢ g x₂ = 0 → x₂ ∈ Set.range ⇑f

case mpr.mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f' ⇑g'
x₂ : M₂
⊢ x₂ ∈ Set.range ⇑f → g x₂ = 0

Proof state:
case mp
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f ⇑g
y₂ : N₂
⊢ g' y₂ = 0 ↔ y₂ ∈ Set.range ⇑f'

Tactic:
obtain ⟨x₂, rfl⟩ := h₂.2 y₂

Result:
case mp.intro
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f ⇑g
x₂ : M₂
⊢ g' (τ₂ x₂) = 0 ↔ τ₂ x₂ ∈ Set.range ⇑f'

Proof state:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), (f'.comp τ₁) x = (τ₂.comp f) x
comm₂₃ : ∀ (x : M₂), (g'.comp τ₂) x = (τ₃.comp g) x
⊢ Exact ⇑f ⇑g ↔ Exact ⇑f' ⇑g'

Tactic:
dsimp at comm₁₂ comm₂₃

Result:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
⊢ Exact ⇑f ⇑g ↔ Exact ⇑f' ⇑g'

Proof state:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f ⇑g
x₂ : M₂
hx₂ : g' (τ₂ x₂) = 0
⊢ τ₃ (g x₂) = τ₃ 0

Tactic:
simpa only [map_zero, comm₂₃] using hx₂

Result:
no goals

Proof state:
case mpr.mp.intro
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f' ⇑g'
x₂ : M₂
hx₂ : g x₂ = 0
y₁ : N₁
hy₁ : f' y₁ = τ₂ x₂
⊢ x₂ ∈ Set.range ⇑f

Tactic:
obtain ⟨x₁, rfl⟩ := h₁ y₁

Result:
case mpr.mp.intro.intro
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f' ⇑g'
x₂ : M₂
hx₂ : g x₂ = 0
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ x₂ ∈ Set.range ⇑f

Proof state:
case mpr.mpr.intro
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f' ⇑g'
x₁ : M₁
⊢ g (f x₁) = 0

Tactic:
apply h₃

Result:
case mpr.mpr.intro.a
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid N₁
inst✝¹ : AddCommMonoid N₂
inst✝ : AddCommMonoid N₃
f : M₁ →+ M₂
g : M₂ →+ M₃
f' : N₁ →+ N₂
g' : N₂ →+ N₃
τ₁ : M₁ →+ N₁
τ₂ : M₂ →+ N₂
τ₃ : M₃ →+ N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : Exact ⇑f' ⇑g'
x₁ : M₁
⊢ τ₃ (g (f x₁)) = τ₃ 0