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

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

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

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

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

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

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

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

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:
<;>

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
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

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

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

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

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

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

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

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

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