-- Mathlib/Algebra/Homology/ShortComplex/Ab.lean
lemma ab_exact_iff_range_eq_ker : S.Exact ↔ S.f.hom.range = S.g.hom.ker

Proof state:
S : ShortComplex Ab
⊢ (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range ↔
    (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker

Tactic:
constructor

Result:
case mp
S : ShortComplex Ab
⊢ (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range →
    (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker

case mpr
S : ShortComplex Ab
⊢ (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker →
    (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range

Proof state:
case mp
S : ShortComplex Ab
⊢ (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range →
    (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker

Tactic:
intro h

Result:
case mp
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range
⊢ (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker

Proof state:
S : ShortComplex Ab
⊢ S.Exact ↔ (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker

Tactic:
rw [ab_exact_iff_ker_le_range]

Result:
S : ShortComplex Ab
⊢ (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range ↔
    (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker

Proof state:
case mp.intro
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range
x₁ : ↑S.X₁
⊢ (ConcreteCategory.hom 0) x₁ = 0

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker
⊢ (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range

Tactic:
rw [h]

Result:
no goals

Proof state:
case mp
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range
⊢ (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker

Tactic:
refine le_antisymm ?_ h

Result:
case mp
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range
⊢ (AddCommGrp.Hom.hom S.f).range ≤ (AddCommGrp.Hom.hom S.g).ker

Proof state:
case mp
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range
⊢ (AddCommGrp.Hom.hom S.f).range ≤ (AddCommGrp.Hom.hom S.g).ker

Tactic:
rintro _ ⟨x₁, rfl⟩

Result:
case mp.intro
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range
x₁ : ↑S.X₁
⊢ (AddCommGrp.Hom.hom S.f) x₁ ∈ (AddCommGrp.Hom.hom S.g).ker

Proof state:
case mp.intro
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range
x₁ : ↑S.X₁
⊢ (AddCommGrp.Hom.hom S.f) x₁ ∈ (AddCommGrp.Hom.hom S.g).ker

Tactic:
rw [AddMonoidHom.mem_ker, ← ConcreteCategory.comp_apply, S.zero]

Result:
case mp.intro
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range
x₁ : ↑S.X₁
⊢ (ConcreteCategory.hom 0) x₁ = 0

Proof state:
case mpr
S : ShortComplex Ab
⊢ (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker →
    (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range

Tactic:
intro h

Result:
case mpr
S : ShortComplex Ab
h : (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker
⊢ (AddCommGrp.Hom.hom S.g).ker ≤ (AddCommGrp.Hom.hom S.f).range