awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 (j + 1) = 0 ≫ 𝟙 (C.X (j + 1))

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 : ℕ
zero : Eq (α := ℕ) 1 1 → 𝟙 (C.X 1) ≫ C.d 1 0 = C.d 1 0 ≫ 𝟙 (C.X 0)
⊢ (ComplexShape.down ℕ).Rel 1 0 →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 1 ⟶ C.X 0)
      (CategoryStruct.comp (Y := C.X 1)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) 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)))
          (C.d 1 0) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 1 ⟶ 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 1 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 1 ⟶ 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 = 1 → 𝟙 (C.X 1) ≫ C.d 1 (j + 1) = C.d 1 (j + 1) ≫ 𝟙 (C.X (j + 1))
⊢ (ComplexShape.down ℕ).Rel 1 (j + 1) →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 1 ⟶ C.X (j + 1))
      (CategoryStruct.comp (Y := C.X 1)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) 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)))
          (C.d 1 (j + 1)) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 1 ⟶ 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 1 (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 1 ⟶ 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 1 → 𝟙 (C.X 1) ≫ C.d 1 0 = C.d 1 0 ≫ 𝟙 (C.X 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 ℕ
i j : ℕ
⊢ j + 1 + 1 = 1 → 𝟙 (C.X 1) ≫ C.d 1 (j + 1) = C.d 1 (j + 1) ≫ 𝟙 (C.X (j + 1))

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 n : ℕ
zero :
  1 = n + 2 →
    Eq (α := C.X (n + 1 + 1) ⟶ C.X 0) (𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) 0)
      ((match (motive :=
          (x x_1 : ℕ) →
            Quiver.Hom.{v, u} (V := V)
              (match (motive := ℕ → V) x with
                | 0 => C.X 0
                | i.succ => C.X (i + 1) :
                V)
              (match (motive := ℕ → V) x_1 with
                | 0 => C.X 0
                | i.succ => C.X (i + 1) :
                V))
          n + 2, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X 0))
⊢ (ComplexShape.down ℕ).Rel (n + 2) 0 →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 2) ⟶ C.X 0)
      (CategoryStruct.comp (Y := C.X (n + 2))
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x)
            n + 2 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 (n + 2) 0) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 2) ⟶ 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 (n + 2) 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 (n + 2) ⟶ 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 n j : ℕ
succ :
  j + 1 + 1 = n + 2 →
    Eq (α := C.X (n + 1 + 1) ⟶ C.X (j + 1)) (𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) (j + 1))
      ((match (motive :=
          (x x_1 : ℕ) →
            Quiver.Hom.{v, u} (V := V)
              (match (motive := ℕ → V) x with
                | 0 => C.X 0
                | i.succ => C.X (i + 1) :
                V)
              (match (motive := ℕ → V) x_1 with
                | 0 => C.X 0
                | i.succ => C.X (i + 1) :
                V))
          n + 2, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X (j + 1)))
⊢ (ComplexShape.down ℕ).Rel (n + 2) (j + 1) →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 2) ⟶ C.X (j + 1))
      (CategoryStruct.comp (Y := C.X (n + 2))
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x)
            n + 2 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 (n + 2) (j + 1)) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 2) ⟶ 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 (n + 2) (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 (n + 2) ⟶ 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 n : ℕ
⊢ 1 = n + 2 →
    Eq (α := C.X (n + 1 + 1) ⟶ C.X 0) (𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) 0)
      ((match (motive :=
          (x x_1 : ℕ) →
            Quiver.Hom.{v, u} (V := V)
              (match (motive := ℕ → V) x with
                | 0 => C.X 0
                | i.succ => C.X (i + 1) :
                V)
              (match (motive := ℕ → V) x_1 with
                | 0 => C.X 0
                | i.succ => C.X (i + 1) :
                V))
          n + 2, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X 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 ℕ
i n j : ℕ
⊢ j + 1 + 1 = n + 2 →
    Eq (α := C.X (n + 1 + 1) ⟶ C.X (j + 1)) (𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) (j + 1))
      ((match (motive :=
          (x x_1 : ℕ) →
            Quiver.Hom.{v, u} (V := V)
              (match (motive := ℕ → V) x with
                | 0 => C.X 0
                | i.succ => C.X (i + 1) :
                V)
              (match (motive := ℕ → V) x_1 with
                | 0 => C.X 0
                | i.succ => C.X (i + 1) :
                V))
          n + 2, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X (j + 1)))

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 : ℕ
⊢ (ComplexShape.down ℕ).Rel i j →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X i ⟶ C.X j)
      ((match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) i 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 i j :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X i ⟶ C.X j)
      (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d i j ≫
          match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) j 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 i ⟶ C.X j)

