-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem exact_iff_epi_imageToKernel' : S.Exact ↔ Epi (imageToKernel' S.f S.g S.zero)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ Epi (imageToKernel' S.f S.g ⋯)

Tactic:
rw [S.exact_iff_epi_kernel_lift]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)

Tactic:
have : factorThruImage S.f ≫ imageToKernel' S.f S.g S.zero = kernel.lift S.g S.f S.zero := by
  simp only [← cancel_mono (kernel.ι _), kernel.lift_ι, imageToKernel',
    Category.assoc, image.fac]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯)

Tactic:
apply epi_comp

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
⊢ Epi (imageToKernel' S.f S.g ⋯) → Epi (kernel.lift S.g S.f ⋯)

Tactic:
intro

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (kernel.lift S.g S.f ⋯)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
⊢ Epi (kernel.lift S.g S.f ⋯) → Epi (imageToKernel' S.f S.g ⋯)

Tactic:
intro

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (kernel.lift S.g S.f ⋯)
⊢ Epi (imageToKernel' S.f S.g ⋯)

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (kernel.lift S.g S.f ⋯)

Tactic:
rw [← this]

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (kernel.lift S.g S.f ⋯)
⊢ Epi (imageToKernel' S.f S.g ⋯)

Tactic:
exact epi_of_epi_fac this

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯

Tactic:
simp only [← cancel_mono (kernel.ι _), kernel.lift_ι, imageToKernel',
  Category.assoc, image.fac]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
⊢ Epi (kernel.lift S.g S.f ⋯) → Epi (imageToKernel' S.f S.g ⋯)

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
⊢ Epi (imageToKernel' S.f S.g ⋯) → Epi (kernel.lift S.g S.f ⋯)