-- 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
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 ⋯)
⊢ (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0

Tactic:
rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]

Result:
no goals

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

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

Tactic:
obtain ⟨A₃, π₃, _, g₀, h₅⟩ := (hR₂.exact 0).exact_up_to_refinements _ 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₃ ⟶ ((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 ⋯

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

Tactic:
obtain ⟨A₁, π₁, _, f₂, h₁⟩ :=
  surjective_up_to_refinements_of_epi (app' φ 2 _) (g₁ ≫ R₂.map' 1 2)

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

Tactic:
have h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 _) ≫ R₂.map' 1 2 = 0 := by
  rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]

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