-- Mathlib/CategoryTheory/Abelian/Refinements.lean
lemma ShortComplex.exact_iff_exact_up_to_refinements :
    S.Exact ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂) (_ : x₂ ≫ S.g = 0),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f

Proof state:
case mp.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ S.liftCycles a ha = x₁ ≫ S.toCycles
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ a = x₁ ≫ S.f

Tactic:
exact ⟨A', π, hπ, x₁, by simpa only [assoc, liftCycles_i, toCycles_i] using fac =≫ S.iCycles⟩

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles

Tactic:
intro hS A a

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ a = x ≫ S.toCycles

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ S.liftCycles a ha = x₁ ≫ S.toCycles
⊢ π ≫ a = x₁ ≫ S.f

Tactic:
simpa only [assoc, liftCycles_i, toCycles_i] using fac =≫ S.iCycles

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ a = x ≫ S.toCycles

Tactic:
obtain ⟨A', π, hπ, x₁, fac⟩ := hS (a ≫ S.iCycles) (by simp)

Result:
case mpr.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ a ≫ S.iCycles = x₁ ≫ S.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ a = x ≫ S.toCycles

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles) →
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
intro hS A a ha

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ a = x₁ ≫ S.f

Proof state:
case mpr.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ a ≫ S.iCycles = x₁ ≫ S.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ a = x ≫ S.toCycles

Tactic:
exact ⟨A', π, hπ, x₁, by simp only [← cancel_mono S.iCycles, assoc, toCycles_i, fac]⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
rw [S.exact_iff_epi_toCycles, epi_iff_surjective_up_to_refinements]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles) →
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
⊢ (a ≫ S.iCycles) ≫ S.g = 0

Tactic:
simp

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ a = x₁ ≫ S.f

Tactic:
obtain ⟨A', π, hπ, x₁, fac⟩ := hS (S.liftCycles a ha)

Result:
case mp.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ S.liftCycles a ha = x₁ ≫ S.toCycles
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ a = x₁ ≫ S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ a ≫ S.iCycles = x₁ ≫ S.f
⊢ π ≫ a = x₁ ≫ S.toCycles

Tactic:
simp only [← cancel_mono S.iCycles, assoc, toCycles_i, fac]

Result:
no goals