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₁ :
  (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
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
have rw₈ : Eq.{v_1 + 1} (α := 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (hypothesis)
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
⊢ ∃ (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 h₄ : f₂ ≫ R₁.map' 2 3 sorry sorry = 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]
-- 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₂_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
⊢ ∃ (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₂ ⟶
          ((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
              sorry 0 sorry).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
                sorry 0 sorry).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
Tactic: obtain ⟨A₂, π₂, _, f₁, h₃⟩ := (hR₁.exact 0).exact_up_to_refinements _ h₂
-- 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₂_1 : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃_1 : 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
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
⊢ Eq (α := A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    ((π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
have rw : HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
    A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
    ((π₂ ≫ π₁ ≫ g₁) ≫ R₂.map' 1 2 sorry sorry : A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
    ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 sorry sorry :
      A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
  0
Tactic: rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]
-- 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₂_1 : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃_1 : 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
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
rw :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((π₂ ≫ π₁ ≫ g₁) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
⊢ Eq (α := A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    ((π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
have rw₁ : HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
    A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
    (π₂ ≫ (π₁ ≫ g₁) ≫ R₂.map' 1 2 sorry sorry : A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
    ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 sorry sorry :
      A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
  0
Tactic: rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]
-- 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₂_1 : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃_1 : 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
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
rw :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((π₂ ≫ π₁ ≫ g₁) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
rw₁ :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (π₂ ≫ (π₁ ≫ g₁) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
⊢ Eq (α := A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    ((π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
have rw₂ : HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
    A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
    (π₂ ≫ π₁ ≫ g₁ ≫ R₂.map' 1 2 sorry sorry : A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
    ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 sorry sorry :
      A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
  0
Tactic: rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]
-- 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₂_1 : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃_1 : 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
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
rw :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((π₂ ≫ π₁ ≫ g₁) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
rw₁ :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (π₂ ≫ (π₁ ≫ g₁) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
rw₂ :
  HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
      A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      (π₂ ≫ π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
      ((f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ :
        A₂ ⟶ R₂.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
    0
⊢ Eq (α := A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    ((π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
have rw₃ : HSub.hSub (α := A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (β :=
    A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
    (π₂ ≫ π₁ ≫ g₁ ≫ R₂.map' 1 2 sorry sorry : A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
    (f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11 ≫ R₂.map' 1 2 sorry sorry :
      A₂ ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) =
  0
Tactic: rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (hypothesis)
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₃_1 : 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
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
⊢ ∃ (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 h₄ : Eq (α := A₂ ⟶ R₂.obj ⟨2, sorry⟩)
  ((π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 sorry sorry : A₂ ⟶ R₂.obj ⟨2, sorry⟩)
  (0 : A₂ ⟶ R₂.obj ⟨2, sorry⟩)
Tactic: have h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 _) ≫ R₂.map' 1 2 = 0 := by
    rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]
-- 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₂_1 : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃_1 : 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
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₄ :
  Eq (α := A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    ((π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
⊢ ∃ (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 π₃ →
    ∀
      (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
              sorry 0 sorry).X₁)
      (h₅ :
        π₃ ≫ (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) =
          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
                sorry 0 sorry).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
Tactic: obtain ⟨A₃, π₃, _, g₀, h₅⟩ := (hR₂.exact 0).exact_up_to_refinements _ h₄
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (hypothesis)
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₃_1 : 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
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₄ :
  Eq (α := A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    ((π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₂ ⟶ R₂.obj ⟨2, ⋯⟩)
A₃ : C
π₃ : A₃ ⟶ A₂
w_2 : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ φ.app 1) = g₀ ≫ R₂.map (homOfLE ⋯)
⊢ ∃ (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 h₆ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE sorry)
Tactic: rw [comp_sub] at h₅
Cleared hypotheses: h₅