awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
rw :
  ∀ ⦃A : C⦄ (y : A ⟶ kernel b),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ kernel t), π ≫ y = x ≫ kernel.map t b l r ⋯
⊢ Epi (X := kernel t) (Y := kernel b) (kernel.map t b l r ⋯)

Tactic:
rw [epi_iff_surjective_up_to_refinements]

Premises used: CategoryTheory.epi_iff_surjective_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
⊢ Eq (α :=
    A₀ ⟶
      ShortComplex.X₃
        (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
          (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯))
    (CategoryStruct.comp (Y :=
      ShortComplex.X₂
        (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
          (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯))
      (z ≫ kernel.ι b ≫ biprod.inr)
      (ShortComplex.g
        (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
          (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)))
    0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
obtain :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A₀),
    Epi π₁ →
      ∀
        (x₁ :
          A₁ ⟶
            ShortComplex.X₁
              (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
                Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
                (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯))
        (hx₁ :
          π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
            x₁ ≫
              ShortComplex.f
                (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
                  Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
                  (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)),
        ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x : A' ⟶ kernel t), π ≫ z = x ≫ kernel.map t b l r ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x : A' ⟶ kernel t), π ≫ z = x ≫ kernel.map t b l r ⋯

Tactic:
obtain ⟨A₁, π₁, _, x₁, hx₁⟩ := ((ShortComplex.mk _ _
    sq.cokernelCofork.condition).exact_of_g_is_cokernel
      sq.isColimitCokernelCofork).exact_up_to_refinements
        (z ≫ kernel.ι _ ≫ biprod.inr) (by simp)

Premises used: CategoryTheory.CommSq.cokernelCofork, CategoryTheory.ShortComplex.mk, CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, CategoryTheory.IsPushout.isColimitCokernelCofork, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsPushout.toCommSq, CategoryTheory.Limits.biprod.inr, CategoryTheory.Limits.kernel.ι
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₁ :
  A₁ ⟶
    ShortComplex.X₁
      (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
        Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
        (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      ShortComplex.f
        (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
          (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x : A' ⟶ kernel t), π ≫ z = x ≫ kernel.map t b l r ⋯

Tactic:
⟨A₁, π₁, inferInstance, -kernel.lift _ x₁ ?_, ?_⟩

Premises used: inferInstance, Exists.intro, Neg.neg, CategoryTheory.Limits.kernel.lift
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₁ :
  A₁ ⟶
    ShortComplex.X₁
      (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
        Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
        (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      ShortComplex.f
        (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
          (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
refine_1 : x₁ ≫ t = 0
refine_2 : π₁ ≫ z = CategoryStruct.comp (Y := kernel t) (-kernel.lift t x₁ ⋯) (kernel.map t b l r ⋯)
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x : A' ⟶ kernel t), π ≫ z = x ≫ kernel.map t b l r ⋯

Tactic:
refine ⟨A₁, π₁, inferInstance, -kernel.lift _ x₁ ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₁ :
  A₁ ⟶
    ShortComplex.X₁
      (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
        Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
        (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      ShortComplex.f
        (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
          (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
⊢ x₁ ≫ t = 0

Tactic:
simpa using hx₁.symm =≫ biprod.fst

Premises used: CategoryTheory.Limits.biprod.fst, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₁ :
  A₁ ⟶
    ShortComplex.X₁
      (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
        Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
        (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      ShortComplex.f
        (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
          (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
refine_2 :
  (π₁ ≫ z) ≫ equalizer.ι b 0 =
    CategoryStruct.comp (Y := equalizer b 0)
      (CategoryStruct.comp (Y := kernel t) (-kernel.lift t x₁ ⋯) (kernel.map t b l r ⋯)) (equalizer.ι b 0)
⊢ π₁ ≫ z = CategoryStruct.comp (Y := kernel t) (-kernel.lift t x₁ ⋯) (kernel.map t b l r ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.CommSq
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w : Epi π₁
x₁ :
  A₁ ⟶
    ShortComplex.X₁
      (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
        Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
        (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      ShortComplex.f
        (ShortComplex.mk (X₂ := biprod.{v, u} X₂ X₃) (X₃ :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} X₂ X₃) (biprod.lift t (-l)) 0) ⋯.cokernelCofork)
          (biprod.lift t (-l)) (Cofork.π ⋯.cokernelCofork) ⋯)
⊢ (π₁ ≫ z) ≫ equalizer.ι b 0 =
    CategoryStruct.comp (Y := equalizer b 0)
      (CategoryStruct.comp (Y := kernel t) (-kernel.lift t x₁ ⋯) (kernel.map t b l r ⋯)) (equalizer.ι b 0)

Tactic:
simpa using hx₁ =≫ biprod.snd

Premises used: CategoryTheory.Limits.biprod.snd
-- 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₁ : 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)
h :
  ∀ {P : C} (g : P ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4),
    g ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0 → g = 0
⊢ Mono (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)

Tactic:
apply mono_of_cancel_zero

Premises used: CategoryTheory.Preadditive.mono_of_cancel_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₁ : 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₃ : 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
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₂ :
  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 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 : 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)
    (CategoryStruct.comp (Y := R₂.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4)
        (0 : A ⟶ R₂.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4)
        (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 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7 : 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) 0 (0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
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, NatTrans.naturality, reassoc_of% h₁,
      zero_comp, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ComposableArrows.app', 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₁ : 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₃ : 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
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0

Tactic:
have h₂ : f₂ ≫ R₁.map' 2 3 = 0 := by
    rw [← cancel_mono (app' φ 3 _), assoc, NatTrans.naturality, reassoc_of% h₁,
      zero_comp, zero_comp]
-- 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₃ : 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
h :
  ∀ (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₁)
        (hf₁ :
          π₁ ≫ 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),
        f₂ = 0
⊢ f₂ = 0

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

Premises used: CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, OfNat.ofNat, CategoryTheory.ComposableArrows.Exact.exact
-- 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₃ : 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 ⋯)
rw :
  Eq (α := A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (f₁ ≫ CategoryStruct.comp (Y := R₂.obj' 1 ⋯) (app' φ 1 ⋯) (R₂.map' 1 2 ⋯ ⋯) : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
rw₁ :
  Eq (α := A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (f₁ ≫
        CategoryStruct.comp (Y := R₁.obj ⟨2, ⋯⟩)
          (R₁.map (homOfLE ⋯) : R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ R₁.obj ⟨2, ⋯⟩)
          (φ.app ⟨2, ⋯⟩ : R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ R₂.obj ⟨2, ⋯⟩) :
      A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
    (0 : A₁ ⟶ R₂.obj ⟨2, ⋯⟩)
rw₂ : π₁ ≫ f₂ ≫ φ.app (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) = 0
rw₃ : Eq (α := A₁ ⟶ R₂.obj ⟨2, ⋯⟩) (π₁ ≫ 0) 0
rw₄ rw₅ : Eq.{v_1 + 1} (α := A₁ ⟶ R₂.obj ⟨2, ⋯⟩) 0 0
⊢ 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, ⋯⟩)

Tactic:
rw [assoc, ← NatTrans.naturality, ← reassoc_of% hf₁, h₁, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.NatTrans.naturality
-- 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₃ : 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 ⋯)
⊢ 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, ⋯⟩)

Tactic:
have h₃ : (f₁ ≫ app' φ 1) ≫ R₂.map' 1 2 = 0 := by
    rw [assoc, ← NatTrans.naturality, ← reassoc_of% hf₁, h₁, 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₁ : 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, ⋯⟩)
h :
  ∀ (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
                ⋯ 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),
        f₂ = 0
⊢ f₂ = 0

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

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