awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
h : ¬Even i
⊢ Eq (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) i j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i j ≫ f)

Tactic:
simp_all [-Nat.not_even_iff_odd]

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : Even n
h₀ : n ≠ 0
⊢ Eq.{v_1 + 1} (α :=
    ShortComplex.X₁.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n) ⟶
      ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n))
    (ShortComplex.f (HomologicalComplex.sc (Functor.obj alternatingConst X) n)) 0

Tactic:
simp [Nat.even_add_one, hn]

Premises used: Nat.even_add_one
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : Even n
h₀ : n ≠ 0
zero :
  ∀ (hn : Even (α := ℕ) 0) (h₀ : Ne (α := ℕ) 0 0) (Z : C)
    (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) 0)),
    g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) 0) = 0 → g = 0
succ :
  ∀ (n : ℕ) (hn : Even (n + 1)) (h₀ : n + 1 ≠ 0) (Z : C)
    (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) (n + 1))),
    g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) (n + 1)) = 0 → g = 0
⊢ ∀ (Z : C) (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n)),
    g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) n) = 0 → g = 0

Tactic:
cases n
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
hn : Even (α := ℕ) 0
h₀ : Ne (α := ℕ) 0 0
⊢ ∀ (Z : C) (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) 0)),
    g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) 0) = 0 → g = 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : Even (n + 1)
h₀ : n + 1 ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) (n + 1))),
    g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) (n + 1)) = 0 → g = 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : Odd n
⊢ Eq.{v_1 + 1} (α :=
    ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n) ⟶
      ShortComplex.X₃.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n))
    (ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) n)) 0

Tactic:
simp [hn]
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : Odd n
⊢ ∀ (Z : C) (g : ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n) ⟶ Z),
    ShortComplex.f (HomologicalComplex.sc (Functor.obj alternatingConst X) n) ≫ g = 0 → g = 0

Tactic:
simp [hn]
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : n = 0
⊢ Eq.{v_1 + 1} (α :=
    ShortComplex.X₁.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n) ⟶
      ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n))
    (ShortComplex.f (HomologicalComplex.sc (Functor.obj alternatingConst X) n)) 0

Tactic:
simp [hn]
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : n = 0
⊢ Eq.{v_1 + 1} (α :=
    ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n) ⟶
      ShortComplex.X₃.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n))
    (ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) n)) 0

Tactic:
simp [hn]
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
inl : ∀ (h : Even n), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
inr : ∀ (h : Odd n), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n

Tactic:
rcases n.even_or_odd with h | h

Premises used: Nat.even_or_odd
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
h : Even n
inl : ∀ (h : Even (α := ℕ) 0), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) 0
inl₁ :
  ∀ (n : ℕ) (h : Even (n + 1)), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) (n + 1)
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n

Tactic:
rcases n with - | n
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
h : Even (α := ℕ) 0
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) 0

Tactic:
⟨⟨alternatingConstHomologyDataZero X _ rfl⟩⟩

Premises used: Nonempty.intro, CategoryTheory.ShortComplex.HasHomology.mk, ChainComplex.alternatingConstHomologyDataZero, rfl
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
h : Even (α := ℕ) 0
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) 0

Tactic:
exact ⟨⟨alternatingConstHomologyDataZero X _ rfl⟩⟩
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
h : Even (n + 1)
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
h : Even (n + 1)
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) (n + 1)

Tactic:
exact ⟨⟨alternatingConstHomologyDataEvenNEZero X _ h (by simp)⟩⟩
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
h : Odd n
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n

Tactic:
⟨⟨alternatingConstHomologyDataOdd X _ h⟩⟩

Premises used: Nonempty.intro, CategoryTheory.ShortComplex.HasHomology.mk, ChainComplex.alternatingConstHomologyDataOdd
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
h : Odd n
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n

Tactic:
exact ⟨⟨alternatingConstHomologyDataOdd X _ h⟩⟩
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : n ≠ 0
inl : ∀ (h : Even n), HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
inr : ∀ (h : Odd n), HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
⊢ HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n

Tactic:
rcases n.even_or_odd with h | h

Premises used: Nat.even_or_odd
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : n ≠ 0
h : Even n
⊢ HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n

Tactic:
⟨(alternatingConstHomologyDataEvenNEZero X _ h hn), isZero_zero C⟩

