-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
theorem epi_of_epi_of_epi_of_mono'
    (hR₁ : (mk₂ (R₁.map' 1 2) (R₁.map' 2 3)).Exact)
    (hR₂ : (mk₂ (R₂.map' 0 1) (R₂.map' 1 2)).Exact) (hR₂' : R₂.map' 1 3 = 0)
    (h₀ : Epi (app' φ 0)) (h₂ : Epi (app' φ 2)) (h₃ : Mono (app' φ 3)) :
    Epi (app' φ 1)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂ : Epi (app' φ 2 ⋯)
h₃ : Mono (app' φ 3 ⋯)
⊢ ∀ ⦃A : C⦄ (y : A ⟶ R₂.obj' 1 ⋯), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ app' φ 1 ⋯

Tactic:
intro A g₁

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂ : Epi (app' φ 2 ⋯)
h₃ : Mono (app' φ 3 ⋯)
A : C
g₁ : A ⟶ R₂.obj' 1 ⋯
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂✝ : Epi (app' φ 2 ⋯)
h₃✝ : Mono (app' φ 3 ⋯)
A : C
g₁ : A ⟶ R₂.obj' 1 ⋯
A₁ : C
π₁ : A₁ ⟶ A
w✝³ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 ⋯
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝² : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0
A₃ : C
π₃ : A₃ ⟶ A₂
w✝¹ : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w✝ : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 ⋯
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 ⋯
⊢ (π₄ ≫ π₃ ≫ π₂ ≫ π₁) ≫ g₁ = (π₄ ≫ π₃ ≫ f₁ + f₀ ≫ R₁.map' 0 1 ⋯ ⋯) ≫ app' φ 1 ⋯

Tactic:
rw [assoc, assoc, assoc, add_comp, assoc, assoc, assoc, NatTrans.naturality,
  ← reassoc_of% h₆, ← h₅, comp_sub]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂✝ : Epi (app' φ 2 ⋯)
h₃✝ : Mono (app' φ 3 ⋯)
A : C
g₁ : A ⟶ R₂.obj' 1 ⋯
A₁ : C
π₁ : A₁ ⟶ A
w✝³ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 ⋯
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝² : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0
A₃ : C
π₃ : A₃ ⟶ A₂
w✝¹ : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w✝ : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 ⋯
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 ⋯
⊢ π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ f₁ ≫ app' φ 1 ⋯ + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂ : Epi (app' φ 2 ⋯)
h₃ : Mono (app' φ 3 ⋯)
⊢ Epi (app' φ 1 ⋯)

Tactic:
rw [epi_iff_surjective_up_to_refinements]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂ : Epi (app' φ 2 ⋯)
h₃ : Mono (app' φ 3 ⋯)
⊢ ∀ ⦃A : C⦄ (y : A ⟶ R₂.obj' 1 ⋯), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ app' φ 1 ⋯

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂✝ : Epi (app' φ 2 ⋯)
h₃✝ : Mono (app' φ 3 ⋯)
A : C
g₁ : A ⟶ R₂.obj' 1 ⋯
A₁ : C
π₁ : A₁ ⟶ A
w✝³ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 ⋯
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝² : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0
A₃ : C
π₃ : A₃ ⟶ A₂
w✝¹ : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w✝ : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 ⋯
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 ⋯
⊢ π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)

Tactic:
rw [add_sub_cancel]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂✝ : Epi (app' φ 2 ⋯)
h₃✝ : Mono (app' φ 3 ⋯)
A : C
g₁ : A ⟶ R₂.obj' 1 ⋯
A₁ : C
π₁ : A₁ ⟶ A
w✝³ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 ⋯
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝² : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0
A₃ : C
π₃ : A₃ ⟶ A₂
w✝¹ : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w✝ : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 ⋯
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 ⋯
⊢ R₁.obj' 0 ⋯ ⟶ R₁.obj 1

Tactic:
exact R₁.map' 0 1

Result:
no goals

Proof state:
case intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂ : Epi (app' φ 2 ⋯)
h₃ : Mono (app' φ 3 ⋯)
A : C
g₁ : A ⟶ R₂.obj' 1 ⋯
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 ⋯
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯

Tactic:
have h₂ : f₂ ≫ R₁.map' 2 3 = 0 := by
  rw [← cancel_mono (app' φ 3 _), assoc, zero_comp, NatTrans.naturality, ← reassoc_of% h₁,
    ← R₂.map'_comp 1 2 3, hR₂', comp_zero, comp_zero]

Result:
case intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0
h₀ : Epi (app' φ 0 ⋯)
h₂✝ : Epi (app' φ 2 ⋯)
h₃ : Mono (app' φ 3 ⋯)
A : C
g₁ : A ⟶ R₂.obj' 1 ⋯
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 ⋯
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