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

Proof state:
case h.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₁ : R₁.map' 0 2 ⋯ ⋯ = 0
hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
h₀ : Epi (app' φ 0 ⋯)
h₁✝ : Mono (app' φ 1 ⋯)
h₃✝ : Mono (app' φ 3 ⋯)
A : C
f₂ : A ⟶ R₁.obj' 2 ⋯
h₁ : f₂ ≫ app' φ 2 ⋯ = 0
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₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₃ : (f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0
⊢ f₂ = 0

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

Result:
case h.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₁ : R₁.map' 0 2 ⋯ ⋯ = 0
hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
h₀ : Epi (app' φ 0 ⋯)
h₁✝ : Mono (app' φ 1 ⋯)
h₃✝ : Mono (app' φ 3 ⋯)
A : C
f₂ : A ⟶ R₁.obj' 2 ⋯
h₁ : f₂ ≫ app' φ 2 ⋯ = 0
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₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₃ : (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₁
hg₀ : π₂ ≫ f₁ ≫ app' φ 1 ⋯ = g₀ ≫ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).f
⊢ f₂ = 0

Proof state:
case h.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₁ : R₁.map' 0 2 ⋯ ⋯ = 0
hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
h₀ : Epi (app' φ 0 ⋯)
h₁✝ : Mono (app' φ 1 ⋯)
h₃ : Mono (app' φ 3 ⋯)
A : C
f₂ : A ⟶ R₁.obj' 2 ⋯
h₁ : f₂ ≫ app' φ 2 ⋯ = 0
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₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).f
⊢ f₂ = 0

Tactic:
dsimp at hf₁

Result:
case h.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₁ : R₁.map' 0 2 ⋯ ⋯ = 0
hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
h₀ : Epi (app' φ 0 ⋯)
h₁✝ : Mono (app' φ 1 ⋯)
h₃ : Mono (app' φ 3 ⋯)
A : C
f₂ : A ⟶ R₁.obj' 2 ⋯
h₁ : f₂ ≫ app' φ 2 ⋯ = 0
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₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
⊢ f₂ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0
hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
h₀ : Epi (app' φ 0 ⋯)
h₁✝ : Mono (app' φ 1 ⋯)
h₃ : Mono (app' φ 3 ⋯)
A : C
f₂ : A ⟶ R₁.obj' 2 ⋯
h₁ : f₂ ≫ app' φ 2 ⋯ = 0
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₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
⊢ (f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0

Tactic:
rw [assoc, ← NatTrans.naturality, ← reassoc_of% hf₁, h₁, comp_zero]

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₁ : R₁.map' 0 2 ⋯ ⋯ = 0
hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact
hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact
h₀ : Epi (app' φ 0 ⋯)
h₁✝ : Mono (app' φ 1 ⋯)
h₃ : Mono (app' φ 3 ⋯)
A : C
f₂ : A ⟶ R₁.obj' 2 ⋯
h₁ : f₂ ≫ app' φ 2 ⋯ = 0
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0

Tactic:
rw [← cancel_mono (app' φ 3 _), assoc, NatTrans.naturality, reassoc_of% h₁,
  zero_comp, zero_comp]

Result:
no goals