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
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
⊢ f₂ = 0
have h₁₄ : Eq.{v_1 + 1} (α := A₃ ⟶ R₁.obj 2) 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]
-- 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₁ :
  (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)
⊢ Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
have 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
Tactic: rw [epi_iff_surjective_up_to_refinements]
-- 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₁ :
  (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) (_ : 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
have 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 sorry sorry = 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
Tactic: obtain ⟨A₁, π₁, _, f₂, h₁⟩ :=
    surjective_up_to_refinements_of_epi (app' φ 2 _) (g₁ ≫ R₂.map' 1 2)
-- 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₁ :
  (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
have rw : (f₂ ≫ R₁.map' 2 3 sorry sorry) ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 =
  0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7
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]
-- 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₁ :
  (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
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
have rw₁ : f₂ ≫ R₁.map' 2 3 sorry sorry ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 =
  0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7
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]
-- 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₁ :
  (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
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
have rw₂ : f₂ ≫ R₁.map' 2 3 sorry sorry ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 = 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]
-- 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₁ :
  (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
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
have rw₃ : Eq (α := A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
  (f₂ ≫ φ.app (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ≫ R₂.map (homOfLE sorry) :
    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)
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]
-- 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₁ :
  (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)
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
have 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 sorry sorry : R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ R₂.obj ⟨2, sorry⟩)
          (R₂.map (homOfLE sorry) : R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ R₂.obj ⟨3, sorry⟩) :
    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)
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]
-- 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₁ :
  (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)
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
have rw₅ : π₁ ≫ g₁ ≫ R₂.map' 1 3 sorry sorry = 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]
-- 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₁ :
  (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
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
have rw₆ : Eq (α := A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7) (π₁ ≫ g₁ ≫ 0) 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]
-- 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₁ :
  (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
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
have rw₇ : Eq (α := A₁ ⟶ R₂.obj' 3 mono_of_epi_of_mono_of_mono'._proof_7) (π₁ ≫ 0) 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]