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 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)
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)
⊢ Epi (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)

Tactic:
apply epi_of_epi_of_epi_of_mono (δ₀Functor.map φ) (R₁.exact_iff_δ₀.1 hR₁).2
      (R₂.exact_iff_δ₀.1 hR₂).2

Premises used: CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono, CategoryTheory.ComposableArrows.exact_iff_δ₀, CategoryTheory.Functor.map, And.right, CategoryTheory.ComposableArrows.δ₀Functor, 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)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
h₂ : Epi (X := R₁.obj 1) (φ.app 1)
⊢ 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:
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)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
h₂ : Epi (X := R₁.obj 3) (φ.app 3)
⊢ 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:
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)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
h₅ : Mono (X := R₁.obj 4) (φ.app 4)
⊢ 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:
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)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
⊢ Epi (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)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
⊢ Epi (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)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
⊢ Mono (X := R₁.obj 4) (φ.app 4)

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)
this : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
⊢ Epi (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)

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
-- 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)
this_1 : Mono (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
this : Epi (X := R₁.obj' 2 ⋯) (app' φ 2 ⋯)
⊢ IsIso (app' φ 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- 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
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₃ ⋯)
subst_vars :
  ∀ (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) ⋯)
⊢ Mono (X := R₁.obj' k₂ ⋯) (app' φ k₂ ⋯)

Tactic:
subst_vars
-- 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
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) ⋯)
⊢ Epi (X := R₁.obj' (k₀ + 0) ⋯) (app' φ (k₀ + 0) ⋯)

