-- 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₂.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 ⋯ ⋯ ⋯ ⋯
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  Epi
    {
        X₁ :=
          (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
            ⟨0, ⋯⟩,
        X₂ :=
          (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
            ⟨1, ⋯⟩,
        X₃ :=
          (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
            ⟨2, ⋯⟩,
        f :=
          (mk₂ (X₀ :=
                (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).δ₀.obj
                  (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
                (X₁ :=
                (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).δ₀.obj
                  (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
                (X₂ :=
                (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).δ₀.obj
                  (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
                ((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).δ₀.map'
                    0 1 isComplex₂_iff._proof_2 ⋯ :
                  (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).δ₀.obj
                      (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
                    (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).δ₀.obj
                      (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
                ((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).δ₀.map'
                    1 2 isComplex₂_iff._proof_4 ⋯ :
                  (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).δ₀.obj
                      (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
                    (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).δ₀.obj
                      (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).map'
            0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
        g :=
          (mk₂ (X₀ :=
                (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).δ₀.obj
                  (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
                (X₁ :=
                (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).δ₀.obj
                  (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
                (X₂ :=
                (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).δ₀.obj
                  (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
                ((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).δ₀.map'
                    0 1 isComplex₂_iff._proof_2 ⋯ :
                  (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).δ₀.obj
                      (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
                    (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).δ₀.obj
                      (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
                ((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).δ₀.map'
                    1 2 isComplex₂_iff._proof_4 ⋯ :
                  (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).δ₀.obj
                      (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
                    (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).δ₀.obj
                      (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).map'
            1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
        zero := ⋯ : ShortComplex.{v_1, u_1} C }.f
⊢ {
      X₁ :=
        (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂ (X₀ :=
              (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).δ₀.obj
                (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
              (X₁ :=
              (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).δ₀.obj
                (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
              (X₂ :=
              (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).δ₀.obj
                (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
              ((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).δ₀.map'
                  0 1 isComplex₂_iff._proof_2 ⋯ :
                (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).δ₀.obj
                    (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
                  (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).δ₀.obj
                    (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
              ((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).δ₀.map'
                  1 2 isComplex₂_iff._proof_4 ⋯ :
                (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).δ₀.obj
                    (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
                  (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).δ₀.obj
                    (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).map'
          0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g :=
        (mk₂ (X₀ :=
              (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).δ₀.obj
                (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
              (X₁ :=
              (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).δ₀.obj
                (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
              (X₂ :=
              (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).δ₀.obj
                (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
              ((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).δ₀.map'
                  0 1 isComplex₂_iff._proof_2 ⋯ :
                (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).δ₀.obj
                    (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
                  (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).δ₀.obj
                    (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
              ((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).δ₀.map'
                  1 2 isComplex₂_iff._proof_4 ⋯ :
                (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).δ₀.obj
                    (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
                  (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).δ₀.obj
                    (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).map'
          1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

Tactic:
rwa [ShortComplex.exact_iff_epi _ (by simp)]

Premises used: CategoryTheory.ShortComplex.exact_iff_epi