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
⊢ (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
            S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
              S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).map'
        0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
            S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
            (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
              S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).map'
        1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

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.Exact
⊢ HAdd.hAdd (α := ℕ) 0 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 (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
          S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
          (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
            S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨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 0 (by lia)

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)
h : S.Exact
⊢ S.δ₀.Exact

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

Premises used: CategoryTheory.ComposableArrows.IsComplex.mk, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.Exact.mk, HAdd.hAdd, OfNat.ofNat, 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
⊢ S.δ₀.Exact

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

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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 2 ≤ n + 2
mpr :
  ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2),
    Eq (α := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
      (S.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ ⋯ ≫ S.map' (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2) ⋯ hi :
        S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
      (0 : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
mpr₁ :
  ∀ (i : ℕ) (hi : i + 1 + 2 ≤ n + 2),
    Eq (α := S.obj (⟨i + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, ⋯⟩)
      (S.map' (i + 1) (i + 1 + 1) ⋯ ⋯ ≫ S.map' (i + 1 + 1) (i + 1 + 2) ⋯ hi :
        S.obj (⟨i + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, ⋯⟩)
      (0 : S.obj (⟨i + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 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, ⋯⟩)

Tactic:
obtain _ | i := i
-- 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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2
⊢ Eq (α := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
    (S.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ ⋯ ≫ S.map' (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2) ⋯ hi :
      S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
    (0 : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 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
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2
⊢ Eq (α := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
    (S.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ ⋯ ≫ S.map' (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2) ⋯ hi :
      S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
    (0 : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 1 + 2 ≤ n + 2
⊢ Eq (α := S.obj (⟨i + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, ⋯⟩)
    (S.map' (i + 1) (i + 1 + 1) ⋯ ⋯ ≫ S.map' (i + 1 + 1) (i + 1 + 2) ⋯ hi :
      S.obj (⟨i + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, ⋯⟩)
    (0 : S.obj (⟨i + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, ⋯⟩)

Tactic:
h₀.toIsComplex.zero i

Premises used: Fin.succ, 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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 1 + 2 ≤ n + 2
⊢ Eq (α := S.obj (⟨i + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, ⋯⟩)
    (S.map' (i + 1) (i + 1 + 1) ⋯ ⋯ ≫ S.map' (i + 1 + 1) (i + 1 + 2) ⋯ hi :
      S.obj (⟨i + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 2, ⋯⟩)
    (0 : S.obj (⟨i + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj ⟨i + 1 + 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
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 2 ≤ n + 2
mpr : ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2), ShortComplex.Exact (S.sc ⋯ 0 hi)
mpr₁ : ∀ (i : ℕ) (hi : i + 1 + 2 ≤ n + 2), ShortComplex.Exact (S.sc ⋯ (i + 1) hi)
⊢ ShortComplex.Exact (S.sc ⋯ i hi)

Tactic:
obtain _ | i := i
-- 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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2
⊢ ShortComplex.Exact (S.sc ⋯ 0 hi)

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
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
hi : HAdd.hAdd (α := ℕ) 0 2 ≤ n + 2
⊢ ShortComplex.Exact (S.sc ⋯ 0 hi)

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)
h :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 1 + 2 ≤ n + 2
⊢ ShortComplex.Exact (S.sc ⋯ (i + 1) hi)

Tactic:
h₀.exact i

Premises used: Fin.succ, 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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : i + 1 + 2 ≤ n + 2
⊢ ShortComplex.Exact (S.sc ⋯ (i + 1) hi)

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
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
hS : S.Exact
⊢ (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
          S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
    S.δ₀.Exact

Tactic:
rw [exact_iff_δ₀] at hS

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)
hS :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
          S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
    S.δ₀.Exact
⊢ S.δ₀.Exact

Tactic:
hS.2

Premises used: And.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)
hS :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
          S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
    S.δ₀.Exact
⊢ S.δ₀.Exact

Tactic:
exact hS.2

Premises used: And.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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
rw :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
          S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
    S.δ₀.Exact
⊢ S.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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
left :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
right : S.δ₀.Exact
⊢ (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
        S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
        (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
          S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact ∧
    S.δ₀.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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
⊢ (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact

Tactic:
assumption
-- 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 :
  (mk₂ (X₀ := S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1))) (X₂ :=
      S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 0 1 isComplex₂_iff._proof_2 ⋯ : S.obj (⟨0, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' 1 2 isComplex₂_iff._proof_4 ⋯ :
        S.obj (⟨1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
h₀ : S.δ₀.Exact
⊢ S.δ₀.Exact

Tactic:
assumption
-- 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)
mp :
  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
mpr :
  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
⊢ 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:
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.Exact
mp : S.δlast.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)))).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.Exact
⊢ S.δlast.Exact

Tactic:
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