-- Mathlib/Algebra/Homology/ShortComplex/Ab.lean
lemma ab_exact_iff_function_exact :
    S.Exact ↔ Function.Exact S.f S.g

Proof state:
case h
S : ShortComplex Ab
⊢ ∀ (a : ↑S.X₂),
    ((ConcreteCategory.hom S.g) a = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = a) ↔
      ((ConcreteCategory.hom S.g) a = 0 ↔ a ∈ Set.range ⇑(ConcreteCategory.hom S.f))

Tactic:
intro x₂

Result:
case h
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) ↔
    ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f))

Proof state:
case h.mp
S : ShortComplex Ab
x₂ : ↑S.X₂
h : (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
⊢ (ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f)

Tactic:
refine ⟨h, ?_⟩

Result:
case h.mp
S : ShortComplex Ab
x₂ : ↑S.X₂
h : (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
⊢ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f) → (ConcreteCategory.hom S.g) x₂ = 0

Proof state:
case h.mp
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) →
    ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f))

Tactic:
intro h

Result:
case h.mp
S : ShortComplex Ab
x₂ : ↑S.X₂
h : (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
⊢ (ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f)

Proof state:
case h.mp
S : ShortComplex Ab
x₂ : ↑S.X₂
h : (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
⊢ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f) → (ConcreteCategory.hom S.g) x₂ = 0

Tactic:
rintro ⟨x₁, rfl⟩

Result:
case h.mp.intro
S : ShortComplex Ab
x₁ : ↑S.X₁
h :
  (ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x₁) = 0 →
    ∃ x₁_1, (ConcreteCategory.hom S.f) x₁_1 = (ConcreteCategory.hom S.f) x₁
⊢ (ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x₁) = 0

Proof state:
case h
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) ↔
    ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f))

Tactic:
constructor

Result:
case h.mp
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) →
    ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f))

case h.mpr
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f)) →
    (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

Proof state:
case h.mpr
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f)) →
    (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

Tactic:
tauto

Result:
no goals

Proof state:
S : ShortComplex Ab
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) ↔
    Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
apply forall_congr'

Result:
case h
S : ShortComplex Ab
⊢ ∀ (a : ↑S.X₂),
    ((ConcreteCategory.hom S.g) a = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = a) ↔
      ((ConcreteCategory.hom S.g) a = 0 ↔ a ∈ Set.range ⇑(ConcreteCategory.hom S.f))

Proof state:
S : ShortComplex Ab
⊢ S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
rw [S.ab_exact_iff]

Result:
S : ShortComplex Ab
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) ↔
    Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Proof state:
case h.mp.intro
S : ShortComplex Ab
x₁ : ↑S.X₁
h :
  (ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x₁) = 0 →
    ∃ x₁_1, (ConcreteCategory.hom S.f) x₁_1 = (ConcreteCategory.hom S.f) x₁
⊢ (ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x₁) = 0

Tactic:
simp only [ab_zero_apply]

Result:
no goals