Premises used: CategoryTheory.ShortComplex.Exact.mk, HomologicalComplex.ExactAt, CategoryTheory.Limits.isZero_zero, Exists.intro, ChainComplex.alternatingConstHomologyDataEvenNEZero
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : n ≠ 0
h : Even n
⊢ HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n

Tactic:
exact ⟨(alternatingConstHomologyDataEvenNEZero X _ h hn), isZero_zero C⟩
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n

Tactic:
⟨(alternatingConstHomologyDataOdd X _ h), isZero_zero C⟩

Premises used: CategoryTheory.ShortComplex.Exact.mk, HomologicalComplex.ExactAt, CategoryTheory.Limits.isZero_zero, Exists.intro, ChainComplex.alternatingConstHomologyDataOdd
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n

Tactic:
exact ⟨(alternatingConstHomologyDataOdd X _ h), isZero_zero C⟩
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
i : ℕ
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
        (i + 1) ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (Functor.obj ChainComplex.alternatingConst X) i)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_1, u_1, 0} (Functor.obj ChainComplex.alternatingConst X) (i + 1))
      (Iso.hom
        ((fun (x : ℕ) ↦
            (Iso.refl
                (HomologicalComplex.X.{v_1, u_1, 0}
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x) :
              HomologicalComplex.X.{v_1, u_1, 0}
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x ≅
                HomologicalComplex.X.{v_1, u_1, 0}
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x))
          (i + 1)))
      (HomologicalComplex.d (Functor.obj ChainComplex.alternatingConst X) (i + 1) i))
    (HomologicalComplex.d (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) (i + 1) i ≫
      Iso.hom
        ((fun (x : ℕ) ↦
            (Iso.refl
                (HomologicalComplex.X.{v_1, u_1, 0}
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x) :
              HomologicalComplex.X.{v_1, u_1, 0}
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x ≅
                HomologicalComplex.X.{v_1, u_1, 0}
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x))
          i))

Tactic:
simp [SimplicialObject.δ, ← Finset.sum_smul, Fin.sum_neg_one_pow, Nat.even_add_one,
      -Nat.not_even_iff_odd]

Premises used: Nat.even_add_one, Finset.sum_smul, Fin.sum_neg_one_pow, Nat.not_even_iff_odd, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X Y : C
f : X ⟶ Y
i : ℕ
⊢ Eq (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
        i ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (Functor.obj ChainComplex.alternatingConst Y) i)
    (HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) f ≫
        Iso.hom
          ((fun (X : C) ↦
              (HomologicalComplex.Hom.isoOfComponents
                  (fun (x : ℕ) ↦
                    Iso.refl
                      (HomologicalComplex.X.{v_1, u_1, 0}
                        (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x))
                  ⋯ :
                Iso (C := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ))
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
                  (Functor.obj ChainComplex.alternatingConst X)))
            Y))
      i)
    (HomologicalComplex.Hom.f
      (Iso.hom
          ((fun (X : C) ↦
              (HomologicalComplex.Hom.isoOfComponents
                  (fun (x : ℕ) ↦
                    Iso.refl
                      (HomologicalComplex.X.{v_1, u_1, 0}
                        (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x))
                  ⋯ :
                Iso (C := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ))
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
                  (Functor.obj ChainComplex.alternatingConst X)))
            X) ≫
        CategoryTheory.Functor.map ChainComplex.alternatingConst f)
      i)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
i j : ℕ
w : ¬(ComplexShape.down ℕ).Rel i j
⊢ ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroObject.{v, u} V
inst_2 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
⊢ Eq (α := (Functor.obj truncate C).X 1 ⟶ C.X 0)
    (CategoryStruct.comp (Y := (Functor.obj truncate C).X 0) ((Functor.obj truncate C).d 1 0) (C.d 1 0)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i j : ℕ
h : ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)
simp : C.d i j = 0
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) i + 1 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) j + 1 with
        | 0 => X
        | i.succ => C.X i :
        V))
    (match (motive :=
        (x x_1 : ℕ) →
          Quiver.Hom.{v, u} (V := V)
            (match (motive := ℕ → V) x with
              | 0 => X
              | i.succ => C.X i :
              V)
            (match (motive := ℕ → V) x_1 with
              | 0 => X
              | i.succ => C.X i :
              V))
        i + 1, j + 1 with
      | 1, 0 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) j + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) j + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp only
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i j : ℕ
h : ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)
⊢ C.d i j = 0

