Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
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)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Epi (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)

Tactic:
refine epi_of_epi_of_epi_of_mono' ψ (exact₂_mk _ (by simp) ?_)
    (hR₂.exact 0).exact_toComposableArrows (by simp)
    h₀ h₁ (by dsimp [ψ]; infer_instance)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
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)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Epi (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ {
      X₁ :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).map'
          0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).map'
          1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ }.Exact