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

Tactic:
rcases i with - | i