-- 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:
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:
dsimp

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:
case 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₂ ⟶ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁
h₃ : π₂ ≫ f₂ = f₁ ≫ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯

Tactic:
dsimp at f₁ h₃

Result:
case 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 ⋯)
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯

Proof state:
case 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₃ ⟶ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁
h₅ : π₃ ≫ (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) = g₀ ≫ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯

Tactic:
dsimp at g₀ h₅

Result:
case 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' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ 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
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 ⋯
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0

Tactic:
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:
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 ⋯
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯

Tactic:
obtain ⟨A₂, π₂, _, f₁, h₃⟩ := (hR₁.exact 0).exact_up_to_refinements _ h₂

Result:
case 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₂ ⟶ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁
h₃ : π₂ ≫ f₂ = f₁ ≫ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 ⋯