awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ S.δlast.Exact

Tactic:
exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero i))
        (fun i hi => h.exact i)

Premises used: CategoryTheory.ComposableArrows.IsComplex.mk, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.Exact.mk, CategoryTheory.ComposableArrows.IsComplex.zero, CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
mp :
  ShortComplex.Exact
    ((mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' (n + 1) (n + 2) ⋯ ⋯ :
            S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).sc'
      ⋯ 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5)
mp₁ :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ :
        S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).IsComplex
⊢ (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact

Tactic:
rw [exact₂_iff]

Premises used: CategoryTheory.ComposableArrows.exact₂_iff
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
mp :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' (n + 1) (n + 2) ⋯ ⋯ :
              S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).map'
        0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' (n + 1) (n + 2) ⋯ ⋯ :
              S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).map'
        1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
⊢ (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ :
        S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).IsComplex

Tactic:
rw [isComplex₂_iff]

Premises used: CategoryTheory.ComposableArrows.isComplex₂_iff
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' (n + 1) (n + 2) ⋯ ⋯ :
              S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).map'
        0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' (n + 1) (n + 2) ⋯ ⋯ :
              S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).map'
        1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

Tactic:
h.toIsComplex.zero n

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.Mk₁.map, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' (n + 1) (n + 2) ⋯ ⋯ :
              S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).map'
        0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' (n + 1) (n + 2) ⋯ ⋯ :
              S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).map'
        1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

Tactic:
exact h.toIsComplex.zero n

Premises used: CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ n + 2 ≤ n + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.Exact
⊢ ShortComplex.Exact
    ((mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' (n + 1) (n + 2) ⋯ ⋯ :
            S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).sc'
      ⋯ 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5)

Tactic:
exact h.exact n (by lia)

Premises used: CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
⊢ S.Exact

Tactic:
Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)

Premises used: CategoryTheory.ComposableArrows.IsComplex.mk, CategoryTheory.ComposableArrows.Exact.mk
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
mpr :
  ∀ (i : ℕ) (hi : i + 2 ≤ n + 2),
    Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
mpr₁ : ∀ (i : ℕ) (hi : i + 2 ≤ n + 2), ShortComplex.Exact (S.sc ⋯ i hi)
⊢ S.Exact

Tactic:
refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)

Premises used: CategoryTheory.ComposableArrows.IsComplex.mk, CategoryTheory.ComposableArrows.Exact.mk
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ i ≤ n

Tactic:
simp only [Nat.add_le_add_iff_right] at hi

Premises used: Nat.add_le_add_iff_right
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi : i ≤ n
mpr :
  ∀ (hi : i < n),
    Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi_1 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
mpr₁ :
  ∀ (S : ComposableArrows.{v_1, u_1} C (i + 2)) (h : S.δlast.Exact)
    (h' :
      (mk₂ (X₀ := S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1))) (X₁ := S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
          (S.map' i (i + 1) ⋯ ⋯ : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
          (S.map' (i + 1) (i + 2) ⋯ ⋯ :
            S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 2, ⋯⟩ : Fin (i + 2 + 1)))).Exact)
    (hi : i + 2 ≤ i + 2) (hi_2 : i ≤ i),
    Eq (α := S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
      (0 : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi_1 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)

Tactic:
obtain hi | rfl := hi.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi_2 : i ≤ n
hi : i < n
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi_1 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)

Tactic:
h.toIsComplex.zero i

Premises used: CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.homOfLE, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi_2 : i ≤ n
hi : i < n
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi_1 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)

Tactic:
exact h.toIsComplex.zero i

