-- 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:
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₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ τ₂ (f x₁) = τ₂ x₂

Tactic:
simpa only [comm₁₂] using hy₁

Result:
no goals

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₃
comm₁₂ : f'.comp τ₁ = τ₂.comp f
comm₂₃ : g'.comp τ₂ = τ₃.comp g
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
⊢ Exact ⇑f ⇑g ↔ Exact ⇑f' ⇑g'

Tactic:
replace comm₁₂ := DFunLike.congr_fun 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₃
comm₂₃ : g'.comp τ₂ = τ₃.comp g
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), (f'.comp τ₁) x = (τ₂.comp f) x
⊢ Exact ⇑f ⇑g ↔ Exact ⇑f' ⇑g'

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)
⊢ Exact ⇑f ⇑g → Exact ⇑f' ⇑g'

Tactic:
intro h y₂

Result:
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'

Proof state:
case mp.intro.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₂
hx₂ : g' (τ₂ x₂) = 0
⊢ τ₂ x₂ ∈ Set.range ⇑f'

Tactic:
obtain ⟨x₁, rfl⟩ := (h x₂).1 (h₃ (by simpa only [map_zero, comm₂₃] using hx₂))

Result:
case mp.intro.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' (τ₂ (f x₁)) = 0
⊢ τ₂ (f x₁) ∈ Set.range ⇑f'

Proof state:
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₂
hx₂ : g x₂ = 0
⊢ x₂ ∈ Set.range ⇑f

Tactic:
obtain ⟨y₁, hy₁⟩ := (h (τ₂ x₂)).1 (by simp only [comm₂₃, hx₂, map_zero])

Result:
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

Proof state:
case mp.intro.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

Tactic:
rintro ⟨y₁, hy₁⟩

Result:
case mp.intro.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₂
y₁ : N₁
hy₁ : f' y₁ = τ₂ x₂
⊢ g' (τ₂ x₂) = 0