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
this : ∀ (k : ℕ), Eq (α := X ⟶ C.X (k + 1)) (f ≫ C.d 0 (k + 1)) 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel (HAdd.hAdd (α := ℕ) 0 1) (k + 1 + 1)
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) k + 1 + 1 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, k + 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) k + 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) k + 1 + 1 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
k j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (k + 1 + 1)
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) k + 1 + 1 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, k + 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) k + 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) k + 1 + 1 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
k j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (k + 1 + 1)
n : ℕ
hij : (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) k + 1 + 1 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))
          n + 1, 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, k + 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) k + 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) k + 1 + 1 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
⊢ (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 : 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 : ℕ
⊢ (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 : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
⊢ (C.augment f w).d 0 1 = 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 : 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 : ℕ
⊢ (C.augment f w).d (i + 1) (j + 1) = C.d i j

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 : 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 : ℕ
zero : (ComplexShape.up ℕ).Rel i 0 → 𝟙 (C.X i) ≫ (Functor.obj truncate (C.augment f w)).d i 0 = C.d i 0 ≫ 𝟙 (C.X 0)
succ :
  ∀ (n : ℕ),
    (ComplexShape.up ℕ).Rel i (n + 1) →
      𝟙 (C.X i) ≫ (Functor.obj truncate (C.augment f w)).d i (n + 1) = C.d i (n + 1) ≫ 𝟙 (C.X (n + 1))
⊢ (ComplexShape.up ℕ).Rel i j → 𝟙 (C.X i) ≫ (Functor.obj truncate (C.augment f w)).d i j = C.d i j ≫ 𝟙 (C.X j)

Tactic:
cases j
-- 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 : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 → 𝟙 (C.X i) ≫ (Functor.obj truncate (C.augment f w)).d i 0 = C.d i 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 : 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 n : ℕ
⊢ (ComplexShape.up ℕ).Rel i (n + 1) →
    𝟙 (C.X i) ≫ (Functor.obj truncate (C.augment f w)).d i (n + 1) = C.d i (n + 1) ≫ 𝟙 (C.X (n + 1))

Tactic:
simp
-- 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
h :
  ∀ (i : ℕ),
    Hom.f
        ({ f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
            Hom (Functor.obj truncate (C.augment f w)) C } ≫
          { f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ })
        i =
      Hom.f (𝟙 (Functor.obj truncate (C.augment f w))) i
⊢ { f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
        Hom (Functor.obj truncate (C.augment f w)) C } ≫
      { f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ } =
    𝟙 (Functor.obj truncate (C.augment f w))

Tactic:
ext i
-- 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 : ℕ
h :
  Eq (α := (Functor.obj truncate (C.augment f w)).X 0 ⟶ (Functor.obj truncate (C.augment f w)).X 0)
    (Hom.f
      ({ f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
          Hom (Functor.obj truncate (C.augment f w)) C } ≫
        { f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ })
      0)
    (Hom.f (𝟙 (Functor.obj truncate (C.augment f w))) 0)
h₁ :
  ∀ (n : ℕ),
    Hom.f
        ({ f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
            Hom (Functor.obj truncate (C.augment f w)) C } ≫
          { f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ })
        (n + 1) =
      Hom.f (𝟙 (Functor.obj truncate (C.augment f w))) (n + 1)
⊢ Hom.f
      ({ f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
          Hom (Functor.obj truncate (C.augment f w)) C } ≫
        { f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ })
      i =
    Hom.f (𝟙 (Functor.obj truncate (C.augment f w))) i

Tactic:
cases i
-- 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
⊢ Eq (α := (Functor.obj truncate (C.augment f w)).X 0 ⟶ (Functor.obj truncate (C.augment f w)).X 0)
    (Hom.f
      ({ f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
          Hom (Functor.obj truncate (C.augment f w)) C } ≫
        { f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ })
      0)
    (Hom.f (𝟙 (Functor.obj truncate (C.augment f w))) 0)

Tactic:
simp
-- 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 : ℕ
⊢ Hom.f
      ({ f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
          Hom (Functor.obj truncate (C.augment f w)) C } ≫
        { f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ })
      (n + 1) =
    Hom.f (𝟙 (Functor.obj truncate (C.augment f w))) (n + 1)

Tactic:
simp
-- 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
h :
  ∀ (i : ℕ),
    Hom.f
        ({ f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ } ≫
          { f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
            Hom (Functor.obj truncate (C.augment f w)) C })
        i =
      Hom.f (𝟙 C) i
⊢ { f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ } ≫
      { f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
        Hom (Functor.obj truncate (C.augment f w)) C } =
    𝟙 C

Tactic:
ext i
-- 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 : ℕ
h :
  Eq (α := C.X 0 ⟶ C.X 0)
    (Hom.f
      ({ f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ } ≫
        { f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
          Hom (Functor.obj truncate (C.augment f w)) C })
      0)
    (Hom.f (𝟙 C) 0)
h₁ :
  ∀ (n : ℕ),
    Hom.f
        ({ f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ } ≫
          { f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
            Hom (Functor.obj truncate (C.augment f w)) C })
        (n + 1) =
      Hom.f (𝟙 C) (n + 1)
⊢ Hom.f
      ({ f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ } ≫
        { f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
          Hom (Functor.obj truncate (C.augment f w)) C })
      i =
    Hom.f (𝟙 C) i

Tactic:
cases i
-- 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
⊢ Eq (α := C.X 0 ⟶ C.X 0)
    (Hom.f
      ({ f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ } ≫
        { f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
          Hom (Functor.obj truncate (C.augment f w)) C })
      0)
    (Hom.f (𝟙 C) 0)

Tactic:
simp
-- 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 : ℕ
⊢ Hom.f
      ({ f := fun (x : ℕ) ↦ 𝟙 (C.X x), comm' := ⋯ } ≫
        { f := fun (x : ℕ) ↦ 𝟙 ((Functor.obj truncate (C.augment f w)).X x), comm' := ⋯ :
          Hom (Functor.obj truncate (C.augment f w)) C })
      (n + 1) =
    Hom.f (𝟙 C) (n + 1)

Tactic:
simp
-- 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 : ℕ
⊢ (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 : 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 : ℕ
⊢ (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 : CochainComplex.{v, u, 0} V ℕ
i : ℕ
a : ¬(ComplexShape.up ℕ).Rel 0 (i + 2)
⊢ Eq (α := C.X 0 ⟶ C.X (i + 2)) (C.d 0 (i + 2)) 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 : CochainComplex.{v, u, 0} V ℕ
i : ℕ
⊢ ¬1 = i + 2

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 ℕ
i : ℕ
⊢ ¬1 = i + 2

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

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

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

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

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

Tactic:
aesop