mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
⊢ s.obj i < s.obj j

Tactic:
obtain h' | h' := (s.monotone hij.le).lt_or_eq

Goal state after:
case inl
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i < s.obj j
⊢ s.obj i < s.obj j

case inr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i = s.obj j
⊢ s.obj i < s.obj j
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: case right
n : ℕ
i : Fin (n + 2)
⊢ Function.Surjective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩

Tactic:
· rintro ⟨j, hj⟩
        simp only [mem_compl, mem_singleton] at hj
        obtain rfl | ⟨i, rfl⟩ := Fin.eq_zero_or_eq_succ i
        · exact ⟨j.pred hj, by simp⟩
        · exact ⟨i.predAbove j, by aesop⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i j : ℕ
⊢ (C.augment f w).d (i + 1) (j + 1) = C.d i j

Tactic:
cases i

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
j : ℕ
⊢ (C.augment f w).d (0 + 1) (j + 1) = C.d 0 j

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ({
            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
      i =
    (𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)).f i

Tactic:
cases i

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: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ({
            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
      i =
    (𝟙 C).f i

Tactic:
cases i

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)
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 ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
s : ¬(ComplexShape.up ℕ).Rel i 0
⊢ (match i, 0 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
s : ¬(ComplexShape.up ℕ).Rel 0 0
⊢ (match 0, 0 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
s : ¬(ComplexShape.up ℕ).Rel (n✝ + 1) 0
⊢ (match n✝ + 1, 0 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
s : ¬(ComplexShape.up ℕ).Rel i (0 + 1)
⊢ (match i, 0 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
s : ¬(ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ (match 0, 0 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
s : ¬(ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1)
⊢ (match n✝ + 1, 0 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
s : ¬(ComplexShape.up ℕ).Rel i (j + 1 + 1)
⊢ (match i, j + 1 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
j : ℕ
s : ¬(ComplexShape.up ℕ).Rel 0 (j + 1 + 1)
⊢ (match 0, j + 1 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
j n✝ : ℕ
s : ¬(ComplexShape.up ℕ).Rel (n✝ + 1) (j + 1 + 1)
⊢ (match n✝ + 1, j + 1 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
this : Mono (objEquiv x)
⊢ False

Tactic:
have := SimplexCategory.len_le_of_mono (objEquiv x)

Goal state after:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
this✝ : Mono (objEquiv x)
this : (unop (op ⦋i⦌)).len ≤ ⦋n⦌.len
⊢ False
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hij : (ComplexShape.up ℕ).Rel i 0
hjk : (ComplexShape.up ℕ).Rel 0 0
⊢ ((match i, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case zero.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk hij : (ComplexShape.up ℕ).Rel 0 0
⊢ ((match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case zero.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel 0 0
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) 0
⊢ ((match n✝ + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hij : (ComplexShape.up ℕ).Rel i (0 + 1)
hjk : (ComplexShape.up ℕ).Rel (0 + 1) 0
⊢ ((match i, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case zero.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel (0 + 1) 0
hij : (ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ ((match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case zero.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel (0 + 1) 0
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1)
⊢ ((match n✝ + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hij : (ComplexShape.up ℕ).Rel i (j + 1 + 1)
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) 0
⊢ ((match i, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case zero.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) 0
hij : (ComplexShape.up ℕ).Rel 0 (j + 1 + 1)
⊢ ((match 0, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case zero.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) 0
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (j + 1 + 1)
⊢ ((match n✝ + 1, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hij : (ComplexShape.up ℕ).Rel i 0
hjk : (ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ ((match i, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case succ.zero.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel 0 (0 + 1)
hij : (ComplexShape.up ℕ).Rel 0 0
⊢ ((match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.zero.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel 0 (0 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) 0
⊢ ((match n✝ + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hij : (ComplexShape.up ℕ).Rel i (0 + 1)
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (0 + 1)
⊢ ((match i, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case succ.zero.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (0 + 1)
hij : (ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ ((match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.zero.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (0 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1)
⊢ ((match n✝ + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hij : (ComplexShape.up ℕ).Rel i (j + 1 + 1)
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (0 + 1)
⊢ ((match i, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case succ.zero.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (0 + 1)
hij : (ComplexShape.up ℕ).Rel 0 (j + 1 + 1)
⊢ ((match 0, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.zero.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (0 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (j + 1 + 1)
⊢ ((match n✝ + 1, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hij : (ComplexShape.up ℕ).Rel i 0
hjk : (ComplexShape.up ℕ).Rel 0 (k + 1 + 1)
⊢ ((match i, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case succ.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel 0 (k + 1 + 1)
hij : (ComplexShape.up ℕ).Rel 0 0
⊢ ((match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel 0 (k + 1 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) 0
⊢ ((match n✝ + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hij : (ComplexShape.up ℕ).Rel i (0 + 1)
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (k + 1 + 1)
⊢ ((match i, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case succ.succ.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (k + 1 + 1)
hij : (ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ ((match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.succ.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (k + 1 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1)
⊢ ((match n✝ + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k j : ℕ
hij : (ComplexShape.up ℕ).Rel i (j + 1 + 1)
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (k + 1 + 1)
⊢ ((match i, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
cases i

Goal state after:
case succ.succ.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), 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)
⊢ ((match 0, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.succ.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), 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)
⊢ ((match n✝ + 1, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f i =
    (𝟙 (truncate.obj (C.augment f w))).f i

Tactic:
cases i

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f 0 =
    (𝟙 (truncate.obj (C.augment f w))).f 0

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