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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
h₃ : (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₁.sc h₁ i hi))
h₄ : (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₂ = ShortComplex.Hom.τ₂ (𝟙 (S₁.sc h₁ i hi))
h₅ : (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₃ = ShortComplex.Hom.τ₃ (𝟙 (S₁.sc h₁ i hi))
⊢ scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi = 𝟙 (S₁.sc h₁ i hi)

Tactic:
ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₁.sc h₁ i hi))

Tactic:
simp
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₂ = ShortComplex.Hom.τ₂ (𝟙 (S₁.sc h₁ i hi))

Tactic:
simp
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₃ = ShortComplex.Hom.τ₃ (𝟙 (S₁.sc h₁ i hi))

Tactic:
simp
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
h₃ : (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₂.sc h₂ i hi))
h₄ : (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₂ = ShortComplex.Hom.τ₂ (𝟙 (S₂.sc h₂ i hi))
h₅ : (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₃ = ShortComplex.Hom.τ₃ (𝟙 (S₂.sc h₂ i hi))
⊢ scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi = 𝟙 (S₂.sc h₂ i hi)

Tactic:
ext
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₁ = ShortComplex.Hom.τ₁ (𝟙 (S₂.sc h₂ i hi))

Tactic:
simp
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₂ = ShortComplex.Hom.τ₂ (𝟙 (S₂.sc h₂ i hi))

Tactic:
simp
-- 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 S₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₃ = ShortComplex.Hom.τ₃ (𝟙 (S₂.sc h₂ i hi))

Tactic:
simp
-- 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₁ S₂ : ComposableArrows.{v_1, u_1} C n
e : S₁ ≅ S₂
⊢ S₁.Exact ↔ S₂.Exact

Tactic:
⟨exact_of_iso e, exact_of_iso e.symm⟩

Premises used: CategoryTheory.ComposableArrows.exact_of_iso, Iff.intro, CategoryTheory.Iso.symm
-- 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
S : ComposableArrows.{v_1, u_1} C 0
i : ℕ
hi : i + 2 ≤ 0
⊢ ShortComplex.Exact (S.sc ⋯ i hi)

Tactic:
simp at hi
-- 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
S : ComposableArrows.{v_1, u_1} C 1
i : ℕ
hi : i + 2 ≤ 1
exfalso : False
⊢ ShortComplex.Exact (S.sc ⋯ i hi)

Tactic:
exfalso
-- 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
S : ComposableArrows.{v_1, u_1} C 1
i : ℕ
hi : i + 2 ≤ 1
⊢ False

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
S : ComposableArrows.{v_1, u_1} C 2
mp :
  S.IsComplex →
    S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0
mpr :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0 →
    S.IsComplex
⊢ S.IsComplex ↔
    S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0

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
S : ComposableArrows.{v_1, u_1} C 2
h : S.IsComplex
⊢ HAdd.hAdd (α := ℕ) 0 2 ≤ 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
S : ComposableArrows.{v_1, u_1} C 2
h : S.IsComplex
⊢ S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

Tactic:
exact h.zero 0 (by lia)

Premises used: 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
S : ComposableArrows.{v_1, u_1} C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
⊢ S.IsComplex

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

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

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

Premises used: CategoryTheory.ComposableArrows.IsComplex.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
S : ComposableArrows.{v_1, u_1} C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
i : ℕ
hi : i + 2 ≤ 2
⊢ i = 0

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
S : ComposableArrows.{v_1, u_1} C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
i : ℕ
hi : i + 2 ≤ 2
mpr :
  ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ 2),
    Eq (α := S.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 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 (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
      (0 : S.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
⊢ Eq (α := S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi :
      S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)
    (0 : S.obj (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨i + 2, ⋯⟩)

Tactic:
obtain rfl : i = 0 := by lia

Premises used: 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
S : ComposableArrows.{v_1, u_1} C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
hi : HAdd.hAdd (α := ℕ) 0 2 ≤ 2
⊢ Eq (α := S.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 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 (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)
    (0 : S.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ S.obj ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩)

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

Tactic:
exact h
-- 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
S : ComposableArrows.{v_1, u_1} C 2
w :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
⊢ S.IsComplex

Tactic:
S.isComplex₂_iff.2 w

Premises used: Iff.mpr, 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
S : ShortComplex.{v_1, u_1} C
⊢ S.toComposableArrows.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.toComposableArrows.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

Tactic:
simp [-Fin.reduceFinMk]

Premises used: Fin.reduceFinMk
-- 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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
mp : S.Exact → (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
mpr : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact → S.Exact
⊢ S.Exact ↔ (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : S.Exact
⊢ HAdd.hAdd (α := ℕ) 0 2 ≤ 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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : S.Exact
⊢ (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
⊢ S.Exact

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

Premises used: 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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
mpr : ∀ (i : ℕ) (hi : i + 2 ≤ 2), (S.sc hS i hi).Exact
⊢ S.Exact

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

Premises used: 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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
i : ℕ
hi : i + 2 ≤ 2
⊢ i = 0

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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
i : ℕ
hi : i + 2 ≤ 2
mpr : ∀ (hi : HAdd.hAdd (α := ℕ) 0 2 ≤ 2), (S.sc hS 0 hi).Exact
⊢ (S.sc hS i hi).Exact

Tactic:
obtain rfl : i = 0 := by lia

Premises used: 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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
hi : HAdd.hAdd (α := ℕ) 0 2 ≤ 2
⊢ (S.sc hS 0 hi).Exact

Tactic:
h
-- 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
S : ComposableArrows.{v_1, u_1} C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
hi : HAdd.hAdd (α := ℕ) 0 2 ≤ 2
⊢ (S.sc hS 0 hi).Exact

Tactic:
exact h
-- 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
S : ComposableArrows.{v_1, u_1} C 2
w :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
h :
  { X₁ := S.obj ⟨0, ⋯⟩, X₂ := S.obj ⟨1, ⋯⟩, X₃ := S.obj ⟨2, ⋯⟩,
      f := S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g := S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5, zero := w : ShortComplex.{v_1, u_1} C }.Exact
⊢ S.Exact

Tactic:
(S.exact₂_iff (S.isComplex₂_mk w)).2 h

Premises used: Iff.mpr, CategoryTheory.ComposableArrows.isComplex₂_mk, 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
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
⊢ S.toComposableArrows.Exact

Tactic:
exact₂_mk _ _ hS

Premises used: 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
S : ShortComplex.{v_1, u_1} C
⊢ S.Exact ↔ S.toComposableArrows.Exact

Tactic:
(S.toComposableArrows.exact₂_iff S.isComplex_toComposableArrows).symm

Premises used: CategoryTheory.ShortComplex.isComplex_toComposableArrows, CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ShortComplex.toComposableArrows, CategoryTheory.ComposableArrows.exact₂_iff, CategoryTheory.ComposableArrows.Mk₁.map, CategoryTheory.ComposableArrows.Precomp.map, Iff.symm
-- 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 →
    (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
mpr :
  (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
⊢ 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 : S.Exact
mp :
  (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
mp₁ : 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 : S.Exact
mp :
  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)
mp₁ :
  (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)))).IsComplex
⊢ (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:
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 (⟨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
⊢ (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)))).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 (⟨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:
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