awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ :
  (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, ⋯⟩)

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]
-- 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₁ :
  (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, ⋯⟩)
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
                ⋯ 0 ⋯).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
                  ⋯ 0 ⋯).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
⊢ ∃ (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₄

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₁ :
  (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 ⋯)
⊢ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)

Tactic:
rw [comp_sub] at h₅

Premises used: CategoryTheory.Preadditive.comp_sub
-- 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₁ :
  (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 ⋯)
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
⊢ ∃ (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₀

Premises used: CategoryTheory.ComposableArrows.app', CategoryTheory.surjective_up_to_refinements_of_epi, 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₁ :
  (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
⊢ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13 ⟶ R₁.obj 1

Tactic:
exact R₁.map' 0 1

Premises used: OfNat.ofNat, CategoryTheory.ComposableArrows.map'
-- 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₁ :
  (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
refine :
  (π₄ ≫ π₃ ≫ π₂ ≫ π₁) ≫ 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
⊢ ∃ (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:
refine ⟨A₄, π₄ ≫ π₃ ≫ π₂ ≫ π₁, inferInstance,
    π₄ ≫ π₃ ≫ f₁ + f₀ ≫ (by exact R₁.map' 0 1), ?_⟩
-- 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₁ :
  (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
rw :
  π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ =
    π₄ ≫ π₃ ≫ f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)
⊢ (π₄ ≫ π₃ ≫ π₂ ≫ π₁) ≫ 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

Tactic:
rw [assoc, assoc, assoc, add_comp, assoc, assoc, assoc, NatTrans.naturality,
    ← reassoc_of% h₆, ← h₅, comp_sub]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.add_comp, CategoryTheory.NatTrans.naturality, CategoryTheory.Preadditive.comp_sub
-- 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₁ :
  (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
dsimp : π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)
⊢ π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ =
    π₄ ≫ π₃ ≫ f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)

Tactic:
dsimp
-- 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₁ :
  (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
rw rw₁ : π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁
⊢ π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)

Tactic:
rw [add_sub_cancel]

Premises used: add_sub_cancel
-- 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₁.Exact
hR₂ : R₂.Exact
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)
⊢ R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0

Tactic:
simpa only [R₂.map'_comp 1 2 3] using hR₂.toIsComplex.zero 1

Premises used: CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.map'_comp, OfNat.ofNat, CategoryTheory.ComposableArrows.IsComplex.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 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)
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)
⊢ Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)

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

Premises used: CategoryTheory.ComposableArrows.exact_iff_δlast, CategoryTheory.ComposableArrows.δlastFunctor, CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono, CategoryTheory.Functor.map, And.left, Iff.mp
-- 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 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 := R₁.obj 0) (φ.app 0)
⊢ 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:
dsimp
-- 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 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₂ : Mono (X := R₁.obj 1) (φ.app 1)
⊢ 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:
dsimp
-- 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 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₅ : Mono (X := R₁.obj 3) (φ.app 3)
⊢ 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:
dsimp
-- 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 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)
⊢ Epi (X := R₁.obj 0) (φ.app 0)

Tactic:
infer_instance
-- 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 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 1) (φ.app 1)

Tactic:
infer_instance
-- 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 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 3) (φ.app 3)

Tactic:
infer_instance
-- 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 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 ⋯)

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