-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
R₁ R₂ : ComposableArrows.{v_1, u_1} C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂_1 : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃_1 : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
rw :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((π₂ ≫ π₁ ≫ g₁) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
rw₁ :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (π₂ ≫ (π₁ ≫ g₁) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
rw₂ :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (π₂ ≫ π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
rw₃ :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (π₂ ≫ π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11 ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
rw₄ :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (π₂ ≫ π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (f₁ ≫
          CategoryStruct.comp (Y := R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
            (R₁.map (homOfLE ⋯) :
              R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
            (φ.app (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) :
              R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
rw₅ :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (π₂ ≫ π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (π₂ ≫ f₂ ≫ φ.app (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
rw₆ :
  π₂ ≫ f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 - π₂ ≫ f₂ ≫ φ.app (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) = 0
rw₇ rw₈ : Eq.{v_1 + 1} (α := A₂ ⟶ R₂.obj ⟨2, ⋯⟩) 0 0
⊢ Eq (α := A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    ((π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)

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

Premises used: CategoryTheory.Category.assoc, sub_self, CategoryTheory.NatTrans.naturality, CategoryTheory.Preadditive.sub_comp