-- 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₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (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₃ := 0) (X₄ := 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 0 ⟶
  mk₄ (X₀ := R₂.obj ⟨0, ⋯⟩) (X₁ := R₂.obj ⟨1, ⋯⟩) (X₃ := 0) (X₄ := 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 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (X₀ := R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
      (X₃ := 0) (X₄ := 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 0).Exact
have refine_2 : (mk₂ (X₀ :=
    (mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (X₃ := 0) (X₄ := 0)
            (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 0).δ₀.obj
      (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
    (X₁ :=
    (mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (X₃ := 0) (X₄ := 0)
            (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 0).δ₀.obj
      (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
    (X₂ :=
    (mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (X₃ := 0) (X₄ := 0)
            (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 0).δ₀.obj
      (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
    ((mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (X₃ := 0) (X₄ := 0)
              (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 0).δ₀.map'
        0 1 isComplex₂_iff._proof_2 sorry :
      (mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                (X₃ := 0) (X₄ := 0)
                (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 0).δ₀.obj
          (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
        (mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ :=
                R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₃ := 0) (X₄ := 0)
                (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 0).δ₀.obj
          (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
    ((mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (X₃ := 0) (X₄ := 0)
              (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 0).δ₀.map'
        1 2 isComplex₂_iff._proof_4 sorry :
      (mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                (X₃ := 0) (X₄ := 0)
                (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 0).δ₀.obj
          (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
        (mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ :=
                R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₃ := 0) (X₄ := 0)
                (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 0).δ₀.obj
          (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).Exact
Tactic: refine exact_of_δ₀ (hR₂.exact 0).exact_toComposableArrows (exact_of_δ₀ ?_ ?_)