-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
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₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₃ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (X₃ := R₁.obj' 0 ⋯)
    (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)))
    0 ⟶
  mk₃ (X₀ := R₂.obj ⟨0, ⋯⟩) (X₁ := R₂.obj ⟨1, ⋯⟩) (X₃ := 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, ⋯⟩) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯)
    (𝟙
      ((mk₃ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ :=
            R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₃ := R₁.obj' 0 ⋯)
            (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)))
            0).obj'
        3 _proof_300✝))
    ⋯ ⋯ ⋯
⊢ (mk₃ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
          (X₃ := R₁.obj' 0 ⋯)
          (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)))
          0).map'
      0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 =
    0
have refine_1 : Eq (α :=
  R₁.obj 0 ⟶
    Precomp.obj
      (mk₂ (X₀ := R₁.obj 1) (X₁ := R₁.obj 2) (X₂ := R₁.obj 0) (R₁.map (homOfLE sorry) : R₁.obj 1 ⟶ R₁.obj 2)
        (0 : R₁.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj' 0 sorry))
      (R₁.obj 0) 2)
  (CategoryStruct.comp (Y := R₁.obj 1) (R₁.map (homOfLE sorry) : R₁.obj 0 ⟶ R₁.obj 1)
      (R₁.map (homOfLE sorry) : R₁.obj 1 ⟶ R₁.obj 2) :
    R₁.obj 0 ⟶
      Precomp.obj
        (mk₂ (X₀ := R₁.obj 1) (X₁ := R₁.obj 2) (X₂ := R₁.obj 0) (R₁.map (homOfLE sorry) : R₁.obj 1 ⟶ R₁.obj 2)
          (0 : R₁.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj' 0 sorry))
        (R₁.obj 0) 2)
  (0 :
    (mk₃ (X₀ := R₁.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (X₃ := R₁.obj' 0 sorry)
            (R₁.map' 0 1 sorry sorry :
              R₁.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 1 2 sorry sorry :
              R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            0).obj
        (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶
      (mk₃ (X₀ := R₁.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (X₃ := R₁.obj' 0 sorry)
            (R₁.map' 0 1 sorry sorry :
              R₁.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 1 2 sorry sorry :
              R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            0).obj
        ⟨2, sorry⟩)
Tactic: dsimp