awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁_1 : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃_1 : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
f₁ :
  A₁ ⟶
    ((mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
            (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).sc
        ⋯ 0 ⋯).X₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₃ :
  Eq (α := A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (CategoryStruct.comp (Y := R₂.obj' 1 ⋯) (f₁ ≫ app' φ 1 ⋯) (R₂.map' 1 2 ⋯ ⋯) : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
g₀ :
  A₂ ⟶
    ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
            (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
        ⋯ 0 ⋯).X₁
hg₀ :
  π₂ ≫ f₁ ≫ app' φ 1 ⋯ =
    g₀ ≫
      ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
              (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
          ⋯ 0 ⋯).f
h :
  ∀ (A₃ : C) (π₃ : A₃ ⟶ A₂),
    Epi π₃ →
      ∀ (f₀ : A₃ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)
        (hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13), f₂ = 0
⊢ f₂ = 0

Tactic:
obtain ⟨A₃, π₃, _, f₀, hf₀⟩ := surjective_up_to_refinements_of_epi (app' φ 0 _) g₀

Premises used: CategoryTheory.ComposableArrows.app', CategoryTheory.surjective_up_to_refinements_of_epi, OfNat.ofNat
-- 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 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁_1 : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃_1 : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
f₁ :
  A₁ ⟶
    ((mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
            (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).sc
        ⋯ 0 ⋯).X₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₃ :
  Eq (α := A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (CategoryStruct.comp (Y := R₂.obj' 1 ⋯) (f₁ ≫ app' φ 1 ⋯) (R₂.map' 1 2 ⋯ ⋯) : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
g₀ :
  A₂ ⟶
    ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
            (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
        ⋯ 0 ⋯).X₁
hg₀ :
  π₂ ≫ f₁ ≫ app' φ 1 ⋯ =
    g₀ ≫
      ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
              (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
          ⋯ 0 ⋯).f
A₃ : C
π₃ : A₃ ⟶ A₂
w_2 : Epi π₃
f₀ : A₃ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
rw :
  π₃ ≫ g₀ ≫ R₂.map (homOfLE ⋯) =
    π₃ ≫
      g₀ ≫
        ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
                (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
            ⋯ 0 ⋯).f
⊢ f₀ ≫ R₁.map' 0 1 ⋯ ⋯ = π₃ ≫ π₂ ≫ f₁

Tactic:
rw [← cancel_mono (app' φ 1 _), assoc, assoc, assoc, NatTrans.naturality,
      ← reassoc_of% hf₀, hg₀]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ComposableArrows.app', CategoryTheory.cancel_mono, CategoryTheory.NatTrans.naturality, OfNat.ofNat
-- 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 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁_1 : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃_1 : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
f₁ :
  A₁ ⟶
    ((mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
            (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).sc
        ⋯ 0 ⋯).X₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₃ :
  Eq (α := A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (CategoryStruct.comp (Y := R₂.obj' 1 ⋯) (f₁ ≫ app' φ 1 ⋯) (R₂.map' 1 2 ⋯ ⋯) : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
g₀ :
  A₂ ⟶
    ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
            (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
        ⋯ 0 ⋯).X₁
hg₀ :
  π₂ ≫ f₁ ≫ app' φ 1 ⋯ =
    g₀ ≫
      ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
              (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
          ⋯ 0 ⋯).f
A₃ : C
π₃ : A₃ ⟶ A₂
w_2 : Epi π₃
f₀ : A₃ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ π₃ ≫ g₀ ≫ R₂.map (homOfLE ⋯) =
    π₃ ≫
      g₀ ≫
        ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
                (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
            ⋯ 0 ⋯).f

Tactic:
rfl
-- 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 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁_1 : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃_1 : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
f₁ :
  A₁ ⟶
    ((mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
            (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).sc
        ⋯ 0 ⋯).X₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₃ :
  Eq (α := A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (CategoryStruct.comp (Y := R₂.obj' 1 ⋯) (f₁ ≫ app' φ 1 ⋯) (R₂.map' 1 2 ⋯ ⋯) : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
g₀ :
  A₂ ⟶
    ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
            (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
        ⋯ 0 ⋯).X₁
hg₀ :
  π₂ ≫ f₁ ≫ app' φ 1 ⋯ =
    g₀ ≫
      ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
              (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
          ⋯ 0 ⋯).f
A₃ : C
π₃ : A₃ ⟶ A₂
w_2 : Epi π₃
f₀ : A₃ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ f₀ ≫ R₁.map' 0 1 ⋯ ⋯ = π₃ ≫ π₂ ≫ f₁

Tactic:
have h₄ : f₀ ≫ R₁.map' 0 1 = π₃ ≫ π₂ ≫ f₁ := by
    rw [← cancel_mono (app' φ 1 _), assoc, assoc, assoc, NatTrans.naturality,
      ← reassoc_of% hf₀, hg₀]
    rfl
-- 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 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁_1 : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃_1 : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
f₁ :
  A₁ ⟶
    ((mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
            (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).sc
        ⋯ 0 ⋯).X₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₃ :
  Eq (α := A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (CategoryStruct.comp (Y := R₂.obj' 1 ⋯) (f₁ ≫ app' φ 1 ⋯) (R₂.map' 1 2 ⋯ ⋯) : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
g₀ :
  A₂ ⟶
    ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
            (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
        ⋯ 0 ⋯).X₁
hg₀ :
  π₂ ≫ f₁ ≫ app' φ 1 ⋯ =
    g₀ ≫
      ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
              (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
          ⋯ 0 ⋯).f
A₃ : C
π₃ : A₃ ⟶ A₂
w_2 : Epi π₃
f₀ : A₃ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
h₄ : f₀ ≫ R₁.map' 0 1 ⋯ ⋯ = π₃ ≫ π₂ ≫ f₁
h : π₁ ≫ f₂ = π₁ ≫ 0
h₅ : π₁ ≫ f₂ = 0
h₆ : f₁ ≫ R₁.map (homOfLE ⋯) = 0
h₇ : π₂ ≫ f₁ ≫ R₁.map (homOfLE ⋯) = π₂ ≫ 0
h₈ : π₃ ≫ π₂ ≫ f₁ ≫ R₁.map (homOfLE ⋯) = π₃ ≫ π₂ ≫ 0
h₉ : π₃ ≫ π₂ ≫ f₁ ≫ R₁.map (homOfLE ⋯) = π₃ ≫ 0
h₁₀ : π₃ ≫ π₂ ≫ f₁ ≫ R₁.map (homOfLE ⋯) = 0
h₁₁ : f₀ ≫ R₁.map' 0 1 ⋯ ⋯ ≫ R₁.map (homOfLE ⋯) = 0
h₁₂ : Eq (α := A₃ ⟶ R₁.obj 2) (f₀ ≫ R₁.map' 0 2 ⋯ ⋯ : A₃ ⟶ R₁.obj 2) (0 : A₃ ⟶ R₁.obj 2)
h₁₃ : Eq (α := A₃ ⟶ R₁.obj 2) (f₀ ≫ 0) 0
h₁₄ h₁₅ : Eq.{v_1 + 1} (α := A₃ ⟶ R₁.obj 2) 0 0
⊢ f₂ = 0

Tactic:
rw [← cancel_epi π₁, comp_zero, hf₁, ← cancel_epi π₂, ← cancel_epi π₃, comp_zero,
    comp_zero, ← reassoc_of% h₄, ← R₁.map'_comp 0 1 2, hR₁, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.ComposableArrows.map'_comp, OfNat.ofNat, CategoryTheory.cancel_epi
-- 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 3
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
⊢ R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0

Tactic:
simpa only [R₁.map'_comp 0 1 2] using hR₁.toIsComplex.zero 0

Premises used: CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.map'_comp, OfNat.ofNat, CategoryTheory.ComposableArrows.IsComplex.zero
-- 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 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
rw :
  ∀ ⦃A : C⦄ (y : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ R₁.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11),
      π ≫ y = x ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11
⊢ Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)

Tactic:
rw [epi_iff_surjective_up_to_refinements]

Premises used: CategoryTheory.epi_iff_surjective_up_to_refinements
-- 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 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
obtain :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A),
    Epi π₁ →
      ∀ (f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4)
        (h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ R₁.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11),
          π ≫ g₁ = x ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ R₁.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11),
    π ≫ g₁ = x ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11

Tactic:
obtain ⟨A₁, π₁, _, f₂, h₁⟩ :=
    surjective_up_to_refinements_of_epi (app' φ 2 _) (g₁ ≫ R₂.map' 1 2)

Premises used: CategoryTheory.ComposableArrows.app', CategoryTheory.surjective_up_to_refinements_of_epi, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.ComposableArrows.map'
-- 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 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
rw :
  (f₂ ≫ R₁.map' 2 3 ⋯ ⋯) ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 =
    0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7
rw₁ :
  f₂ ≫ R₁.map' 2 3 ⋯ ⋯ ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 =
    0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7
rw₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 = 0
rw₃ :
  Eq (α := A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
    (f₂ ≫ φ.app (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ≫ R₂.map (homOfLE ⋯) :
      A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
    (0 : A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
rw₄ :
  Eq (α := A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
    (π₁ ≫
        g₁ ≫
          CategoryStruct.comp (Y := R₂.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4)
            (R₂.map' 1 2 ⋯ ⋯ : R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ R₂.obj ⟨2, ⋯⟩)
            (R₂.map (homOfLE ⋯) : R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ R₂.obj ⟨3, ⋯⟩) :
      A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
    (0 : A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
rw₅ : π₁ ≫ g₁ ≫ R₂.map' 1 3 ⋯ ⋯ = 0
rw₆ : Eq (α := A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7) (π₁ ≫ g₁ ≫ 0) 0
rw₇ : Eq (α := A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7) (π₁ ≫ 0) 0
rw₈ rw₉ : Eq.{v_1 + 1} (α := A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7) 0 0
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0

Tactic:
rw [← cancel_mono (app' φ 3 _), assoc, zero_comp, NatTrans.naturality, ← reassoc_of% h₁,
      ← R₂.map'_comp 1 2 3, hR₂', comp_zero, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ComposableArrows.app', CategoryTheory.Limits.comp_zero, CategoryTheory.ComposableArrows.map'_comp, CategoryTheory.cancel_mono, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.zero_comp, OfNat.ofNat
-- 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 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0

Tactic:
have h₂ : f₂ ≫ R₁.map' 2 3 = 0 := by
    rw [← cancel_mono (app' φ 3 _), assoc, zero_comp, NatTrans.naturality, ← reassoc_of% h₁,
      ← R₂.map'_comp 1 2 3, hR₂', comp_zero, comp_zero]
-- 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 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂_1 : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
obtain :
  ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁),
    Epi π₂ →
      ∀
        (f₁ :
          A₂ ⟶
            ((mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
                    (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).sc
                ⋯ 0 ⋯).X₁)
        (h₃ :
          π₂ ≫ f₂ =
            f₁ ≫
              ((mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
                      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).sc
                  ⋯ 0 ⋯).f),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ R₁.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11),
          π ≫ g₁ = x ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ R₁.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11),
    π ≫ g₁ = x ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11

Tactic:
obtain ⟨A₂, π₂, _, f₁, h₃⟩ := (hR₁.exact 0).exact_up_to_refinements _ h₂

Premises used: CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, OfNat.ofNat, CategoryTheory.ComposableArrows.Exact.exact