Tactic:
change Epi (app' φ (k₀ + 0)) at h₀

Premises used: CategoryTheory.Epi, CategoryTheory.ComposableArrows.app', HAdd.hAdd, 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
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) ⋯)
rw :
  ∀
    (h₁ :
      Mono (X := R₁.obj' (k₀ + 1) ⋯) (Y := R₂.obj' (k₀ + 1) ⋯)
        (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) ⋯) (Y := R₂.obj' (k₀ + 3) ⋯)
        (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) ⋯) (Y := R₂.obj' (k₀ + 0) ⋯)
        (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) ⋯) (Y := R₂.obj' (k₀ + 2) ⋯)
      (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)
⊢ Mono (app' φ (k₀ + 2) ⋯)

Tactic:
rw [← natAddLEFunctor_app' h] at h₀ h₁ h₃ ⊢

Premises used: CategoryTheory.ComposableArrows.natAddLEFunctor_app'
-- 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
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 (X := R₁.obj' (k₀ + 1) ⋯) (Y := R₂.obj' (k₀ + 1) ⋯)
    (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) ⋯) (Y := R₂.obj' (k₀ + 3) ⋯)
    (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) ⋯) (Y := R₂.obj' (k₀ + 0) ⋯)
    (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) ⋯) (Y := R₂.obj' (k₀ + 2) ⋯)
    (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:
mono_of_epi_of_mono_of_mono _ (natAddLEFunctor_obj_exact h hR₁)
    (natAddLEFunctor_obj_exact h hR₂) h₀ h₁ h₃

Premises used: CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono, CategoryTheory.ComposableArrows.natAddLEFunctor_obj_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
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 (X := R₁.obj' (k₀ + 1) ⋯) (Y := R₂.obj' (k₀ + 1) ⋯)
    (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) ⋯) (Y := R₂.obj' (k₀ + 3) ⋯)
    (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) ⋯) (Y := R₂.obj' (k₀ + 0) ⋯)
    (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) ⋯) (Y := R₂.obj' (k₀ + 2) ⋯)
    (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:
exact mono_of_epi_of_mono_of_mono _ (natAddLEFunctor_obj_exact h hR₁)
    (natAddLEFunctor_obj_exact h hR₂) h₀ h₁ h₃

Premises used: CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono, CategoryTheory.ComposableArrows.natAddLEFunctor_obj_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
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₃ ⋯)
subst_vars :
  ∀ (h : k₀ + 3 ≤ n) (h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)) (h₂ : Epi (app' φ (k₀ + 2) ⋯))
    (h₃ : Mono (app' φ (k₀ + 3) ⋯)), Epi (app' φ (k₀ + 1) ⋯)
⊢ Epi (X := R₁.obj' k₁ ⋯) (app' φ k₁ ⋯)

Tactic:
subst_vars
-- 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
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₂ : Epi (app' φ (k₀ + 2) ⋯)
h₃ : Mono (app' φ (k₀ + 3) ⋯)
⊢ Epi (X := R₁.obj' (k₀ + 0) ⋯) (app' φ (k₀ + 0) ⋯)

Tactic:
change Epi (app' φ (k₀ + 0)) at h₀

Premises used: CategoryTheory.Epi, CategoryTheory.ComposableArrows.app', HAdd.hAdd, 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
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 (app' φ (k₀ + 2) ⋯)
h₃ : Mono (app' φ (k₀ + 3) ⋯)
h₀ : Epi (X := R₁.obj' (k₀ + 0) ⋯) (app' φ (k₀ + 0) ⋯)
rw :
  ∀
    (h₂ :
      Epi (X := R₁.obj' (k₀ + 2) ⋯) (Y := R₂.obj' (k₀ + 2) ⋯)
        (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))
    (h₃ :
      Mono (X := R₁.obj' (k₀ + 3) ⋯) (Y := R₂.obj' (k₀ + 3) ⋯)
        (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) ⋯) (Y := R₂.obj' (k₀ + 0) ⋯)
        (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)),
    Epi (X := R₁.obj' (k₀ + 1) ⋯) (Y := R₂.obj' (k₀ + 1) ⋯)
      (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)
⊢ Epi (app' φ (k₀ + 1) ⋯)

Tactic:
rw [← natAddLEFunctor_app' h] at h₀ h₂ h₃ ⊢

Premises used: CategoryTheory.ComposableArrows.natAddLEFunctor_app'
-- 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
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₀ + 2) ⋯) (Y := R₂.obj' (k₀ + 2) ⋯)
    (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)
h₃ :
  Mono (X := R₁.obj' (k₀ + 3) ⋯) (Y := R₂.obj' (k₀ + 3) ⋯)
    (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) ⋯) (Y := R₂.obj' (k₀ + 0) ⋯)
    (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)
⊢ Epi (X := R₁.obj' (k₀ + 1) ⋯) (Y := R₂.obj' (k₀ + 1) ⋯)
    (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)

Tactic:
epi_of_epi_of_epi_of_mono _ (natAddLEFunctor_obj_exact h hR₁)
    (natAddLEFunctor_obj_exact h hR₂) h₀ h₂ h₃

Premises used: CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono, CategoryTheory.ComposableArrows.natAddLEFunctor_obj_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
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₀ + 2) ⋯) (Y := R₂.obj' (k₀ + 2) ⋯)
    (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)
h₃ :
  Mono (X := R₁.obj' (k₀ + 3) ⋯) (Y := R₂.obj' (k₀ + 3) ⋯)
    (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) ⋯) (Y := R₂.obj' (k₀ + 0) ⋯)
    (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)
⊢ Epi (X := R₁.obj' (k₀ + 1) ⋯) (Y := R₂.obj' (k₀ + 1) ⋯)
    (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)

Tactic:
exact epi_of_epi_of_epi_of_mono _ (natAddLEFunctor_obj_exact h hR₁)
    (natAddLEFunctor_obj_exact h hR₂) h₀ h₂ h₃

Premises used: CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono, CategoryTheory.ComposableArrows.natAddLEFunctor_obj_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
n k : ℕ
h : k + 4 ≤ n
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ k₁ k₂ k₃ k₄ : ℕ
hk₀ : k₀ = k
hk₁ : k₁ = k + 1
hk₂ : k₂ = k + 2
hk₃ : k₃ = k + 3
hk₄ : k₄ = k + 4
h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)
h₁ : IsIso (X := R₁.obj' k₁ ⋯) (app' φ k₁ ⋯)
h₃ : IsIso (X := R₁.obj' k₃ ⋯) (app' φ k₃ ⋯)
h₄ : Mono (X := R₁.obj' k₄ ⋯) (app' φ k₄ ⋯)
subst_vars :
  ∀ (h : k₀ + 4 ≤ n) (h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)) (h₁ : IsIso (app' φ (k₀ + 1) ⋯))
    (h₃ : IsIso (app' φ (k₀ + 3) ⋯)) (h₄ : Mono (app' φ (k₀ + 4) ⋯)), IsIso (app' φ (k₀ + 2) ⋯)
⊢ IsIso (X := R₁.obj' k₂ ⋯) (app' φ k₂ ⋯)

Tactic:
subst_vars
-- 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
n : ℕ
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 4 ≤ n
h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)
h₁ : IsIso (app' φ (k₀ + 1) ⋯)
h₃ : IsIso (app' φ (k₀ + 3) ⋯)
h₄ : Mono (app' φ (k₀ + 4) ⋯)
⊢ Epi (X := R₁.obj' (k₀ + 0) ⋯) (app' φ (k₀ + 0) ⋯)

Tactic:
change Epi (app' φ (k₀ + 0)) at h₀

Premises used: CategoryTheory.Epi, CategoryTheory.ComposableArrows.app', HAdd.hAdd, 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
n : ℕ
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 4 ≤ n
h₁ : IsIso (app' φ (k₀ + 1) ⋯)
h₃ : IsIso (app' φ (k₀ + 3) ⋯)
h₄ : Mono (app' φ (k₀ + 4) ⋯)
h₀ : Epi (X := R₁.obj' (k₀ + 0) ⋯) (app' φ (k₀ + 0) ⋯)
rw :
  ∀
    (h₁ :
      IsIso (X := R₁.obj' (k₀ + 1) ⋯) (Y := R₂.obj' (k₀ + 1) ⋯)
        (app' (Functor.map (natAddLEFunctor h) φ) 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4 :
          (Functor.obj (natAddLEFunctor h) R₁).obj' 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4 ⟶
            (Functor.obj (natAddLEFunctor h) R₂).obj' 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4))
    (h₃ :
      IsIso (X := R₁.obj' (k₀ + 3) ⋯) (Y := R₂.obj' (k₀ + 3) ⋯)
        (app' (Functor.map (natAddLEFunctor h) φ) 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6 :
          (Functor.obj (natAddLEFunctor h) R₁).obj' 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6 ⟶
            (Functor.obj (natAddLEFunctor h) R₂).obj' 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6))
    (h₄ :
      Mono (X := R₁.obj' (k₀ + 4) ⋯) (Y := R₂.obj' (k₀ + 4) ⋯)
        (app' (Functor.map (natAddLEFunctor h) φ) 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7 :
          (Functor.obj (natAddLEFunctor h) R₁).obj' 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7 ⟶
            (Functor.obj (natAddLEFunctor h) R₂).obj' 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7))
    (h₀ :
      Epi (X := R₁.obj' (k₀ + 0) ⋯) (Y := R₂.obj' (k₀ + 0) ⋯)
        (app' (Functor.map (natAddLEFunctor h) φ) 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2 :
          (Functor.obj (natAddLEFunctor h) R₁).obj' 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2 ⟶
            (Functor.obj (natAddLEFunctor h) R₂).obj' 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)),
    IsIso (X := R₁.obj' (k₀ + 2) ⋯) (Y := R₂.obj' (k₀ + 2) ⋯)
      (app' (Functor.map (natAddLEFunctor h) φ) 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)
⊢ IsIso (app' φ (k₀ + 2) ⋯)

Tactic:
rw [← natAddLEFunctor_app' h] at h₀ h₁ h₃ h₄ ⊢

Premises used: CategoryTheory.ComposableArrows.natAddLEFunctor_app'