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 : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
s : ¬(ComplexShape.up ℕ).Rel 0 0
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) 0 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))
        0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp_all
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
n : ℕ
s : ¬(ComplexShape.up ℕ).Rel (n + 1) 0
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) n + 1 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) 0 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))
        n + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp_all
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
s : ¬(ComplexShape.up ℕ).Rel 0 (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) HAdd.hAdd (α := ℕ) 0 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))
        0, HAdd.hAdd (α := ℕ) 0 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) HAdd.hAdd (α := ℕ) 0 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) HAdd.hAdd (α := ℕ) 0 1 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp_all
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
n : ℕ
s : ¬(ComplexShape.up ℕ).Rel (n + 1) (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) n + 1 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) HAdd.hAdd (α := ℕ) 0 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))
        n + 1, HAdd.hAdd (α := ℕ) 0 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) HAdd.hAdd (α := ℕ) 0 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) HAdd.hAdd (α := ℕ) 0 1 with
          | 0 => X
          | i.succ => C.X i :
          V))

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

Tactic:
simp_all
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
j n : ℕ
s : ¬(ComplexShape.up ℕ).Rel (n + 1) (j + 1 + 1)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) n + 1 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) j + 1 + 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))
        n + 1, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) j + 1 + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) j + 1 + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp_all
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
i j k_1 : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k_1
k : ℕ
zero : Eq (α := X ⟶ C.X (HAdd.hAdd (α := ℕ) 0 1)) (f ≫ C.d 0 (HAdd.hAdd (α := ℕ) 0 1)) 0
succ : ∀ (n : ℕ), Eq (α := X ⟶ C.X (n + 1 + 1)) (f ≫ C.d 0 (n + 1 + 1)) 0
⊢ Eq (α := X ⟶ C.X (k + 1)) (f ≫ C.d 0 (k + 1)) 0

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

Tactic:
w
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
⊢ Eq (α := X ⟶ C.X (HAdd.hAdd (α := ℕ) 0 1)) (f ≫ C.d 0 (HAdd.hAdd (α := ℕ) 0 1)) 0

Tactic:
exact w
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n : ℕ
succ : ¬(ComplexShape.up ℕ).Rel 0 (n + 1 + 1)
⊢ Eq (α := X ⟶ C.X (n + 1 + 1)) (f ≫ C.d 0 (n + 1 + 1)) 0

Tactic:
rw [C.shape, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n : ℕ
⊢ ¬1 = n + 1 + 1

Tactic:
(Nat.one_lt_succ_succ _).ne

Premises used: Nat.one_lt_succ_succ, LT.lt.ne
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n : ℕ
⊢ ¬1 = n + 1 + 1

Tactic:
exact (Nat.one_lt_succ_succ _).ne

Premises used: Nat.one_lt_succ_succ, LT.lt.ne
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
⊢ ∀ (k : ℕ), Eq (α := X ⟶ C.X (k + 1)) (f ≫ C.d 0 (k + 1)) 0

Tactic:
have (k : ℕ) : f ≫ C.d 0 (k + 1) = 0 := by
      cases k
      · exact w
      · rw [C.shape, comp_zero]
        simp only [ComplexShape.up_Rel, zero_add]
        exact (Nat.one_lt_succ_succ _).ne
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
this : ∀ (k : ℕ), Eq (α := X ⟶ C.X (k + 1)) (f ≫ C.d 0 (k + 1)) 0
hjk hij : (ComplexShape.up ℕ).Rel 0 0
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V))
    (CategoryStruct.comp (Y :=
        match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i)
        (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))
          0, 0 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0)
        (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))
          0, 0 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0) :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
this : ∀ (k : ℕ), Eq (α := X ⟶ C.X (k + 1)) (f ≫ C.d 0 (k + 1)) 0
hjk : (ComplexShape.up ℕ).Rel 0 0
n : ℕ
hij : (ComplexShape.up ℕ).Rel (n + 1) 0
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) n + 1 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V))
    (CategoryStruct.comp (Y :=
        match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i)
        (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))
          n + 1, 0 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0)
        (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))
          0, 0 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0) :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
this : ∀ (k : ℕ), Eq (α := X ⟶ C.X (k + 1)) (f ≫ C.d 0 (k + 1)) 0
hjk : (ComplexShape.up ℕ).Rel (HAdd.hAdd (α := ℕ) 0 1) 0
hij : (ComplexShape.up ℕ).Rel 0 (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V))
    (CategoryStruct.comp (Y :=
        match (motive := ℕ → V) HAdd.hAdd (α := ℕ) 0 1 with
        | 0 => X
        | i.succ => C.X i)
        (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))
          0, HAdd.hAdd (α := ℕ) 0 1 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0)
        (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))
          HAdd.hAdd (α := ℕ) 0 1, 0 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0) :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
this : ∀ (k : ℕ), Eq (α := X ⟶ C.X (k + 1)) (f ≫ C.d 0 (k + 1)) 0
hjk : (ComplexShape.up ℕ).Rel (HAdd.hAdd (α := ℕ) 0 1) 0
n : ℕ
hij : (ComplexShape.up ℕ).Rel (n + 1) (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) n + 1 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V))
    (CategoryStruct.comp (Y :=
        match (motive := ℕ → V) HAdd.hAdd (α := ℕ) 0 1 with
        | 0 => X
        | i.succ => C.X i)
        (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))
          n + 1, HAdd.hAdd (α := ℕ) 0 1 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0)
        (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))
          HAdd.hAdd (α := ℕ) 0 1, 0 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0) :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) n + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
this : ∀ (k : ℕ), Eq (α := X ⟶ C.X (k + 1)) (f ≫ C.d 0 (k + 1)) 0
j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) 0
hij : (ComplexShape.up ℕ).Rel 0 (j + 1 + 1)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) 0 with
        | 0 => X
        | i.succ => C.X i :
        V))
    (CategoryStruct.comp (Y :=
        match (motive := ℕ → V) j + 1 + 1 with
        | 0 => X
        | i.succ => C.X i)
        (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))
          0, j + 1 + 1 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0)
        (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))
          j + 1 + 1, 0 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0) :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i :
          V))

Tactic:
simp [this]