mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Augment

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 0 = 0 ≫ 𝟙 (C.X 0)

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 (j + 1) = 0 ≫ 𝟙 (C.X (j + 1))

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 0 = 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 (j + 1) = 0 ≫ 𝟙 (C.X (j + 1))
Module: Mathlib.Algebra.Homology.Augment

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 1 →
    𝟙 (C.X 1) ≫ C.d 1 0 =
      (match 1, 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)

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 1 →
    𝟙 (C.X 1) ≫ C.d 1 (j + 1) =
      (match 1, 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:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 1 →
    𝟙 (C.X 1) ≫ C.d 1 0 =
      (match 1, 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)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 1 →
    𝟙 (C.X 1) ≫ C.d 1 (j + 1) =
      (match 1, 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))
Module: Mathlib.Algebra.Homology.Augment

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 1 = n + 2 →
    𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) 0 =
      (match 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)

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ j + 1 + 1 = n + 2 →
    𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) (j + 1) =
      (match 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:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 1 = n + 2 →
    𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) 0 =
      (match 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)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ j + 1 + 1 = n + 2 →
    𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) (j + 1) =
      (match 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))
Module: Mathlib.Algebra.Homology.Augment

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 0 → 𝟙 (C.X 0) ≫ 0 = C.d 0 0 ≫ 𝟙 (C.X 0)

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ 0 = C.d 0 (j + 1) ≫ 𝟙 (C.X (j + 1))

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 0 → 𝟙 (C.X 0) ≫ 0 = C.d 0 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ 0 = C.d 0 (j + 1) ≫ 𝟙 (C.X (j + 1))
Module: Mathlib.Algebra.Homology.Augment

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 1 →
    (𝟙 (C.X 1) ≫
        match 1, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d 1 0 ≫ 𝟙 (C.X 0)

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 1 →
    (𝟙 (C.X 1) ≫
        match 1, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d 1 (j + 1) ≫ 𝟙 (C.X (j + 1))

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 1 →
    (𝟙 (C.X 1) ≫
        match 1, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d 1 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 1 →
    (𝟙 (C.X 1) ≫
        match 1, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d 1 (j + 1) ≫ 𝟙 (C.X (j + 1))
Module: Mathlib.Algebra.Homology.Augment

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 1 = n + 2 →
    (𝟙 (C.X (n + 1 + 1)) ≫
        match 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.d (n + 2) 0 ≫ 𝟙 (C.X 0)

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ j + 1 + 1 = n + 2 →
    (𝟙 (C.X (n + 1 + 1)) ≫
        match 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.d (n + 2) (j + 1) ≫ 𝟙 (C.X (j + 1))

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 1 = n + 2 →
    (𝟙 (C.X (n + 1 + 1)) ≫
        match 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.d (n + 2) 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ j + 1 + 1 = n + 2 →
    (𝟙 (C.X (n + 1 + 1)) ≫
        match 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.d (n + 2) (j + 1) ≫ 𝟙 (C.X (j + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ }).f
      0 =
    (𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)).f 0

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)).f (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ }).f
      0 =
    (𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)).f 0

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)).f (n✝ + 1)
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ }).f
      0 =
    (𝟙 C).f 0

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 C).f (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ }).f
      0 =
    (𝟙 C).f 0

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 C).f (n✝ + 1)