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₂_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 obtain : ∀ (A₄ : C) (π₄ : A₄ ⟶ A₃),
  Epi π₄ →
    ∀ (f₀ : A₄ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)
      (h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13),
      ∃ (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' φ 0 _) g₀
-- 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₂
w_2 : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w_3 : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ ∃ (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 refine : (π₄ ≫ π₃ ≫ π₂ ≫ π₁) ≫ g₁ =
  HAdd.hAdd (β := A₄ ⟶ R₁.obj 1) (π₄ ≫ π₃ ≫ f₁) (f₀ ≫ R₁.map' 0 1 sorry sorry : A₄ ⟶ R₁.obj 1) ≫
    app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11
Tactic: refine ⟨A₄, π₄ ≫ π₃ ≫ π₂ ≫ π₁, inferInstance,
    π₄ ≫ π₃ ≫ f₁ + f₀ ≫ (by exact R₁.map' 0 1), ?_⟩
-- 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₂
w_2 : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w_3 : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ (π₄ ≫ π₃ ≫ π₂ ≫ π₁) ≫ g₁ =
    HAdd.hAdd (β := A₄ ⟶ R₁.obj 1) (π₄ ≫ π₃ ≫ f₁) (f₀ ≫ R₁.map' 0 1 ⋯ ⋯ : A₄ ⟶ R₁.obj 1) ≫
      app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11
have rw : π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ =
  π₄ ≫ π₃ ≫ f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)
Tactic: rw [assoc, assoc, assoc, add_comp, assoc, assoc, assoc, NatTrans.naturality,
    ← reassoc_of% h₆, ← h₅, comp_sub]
-- 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₂
w_2 : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w_3 : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ =
    π₄ ≫ π₃ ≫ f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)
have dsimp : π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)
Tactic: dsimp
-- 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₂
w_2 : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w_3 : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)
have rw : π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁
Tactic: rw [add_sub_cancel]
-- 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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
⊢ Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
have h₂ : Epi (X := (Functor.obj δlastFunctor R₁).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)
  (app' (Functor.map δlastFunctor φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
Tactic: apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1
      (R₂.exact_iff_δlast.1 hR₂).1
-- 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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
h₂ :
  Epi (X := (Functor.obj δlastFunctor R₁).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)
    (app' (Functor.map δlastFunctor φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
⊢ Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
have h₅ : Mono (X := (Functor.obj δlastFunctor R₁).obj' 1 mono_of_epi_of_mono_of_mono'._proof_11)
  (app' (Functor.map δlastFunctor φ) 1 mono_of_epi_of_mono_of_mono'._proof_11)
Tactic: apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1
      (R₂.exact_iff_δlast.1 hR₂).1
-- 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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
h₂ :
  Epi (X := (Functor.obj δlastFunctor R₁).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)
    (app' (Functor.map δlastFunctor φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₅ :
  Mono (X := (Functor.obj δlastFunctor R₁).obj' 1 mono_of_epi_of_mono_of_mono'._proof_11)
    (app' (Functor.map δlastFunctor φ) 1 mono_of_epi_of_mono_of_mono'._proof_11)
⊢ Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
have h₆ : Mono (X := (Functor.obj δlastFunctor R₁).obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
  (app' (Functor.map δlastFunctor φ) 3 mono_of_epi_of_mono_of_mono'._proof_7)
Tactic: apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1
      (R₂.exact_iff_δlast.1 hR₂).1
-- 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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
⊢ Mono (X := (Functor.obj δlastFunctor R₁).obj' 1 mono_of_epi_of_mono_of_mono'._proof_11)
    (app' (Functor.map δlastFunctor φ) 1 mono_of_epi_of_mono_of_mono'._proof_11)
have h₂ : Mono (X := R₁.obj 1) (φ.app 1)
Tactic: dsimp
-- 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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
⊢ Mono (X := (Functor.obj δlastFunctor R₁).obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
    (app' (Functor.map δlastFunctor φ) 3 mono_of_epi_of_mono_of_mono'._proof_7)
have h₅ : Mono (X := R₁.obj 3) (φ.app 3)
Tactic: dsimp
-- 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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
⊢ IsIso (app' φ 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)
have this : Mono (X := R₁.obj' 2 sorry) (app' φ 2 sorry)
Tactic: have : Mono (app' φ 2) := by
    apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1
      (R₂.exact_iff_δlast.1 hR₂).1 <;> dsimp <;> infer_instance
-- 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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
⊢ Epi (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
have h₂ : Epi (X := (Functor.obj δ₀Functor R₁).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)
  (app' (Functor.map δ₀Functor φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
Tactic: apply epi_of_epi_of_epi_of_mono (δ₀Functor.map φ) (R₁.exact_iff_δ₀.1 hR₁).2
      (R₂.exact_iff_δ₀.1 hR₂).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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
h₂ :
  Epi (X := (Functor.obj δ₀Functor R₁).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)
    (app' (Functor.map δ₀Functor φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
⊢ Epi (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
have h₅ : Epi (X := (Functor.obj δ₀Functor R₁).obj' 2 mono_of_epi_of_mono_of_mono'._proof_4)
  (app' (Functor.map δ₀Functor φ) 2 mono_of_epi_of_mono_of_mono'._proof_4)
Tactic: apply epi_of_epi_of_epi_of_mono (δ₀Functor.map φ) (R₁.exact_iff_δ₀.1 hR₁).2
      (R₂.exact_iff_δ₀.1 hR₂).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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
h₂ :
  Epi (X := (Functor.obj δ₀Functor R₁).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)
    (app' (Functor.map δ₀Functor φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₅ :
  Epi (X := (Functor.obj δ₀Functor R₁).obj' 2 mono_of_epi_of_mono_of_mono'._proof_4)
    (app' (Functor.map δ₀Functor φ) 2 mono_of_epi_of_mono_of_mono'._proof_4)
⊢ Epi (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
have h₆ : Mono (X := (Functor.obj δ₀Functor R₁).obj' 3 mono_of_epi_of_mono_of_mono'._proof_7)
  (app' (Functor.map δ₀Functor φ) 3 mono_of_epi_of_mono_of_mono'._proof_7)
Tactic: apply epi_of_epi_of_epi_of_mono (δ₀Functor.map φ) (R₁.exact_iff_δ₀.1 hR₁).2
      (R₂.exact_iff_δ₀.1 hR₂).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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
⊢ Epi (X := (Functor.obj δ₀Functor R₁).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)
    (app' (Functor.map δ₀Functor φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
have h₂ : Epi (X := R₁.obj 1) (φ.app 1)
Tactic: dsimp
-- 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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
⊢ Epi (X := (Functor.obj δ₀Functor R₁).obj' 2 mono_of_epi_of_mono_of_mono'._proof_4)
    (app' (Functor.map δ₀Functor φ) 2 mono_of_epi_of_mono_of_mono'._proof_4)
have h₂ : Epi (X := R₁.obj 3) (φ.app 3)
Tactic: dsimp
-- 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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (X := R₁.obj 0) (φ.app 0)
h₁ : IsIso (X := R₁.obj 1) (φ.app 1)
h₃ : IsIso (X := R₁.obj 3) (φ.app 3)
h₄ : Mono (X := R₁.obj 4) (φ.app 4)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
⊢ IsIso (app' φ 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)
have this₁ : Epi (X := R₁.obj' 2 sorry) (app' φ 2 sorry)
Tactic: have : Epi (app' φ 2) := by
    apply epi_of_epi_of_epi_of_mono (δ₀Functor.map φ) (R₁.exact_iff_δ₀.1 hR₁).2
      (R₂.exact_iff_δ₀.1 hR₂).2 <;> dsimp <;> infer_instance
-- 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
n k : ℕ
h : k + 3 ≤ n
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ k₁ k₂ k₃ : ℕ
hk₀ : k₀ = k
hk₁ : k₁ = k + 1
hk₂ : k₂ = k + 2
hk₃ : k₃ = k + 3
h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)
h₁ : Mono (X := R₁.obj' k₁ ⋯) (app' φ k₁ ⋯)
h₃ : Mono (X := R₁.obj' k₃ ⋯) (app' φ k₃ ⋯)
⊢ Mono (X := R₁.obj' k₂ ⋯) (app' φ k₂ ⋯)
have subst_vars : ∀ (h : k₀ + 3 ≤ n) (h₀ : Epi (X := R₁.obj' k₀ sorry) (app' φ k₀ sorry)) (h₁ : Mono (app' φ (k₀ + 1) sorry))
  (h₃ : Mono (app' φ (k₀ + 3) sorry)), Mono (app' φ (k₀ + 2) sorry)
Tactic: subst_vars
Cleared hypotheses: k, h, k₁, k₂, k₃, hk₀, hk₁, hk₂, hk₃, h₀, h₁, 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
n : ℕ
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)
h₁ : Mono (app' φ (k₀ + 1) ⋯)
h₃ : Mono (app' φ (k₀ + 3) ⋯)
⊢ Mono (app' φ (k₀ + 2) ⋯)
have h₂ : Epi (X := R₁.obj' (k₀ + 0) sorry) (app' φ (k₀ + 0) sorry)
Tactic: change Epi (app' φ (k₀ + 0)) at h₀
Cleared hypotheses: 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
n : ℕ
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₁ : Mono (app' φ (k₀ + 1) ⋯)
h₃ : Mono (app' φ (k₀ + 3) ⋯)
h₀ : Epi (X := R₁.obj' (k₀ + 0) ⋯) (app' φ (k₀ + 0) ⋯)
⊢ Mono (app' φ (k₀ + 2) ⋯)
have rw : ∀
  (h₁ :
    Mono (X := R₁.obj' (k₀ + 1) sorry) (Y := R₂.obj' (k₀ + 1) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 1 mono_of_epi_of_mono_of_mono'._proof_11 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 1 mono_of_epi_of_mono_of_mono'._proof_11 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 1 mono_of_epi_of_mono_of_mono'._proof_11))
  (h₃ :
    Mono (X := R₁.obj' (k₀ + 3) sorry) (Y := R₂.obj' (k₀ + 3) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 3 mono_of_epi_of_mono_of_mono'._proof_7 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 3 mono_of_epi_of_mono_of_mono'._proof_7 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 3 mono_of_epi_of_mono_of_mono'._proof_7))
  (h₀ :
    Epi (X := R₁.obj' (k₀ + 0) sorry) (Y := R₂.obj' (k₀ + 0) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 0 mono_of_epi_of_mono_of_mono'._proof_13 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)),
  Mono (X := R₁.obj' (k₀ + 2) sorry) (Y := R₂.obj' (k₀ + 2) sorry)
    (app' (Functor.map (natAddLEFunctor h) φ) 2 mono_of_epi_of_mono_of_mono'._proof_4 :
      (Functor.obj (natAddLEFunctor h) R₁).obj' 2 mono_of_epi_of_mono_of_mono'._proof_4 ⟶
        (Functor.obj (natAddLEFunctor h) R₂).obj' 2 mono_of_epi_of_mono_of_mono'._proof_4)
Tactic: rw [← natAddLEFunctor_app' h] at h₀ h₁ h₃ ⊢
Cleared hypotheses: h₁, h₃, 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
n k : ℕ
h : k + 3 ≤ n
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ k₁ k₂ k₃ : ℕ
hk₀ : k₀ = k
hk₁ : k₁ = k + 1
hk₂ : k₂ = k + 2
hk₃ : k₃ = k + 3
h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)
h₂ : Epi (X := R₁.obj' k₂ ⋯) (app' φ k₂ ⋯)
h₃ : Mono (X := R₁.obj' k₃ ⋯) (app' φ k₃ ⋯)
⊢ Epi (X := R₁.obj' k₁ ⋯) (app' φ k₁ ⋯)
have subst_vars : ∀ (h : k₀ + 3 ≤ n) (h₀ : Epi (X := R₁.obj' k₀ sorry) (app' φ k₀ sorry)) (h₂ : Epi (app' φ (k₀ + 2) sorry))
  (h₃ : Mono (app' φ (k₀ + 3) sorry)), Epi (app' φ (k₀ + 1) sorry)
Tactic: subst_vars
Cleared hypotheses: k, h, k₁, k₂, k₃, hk₀, hk₁, hk₂, hk₃, h₀, h₂, h₃