-- Mathlib/Algebra/Homology/ShortComplex/Ab.lean
lemma ab_exact_iff :
    S.Exact ↔ ∀ (x₂ : S.X₂) (_ : S.g x₂ = 0), ∃ (x₁ : S.X₁), S.f x₁ = x₂

Proof state:
S : ShortComplex Ab
h : Function.Surjective ⇑S.abToCycles
x₂ : ↑S.X₂
hx₂ : (ConcreteCategory.hom S.g) x₂ = 0
x₁ : ↑S.X₁
hx₁ : S.abToCycles x₁ = ⟨x₂, hx₂⟩
⊢ (ConcreteCategory.hom S.f) x₁ = x₂

Tactic:
simpa only [Subtype.ext_iff, abToCycles_apply_coe] using hx₁

Result:
no goals

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

Tactic:
rw [exact_iff_surjective_abToCycles]

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

Proof state:
case mp.intro
S : ShortComplex Ab
h : Function.Surjective ⇑S.abToCycles
x₂ : ↑S.X₂
hx₂ : (ConcreteCategory.hom S.g) x₂ = 0
x₁ : ↑S.X₁
hx₁ : S.abToCycles x₁ = ⟨x₂, hx₂⟩
⊢ ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

Tactic:
exact ⟨x₁, by simpa only [Subtype.ext_iff, abToCycles_apply_coe] using hx₁⟩

Result:
no goals

Proof state:
case mpr.mk
S : ShortComplex Ab
h : ∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
x₂ : ↑S.X₂
hx₂ : x₂ ∈ (AddCommGrp.Hom.hom S.g).ker
⊢ ∃ a, S.abToCycles a = ⟨x₂, hx₂⟩

Tactic:
obtain ⟨x₁, rfl⟩ := h x₂ hx₂

Result:
case mpr.mk.intro
S : ShortComplex Ab
h : ∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
x₁ : ↑S.X₁
hx₂ : (ConcreteCategory.hom S.f) x₁ ∈ (AddCommGrp.Hom.hom S.g).ker
⊢ ∃ a, S.abToCycles a = ⟨(ConcreteCategory.hom S.f) x₁, hx₂⟩

Proof state:
case mpr.mk.intro
S : ShortComplex Ab
h : ∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
x₁ : ↑S.X₁
hx₂ : (ConcreteCategory.hom S.f) x₁ ∈ (AddCommGrp.Hom.hom S.g).ker
⊢ ∃ a, S.abToCycles a = ⟨(ConcreteCategory.hom S.f) x₁, hx₂⟩

Tactic:
exact ⟨x₁, rfl⟩

Result:
no goals

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

Tactic:
intro h x₂ hx₂

Result:
case mp
S : ShortComplex Ab
h : Function.Surjective ⇑S.abToCycles
x₂ : ↑S.X₂
hx₂ : (ConcreteCategory.hom S.g) x₂ = 0
⊢ ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

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

Tactic:
rintro h ⟨x₂, hx₂⟩

Result:
case mpr.mk
S : ShortComplex Ab
h : ∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
x₂ : ↑S.X₂
hx₂ : x₂ ∈ (AddCommGrp.Hom.hom S.g).ker
⊢ ∃ a, S.abToCycles a = ⟨x₂, hx₂⟩

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

Tactic:
constructor

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

case mpr
S : ShortComplex Ab
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) →
    Function.Surjective ⇑S.abToCycles

Proof state:
case mp
S : ShortComplex Ab
h : Function.Surjective ⇑S.abToCycles
x₂ : ↑S.X₂
hx₂ : (ConcreteCategory.hom S.g) x₂ = 0
⊢ ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

Tactic:
obtain ⟨x₁, hx₁⟩ := h ⟨x₂, hx₂⟩

Result:
case mp.intro
S : ShortComplex Ab
h : Function.Surjective ⇑S.abToCycles
x₂ : ↑S.X₂
hx₂ : (ConcreteCategory.hom S.g) x₂ = 0
x₁ : ↑S.X₁
hx₁ : S.abToCycles x₁ = ⟨x₂, hx₂⟩
⊢ ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