-- 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₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Mono (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
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 ⋯) ⋯ ⋯ ⋯
⊢ Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
have refine : {
    X₁ :=
      (mk₂
            ((mk₃ 0 (R₂.map' 0 1 sorry sorry) (R₂.map' 1 2 sorry sorry)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
              mono_of_epi_of_mono_of_mono'._proof_11)
            ((mk₃ 0 (R₂.map' 0 1 sorry sorry) (R₂.map' 1 2 sorry sorry)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
              mono_of_epi_of_mono_of_mono'._proof_4)).obj
        ⟨0, sorry⟩,
    X₂ :=
      (mk₂
            ((mk₃ 0 (R₂.map' 0 1 sorry sorry) (R₂.map' 1 2 sorry sorry)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
              mono_of_epi_of_mono_of_mono'._proof_11)
            ((mk₃ 0 (R₂.map' 0 1 sorry sorry) (R₂.map' 1 2 sorry sorry)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
              mono_of_epi_of_mono_of_mono'._proof_4)).obj
        ⟨1, sorry⟩,
    X₃ :=
      (mk₂
            ((mk₃ 0 (R₂.map' 0 1 sorry sorry) (R₂.map' 1 2 sorry sorry)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
              mono_of_epi_of_mono_of_mono'._proof_11)
            ((mk₃ 0 (R₂.map' 0 1 sorry sorry) (R₂.map' 1 2 sorry sorry)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
              mono_of_epi_of_mono_of_mono'._proof_4)).obj
        ⟨2, sorry⟩,
    f :=
      (mk₂
            ((mk₃ (X₀ := R₁.obj' 0 sorry) (X₁ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
                  R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                  (0 : R₁.obj' 0 sorry ⟶ R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                  (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)))).map'
              0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
            ((mk₃ (X₀ := R₁.obj' 0 sorry) (X₁ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
                  R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                  (0 : R₁.obj' 0 sorry ⟶ R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                  (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)))).map'
              1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).map'
        0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
    g :=
      (mk₂
            ((mk₃ (X₀ := R₁.obj' 0 sorry) (X₁ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
                  R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                  (0 : R₁.obj' 0 sorry ⟶ R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                  (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)))).map'
              0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
            ((mk₃ (X₀ := R₁.obj' 0 sorry) (X₁ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
                  R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                  (0 : R₁.obj' 0 sorry ⟶ R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
                  (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)))).map'
              1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).map'
        1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
    zero := sorry : ShortComplex.{v_1, u_1} C }.Exact
Tactic: refine mono_of_epi_of_mono_of_mono' ψ (by simp)
    (hR₁.exact 0).exact_toComposableArrows
    (exact₂_mk _ (by simp) ?_) (by dsimp [ψ]; infer_instance) h₀ h₁