Tactic:
C.shape i j (Nat.succ_ne_succ_iff.1 h)

Premises used: Nat.succ_ne_succ_iff, Iff.mp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i j : ℕ
h : ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)
⊢ C.d i j = 0

Tactic:
exact C.shape i j (Nat.succ_ne_succ_iff.1 h)

Premises used: Nat.succ_ne_succ_iff, Iff.mp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
⊢ (C.augment f w).X 0 = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i : ℕ
⊢ (C.augment f w).X (i + 1) = C.X i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
⊢ (C.augment f w).d 1 0 = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i j : ℕ
zero :
  Eq (α := (C.augment f w).X (HAdd.hAdd (α := ℕ) 0 1) ⟶ (C.augment f w).X (j + 1))
    ((C.augment f w).d (HAdd.hAdd (α := ℕ) 0 1) (j + 1)) (C.d 0 j)
succ :
  ∀ (n : ℕ),
    Eq (α := (C.augment f w).X (n + 1 + 1) ⟶ (C.augment f w).X (j + 1)) ((C.augment f w).d (n + 1 + 1) (j + 1))
      (C.d (n + 1) j)
⊢ (C.augment f w).d (i + 1) (j + 1) = C.d i j

Tactic:
cases i
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
j : ℕ
⊢ Eq (α := (C.augment f w).X (HAdd.hAdd (α := ℕ) 0 1) ⟶ (C.augment f w).X (j + 1))
    ((C.augment f w).d (HAdd.hAdd (α := ℕ) 0 1) (j + 1)) (C.d 0 j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
j n : ℕ
⊢ Eq (α := (C.augment f w).X (n + 1 + 1) ⟶ (C.augment f w).X (j + 1)) ((C.augment f w).d (n + 1 + 1) (j + 1))
    (C.d (n + 1) j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i : ℕ
⊢ (C.truncateAugment f w).hom.f i = 𝟙 (C.X i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i : ℕ
⊢ (C.truncateAugment f w).inv.f i = 𝟙 ((Functor.obj truncate (C.augment f w)).X i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
i : ℕ
a : ¬(ComplexShape.down ℕ).Rel (i + 2) 0
⊢ Eq (α := C.X (i + 2) ⟶ C.X 0) (C.d (i + 2) 0) 0

Tactic:
rw [C.shape]

Premises used: HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
i : ℕ
⊢ ¬(ComplexShape.down ℕ).Rel (i + 2) 0

Tactic:
i.succ_succ_ne_one.symm

Premises used: Ne.symm, Nat.succ_succ_ne_one
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
i : ℕ
⊢ ¬(ComplexShape.down ℕ).Rel (i + 2) 0

Tactic:
exact i.succ_succ_ne_one.symm

Premises used: Ne.symm, Nat.succ_succ_ne_one
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
i : ℕ
zero : Eq (α := ℕ) 1 0 → 𝟙 (C.X 0) ≫ C.d 0 0 = 0 ≫ 𝟙 (C.X 0)
⊢ (ComplexShape.down ℕ).Rel 0 0 →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X 0)
      (CategoryStruct.comp (Y := C.X 0)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) 0 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1)))
          (C.d 0 0) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 0)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) 0 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1))) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X 0)

Tactic:
dsimp [augment, truncate]

Premises used: ChainComplex.truncate, ChainComplex.augment
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
i j : ℕ
succ : j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 (j + 1) = 0 ≫ 𝟙 (C.X (j + 1))
⊢ (ComplexShape.down ℕ).Rel 0 (j + 1) →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X (j + 1))
      (CategoryStruct.comp (Y := C.X 0)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) 0 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1)))
          (C.d 0 (j + 1)) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X (j + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 (j + 1))
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x)
            j + 1 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1))) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X (j + 1))

Tactic:
dsimp [augment, truncate]

Premises used: ChainComplex.truncate, ChainComplex.augment
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
i : ℕ
⊢ Eq (α := ℕ) 1 0 → 𝟙 (C.X 0) ≫ C.d 0 0 = 0 ≫ 𝟙 (C.X 0)

Tactic:
simp