Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i 0 =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

pp: case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i (0 + 1) →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i (0 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i (0 + 1) ≫
        match 0 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

pp: case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i (j + 1 + 1) →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i (j + 1 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i (j + 1 + 1) ≫
        match j + 1 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i 0 =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i (0 + 1) →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i (0 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i (0 + 1) ≫
        match 0 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i (j + 1 + 1) →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i (j + 1 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i (j + 1 + 1) ≫
        match j + 1 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))