Tactic:
match i with
        | 0 | 1 | n + 2 =>
          rcases j with - | j <;> dsimp [augment, truncate] <;> 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 : ℕ
zero :
  (ComplexShape.down ℕ).Rel 0 0 →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 0) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
      (CategoryStruct.comp (Y := C.X 0) (C.d 0 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
succ :
  ∀ (j : ℕ),
    (ComplexShape.down ℕ).Rel 0 (j + 1) →
      Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
        (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
            (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 0 with
            | 0 => 𝟙 (C.X 0)
            | n.succ => 𝟙 (C.X (n + 1)))
            (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 (j + 1)) :
          C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
        (CategoryStruct.comp (Y := C.X (j + 1)) (C.d 0 (j + 1))
            (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x)
              j + 1 with
            | 0 => 𝟙 (C.X 0)
            | n.succ => 𝟙 (C.X (n + 1))) :
          C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
⊢ (ComplexShape.down ℕ).Rel 0 j →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X j)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 j) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X j)
      (C.d 0 j ≫
          match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) j with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X j)

Tactic:
rcases j with - | j
-- 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) ≫ 0 = C.d 0 0 ≫ 𝟙 (C.X 0)
⊢ (ComplexShape.down ℕ).Rel 0 0 →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 0) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
      (CategoryStruct.comp (Y := C.X 0) (C.d 0 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).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) ≫ 0 = C.d 0 (j + 1) ≫ 𝟙 (C.X (j + 1))
⊢ (ComplexShape.down ℕ).Rel 0 (j + 1) →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 (j + 1)) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
      (CategoryStruct.comp (Y := C.X (j + 1)) (C.d 0 (j + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x)
            j + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).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) ≫ 0 = C.d 0 0 ≫ 𝟙 (C.X 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 ℕ
i j : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ 0 = C.d 0 (j + 1) ≫ 𝟙 (C.X (j + 1))

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 : ℕ
zero :
  (ComplexShape.down ℕ).Rel 1 0 →
    Eq.{v + 1} (α := C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 1)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 1 0) :
        C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
      (CategoryStruct.comp (Y := C.X 0) (C.d 1 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
succ :
  ∀ (j : ℕ),
    (ComplexShape.down ℕ).Rel 1 (j + 1) →
      Eq.{v + 1} (α := C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
        (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 1)
            (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 1 with
            | 0 => 𝟙 (C.X 0)
            | n.succ => 𝟙 (C.X (n + 1)))
            (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 1 (j + 1)) :
          C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
        (CategoryStruct.comp (Y := C.X (j + 1)) (C.d 1 (j + 1))
            (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x)
              j + 1 with
            | 0 => 𝟙 (C.X 0)
            | n.succ => 𝟙 (C.X (n + 1))) :
          C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
⊢ (ComplexShape.down ℕ).Rel 1 j →
    Eq.{v + 1} (α := C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X j)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 1)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 1 j) :
        C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X j)
      (C.d 1 j ≫
          match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) j with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)) :
        C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X j)

Tactic:
rcases j with - | j
-- 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 1 → 𝟙 (C.X 1) ≫ C.d 1 0 = C.d 1 0 ≫ 𝟙 (C.X 0)
⊢ (ComplexShape.down ℕ).Rel 1 0 →
    Eq.{v + 1} (α := C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 1)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 1 0) :
        C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
      (CategoryStruct.comp (Y := C.X 0) (C.d 1 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).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 = 1 → 𝟙 (C.X 1) ≫ C.d 1 (j + 1) = C.d 1 (j + 1) ≫ 𝟙 (C.X (j + 1))
⊢ (ComplexShape.down ℕ).Rel 1 (j + 1) →
    Eq.{v + 1} (α := C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 1)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x) 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 1 (j + 1)) :
        C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))
      (CategoryStruct.comp (Y := C.X (j + 1)) (C.d 1 (j + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x)
            j + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 1 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (j + 1))

Tactic:
dsimp [augment, truncate]

Premises used: ChainComplex.truncate, ChainComplex.augment