-- 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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
    R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (0 : R₁.obj' 0 ⋯ ⟶ R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 0 1 ⋯ ⋯ : R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 1 2 ⋯ ⋯ :
      R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) ⟶
  mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₂.obj ⟨0, ⋯⟩) (X₂ := R₂.obj ⟨1, ⋯⟩) (0 : R₁.obj' 0 ⋯ ⟶ R₂.obj ⟨0, ⋯⟩)
    (R₂.map' 0 1 ⋯ ⋯ : R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨1, ⋯⟩)
    (R₂.map' 1 2 ⋯ ⋯ : R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨2, ⋯⟩) :=
  homMk₃
    (𝟙
      ((mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
            R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (0 : R₁.obj' 0 ⋯ ⟶ R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 0 1 ⋯ ⋯ :
              R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 1 2 ⋯ ⋯ :
              R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))).obj'
        0 _proof_297✝))
    (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯
refine_2 :
  Eq (α :=
    R₂.obj 0 ⟶
      Precomp.obj
        (mk₂ (X₀ := R₂.obj 0) (X₁ := R₂.obj 1) (X₂ := R₂.obj 2) (R₂.map (homOfLE ⋯) : R₂.obj 0 ⟶ R₂.obj 1)
          (R₂.map (homOfLE ⋯) : R₂.obj 1 ⟶ R₂.obj 2))
        (R₁.obj 0) 3)
    (R₂.map
        (CategoryStruct.comp (Y := 1) (homOfLE ⋯ : Quiver.Hom (V := Fin 3) 0 1)
          (homOfLE ⋯ : Quiver.Hom (V := Fin 3) 1 2)) :
      R₂.obj 0 ⟶ R₂.obj 2)
    (0 :
      (mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
              R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (0 : R₁.obj' 0 ⋯ ⟶ R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (R₂.map' 0 1 ⋯ ⋯ :
                R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (R₂.map' 1 2 ⋯ ⋯ :
                R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))).obj
          (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶
        (mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
              R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (0 : R₁.obj' 0 ⋯ ⟶ R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (R₂.map' 0 1 ⋯ ⋯ :
                R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (R₂.map' 1 2 ⋯ ⋯ :
                R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))).obj
          ⟨3, ⋯⟩)
⊢ Eq (α :=
    R₂.obj 0 ⟶
      Precomp.obj
        (mk₂ (X₀ := R₂.obj 0) (X₁ := R₂.obj 1) (X₂ := R₂.obj 2) (R₂.map (homOfLE ⋯) : R₂.obj 0 ⟶ R₂.obj 1)
          (R₂.map (homOfLE ⋯) : R₂.obj 1 ⟶ R₂.obj 2))
        (R₁.obj 0) 3)
    (CategoryStruct.comp (Y := R₂.obj 1) (R₂.map (homOfLE ⋯) : R₂.obj 0 ⟶ R₂.obj 1)
        (R₂.map (homOfLE ⋯) : R₂.obj 1 ⟶ R₂.obj 2) :
      R₂.obj 0 ⟶
        Precomp.obj (mk₁ (X₀ := R₂.obj 1) (X₁ := R₂.obj 2) (R₂.map (homOfLE ⋯) : R₂.obj 1 ⟶ R₂.obj 2)) (R₂.obj 0) 2)
    (0 :
      (mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
              R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (0 : R₁.obj' 0 ⋯ ⟶ R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (R₂.map' 0 1 ⋯ ⋯ :
                R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (R₂.map' 1 2 ⋯ ⋯ :
                R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))).obj
          (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶
        (mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
              R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (0 : R₁.obj' 0 ⋯ ⟶ R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (R₂.map' 0 1 ⋯ ⋯ :
                R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (R₂.map' 1 2 ⋯ ⋯ :
                R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))).obj
          ⟨3, ⋯⟩)

Tactic:
rw [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp