awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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
⊢ f₂ = 0
have h₆ : f₁ ≫ R₁.map (homOfLE sorry) = 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]
-- 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 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
⊢ f₂ = 0
have h₇ : π₂ ≫ f₁ ≫ R₁.map (homOfLE sorry) = π₂ ≫ 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]
-- 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 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
⊢ f₂ = 0
have h₈ : π₃ ≫ π₂ ≫ f₁ ≫ R₁.map (homOfLE sorry) = π₃ ≫ π₂ ≫ 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]
-- 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 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
⊢ f₂ = 0
have h₉ : π₃ ≫ π₂ ≫ f₁ ≫ R₁.map (homOfLE sorry) = π₃ ≫ 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]
-- 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 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
⊢ f₂ = 0
have h₁₀ : π₃ ≫ π₂ ≫ f₁ ≫ R₁.map (homOfLE sorry) = 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]
-- 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 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
⊢ f₂ = 0
have h₁₁ : f₀ ≫ R₁.map' 0 1 sorry sorry ≫ R₁.map (homOfLE sorry) = 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]
-- 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 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
⊢ f₂ = 0
have h₁₂ : Eq (α := A₃ ⟶ R₁.obj 2) (f₀ ≫ R₁.map' 0 2 sorry sorry : A₃ ⟶ R₁.obj 2) (0 : A₃ ⟶ R₁.obj 2)
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]
-- 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 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)
⊢ f₂ = 0
have h₁₃ : Eq (α := A₃ ⟶ R₁.obj 2) (f₀ ≫ 0) 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]