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 j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, k with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
rcases k with (_ | _ | k) <;> rcases j with (_ | _ | j) <;> 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

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

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

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

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

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

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

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

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