Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_1
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₂ : R₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
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₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯
    ⋯
⊢ {
      X₁ :=
        (mk₂
              ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂
              ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂
              ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂
              ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 := ⋯ }.Exact

Tactic:
ShortComplex.exact_iff_mono _ (by simp)

Goal state after:
case refine_1
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₂ : R₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
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₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯
    ⋯
⊢ Mono
    {
        X₁ :=
          (mk₂
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)).obj
            ⟨0, ⋯⟩,
        X₂ :=
          (mk₂
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)).obj
            ⟨1, ⋯⟩,
        X₃ :=
          (mk₂
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)).obj
            ⟨2, ⋯⟩,
        f :=
          (mk₂
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).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 := ⋯ }.g