-- 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
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₂ = 0

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

Result:
case h
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
⊢ f₂ = 0

Proof state:
case h.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₁ : 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
A₃ : C
π₃ : A₃ ⟶ A₂
w✝ : Epi π₃
f₀ : A₃ ⟶ R₁.obj' 0 ⋯
hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 ⋯
h₄ : f₀ ≫ R₁.map' 0 1 ⋯ ⋯ = π₃ ≫ π₂ ≫ f₁
⊢ f₂ = 0

Tactic:
rw [← cancel_epi π₁, comp_zero, hf₁, ← cancel_epi π₂, ← cancel_epi π₃, comp_zero,
  comp_zero, ← reassoc_of% h₄, ← R₁.map'_comp 0 1 2, hR₁, comp_zero]

Result:
no goals

Proof state:
case h
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 ⋯)
⊢ ∀ {P : C} (g : P ⟶ R₁.obj' 2 ⋯), g ≫ app' φ 2 ⋯ = 0 → g = 0

Tactic:
intro A f₂ h₁

Result:
case h
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₂ = 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 ⋯)
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
A₃ : C
π₃ : A₃ ⟶ A₂
w✝ : Epi π₃
f₀ : A₃ ⟶ R₁.obj' 0 ⋯
hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 ⋯
⊢ f₀ ≫ R₁.map' 0 1 ⋯ ⋯ = π₃ ≫ π₂ ≫ f₁

Tactic:
rw [← cancel_mono (app' φ 1 _), assoc, assoc, assoc, NatTrans.naturality,
  ← reassoc_of% hf₀, hg₀]

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

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

Tactic:
rfl

Result:
no goals