Premises used: CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
i : ℕ
S : ComposableArrows.{v_1, u_1} C (i + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1))) (X₁ := S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
      (S.map' i (i + 1) ⋯ ⋯ : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
      (S.map' (i + 1) (i + 2) ⋯ ⋯ : S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 2, ⋯⟩ : Fin (i + 2 + 1)))).Exact
hi_1 : i + 2 ≤ i + 2
hi : i ≤ i
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi_1 : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)

Tactic:
h'.toIsComplex.zero 0

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
i : ℕ
S : ComposableArrows.{v_1, u_1} C (i + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1))) (X₁ := S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
      (S.map' i (i + 1) ⋯ ⋯ : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
      (S.map' (i + 1) (i + 2) ⋯ ⋯ : S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 2, ⋯⟩ : Fin (i + 2 + 1)))).Exact
hi_1 : i + 2 ≤ i + 2
hi : i ≤ i
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi_1 : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)

Tactic:
exact h'.toIsComplex.zero 0

Premises used: CategoryTheory.ComposableArrows.Exact.toIsComplex, OfNat.ofNat, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi : i ≤ n
mpr : ∀ (hi : i < n), ShortComplex.Exact (S.sc ⋯ i hi_1)
mpr₁ :
  ∀ (S : ComposableArrows.{v_1, u_1} C (i + 2)) (h : S.δlast.Exact)
    (h' :
      (mk₂ (X₀ := S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1))) (X₁ := S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
          (S.map' i (i + 1) ⋯ ⋯ : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
          (S.map' (i + 1) (i + 2) ⋯ ⋯ :
            S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 2, ⋯⟩ : Fin (i + 2 + 1)))).Exact)
    (hi : i + 2 ≤ i + 2) (hi_2 : i ≤ i), ShortComplex.Exact (S.sc ⋯ i hi)
⊢ ShortComplex.Exact (S.sc ⋯ i hi_1)

Tactic:
obtain hi | rfl := hi.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi_2 : i ≤ n
hi : i < n
⊢ ShortComplex.Exact (S.sc ⋯ i hi_1)

Tactic:
h.exact i

Premises used: CategoryTheory.homOfLE, CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
i : ℕ
hi_1 : i + 2 ≤ n + 2
hi_2 : i ≤ n
hi : i < n
⊢ ShortComplex.Exact (S.sc ⋯ i hi_1)

Tactic:
exact h.exact i

Premises used: CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
i : ℕ
S : ComposableArrows.{v_1, u_1} C (i + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1))) (X₁ := S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
      (S.map' i (i + 1) ⋯ ⋯ : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
      (S.map' (i + 1) (i + 2) ⋯ ⋯ : S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 2, ⋯⟩ : Fin (i + 2 + 1)))).Exact
hi_1 : i + 2 ≤ i + 2
hi : i ≤ i
⊢ ShortComplex.Exact (S.sc ⋯ i hi_1)

Tactic:
h'.exact 0

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
i : ℕ
S : ComposableArrows.{v_1, u_1} C (i + 2)
h : S.δlast.Exact
h' :
  (mk₂ (X₀ := S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1))) (X₁ := S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
      (S.map' i (i + 1) ⋯ ⋯ : S.obj (⟨i, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)))
      (S.map' (i + 1) (i + 2) ⋯ ⋯ : S.obj (⟨i + 1, ⋯⟩ : Fin (i + 2 + 1)) ⟶ S.obj (⟨i + 2, ⋯⟩ : Fin (i + 2 + 1)))).Exact
hi_1 : i + 2 ≤ i + 2
hi : i ≤ i
⊢ ShortComplex.Exact (S.sc ⋯ i hi_1)

Tactic:
exact h'.exact 0

Premises used: OfNat.ofNat, CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
hS : S.Exact
⊢ S.δlast.Exact ∧
    (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) ⋯ ⋯ :
          S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact

Tactic:
rw [exact_iff_δlast] at hS

Premises used: CategoryTheory.ComposableArrows.exact_iff_δlast
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
hS :
  S.δlast.Exact ∧
    (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) ⋯ ⋯ :
          S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
⊢ S.δlast.Exact

Tactic:
hS.1

Premises used: And.left
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
hS :
  S.δlast.Exact ∧
    (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) ⋯ ⋯ :
          S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
⊢ S.δlast.Exact

Tactic:
exact hS.1

Premises used: And.left
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h₁ : S.δlast.Exact
h₂ :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
rw :
  S.δlast.Exact ∧
    (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) ⋯ ⋯ :
          S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
⊢ S.Exact

Tactic:
rw [exact_iff_δlast]

Premises used: CategoryTheory.ComposableArrows.exact_iff_δlast
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h₁ : S.δlast.Exact
h₂ :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
left : S.δlast.Exact
right :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
⊢ S.δlast.Exact ∧
    (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' (n + 1) (n + 2) ⋯ ⋯ :
          S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h₁ : S.δlast.Exact
h₂ :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
⊢ S.δlast.Exact

Tactic:
assumption