[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
w : ¬ComplexShape.Rel (ComplexShape.down ℕ) i j
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) (i + 1) (j + 1)
[PROOFSTEP]
simpa
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroObject V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ d (truncate.obj C) 1 0 ≫ d C 1 0 = 0
[PROOFSTEP]
aesop
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i j : ℕ
h : ¬ComplexShape.Rel (ComplexShape.down ℕ) (i + 1) (j + 1)
⊢ (fun x x_1 =>
        match x, x_1 with
        | 1, 0 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      (i + 1) (j + 1) =
    0
[PROOFSTEP]
simp only
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i j : ℕ
h : ¬ComplexShape.Rel (ComplexShape.down ℕ) (i + 1) (j + 1)
⊢ d C i j = 0
[PROOFSTEP]
exact C.shape i j (Nat.succ_ne_succ.1 h)
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i j : ℕ
⊢ d (augment C f w) (i + 1) (j + 1) = d C i j
[PROOFSTEP]
cases i
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
j : ℕ
⊢ d (augment C f w) (Nat.zero + 1) (j + 1) = d C Nat.zero j
[PROOFSTEP]
rfl
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
j n✝ : ℕ
⊢ d (augment C f w) (Nat.succ n✝ + 1) (j + 1) = d C (Nat.succ n✝) j
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) i j →
    (fun i => 𝟙 (HomologicalComplex.X C i)) i ≫ d (truncate.obj (augment C f w)) i j =
      d C i j ≫ (fun i => 𝟙 (HomologicalComplex.X C i)) j
[PROOFSTEP]
cases j
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) i Nat.zero →
    (fun i => 𝟙 (HomologicalComplex.X C i)) i ≫ d (truncate.obj (augment C f w)) i Nat.zero =
      d C i Nat.zero ≫ (fun i => 𝟙 (HomologicalComplex.X C i)) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i : ℕ
⊢ 0 + 1 = i → 𝟙 (HomologicalComplex.X C i) ≫ d (augment C f w) (i + 1) (0 + 1) = d C i 0 ≫ 𝟙 (HomologicalComplex.X C 0)
[PROOFSTEP]
simp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i n✝ : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) i (Nat.succ n✝) →
    (fun i => 𝟙 (HomologicalComplex.X C i)) i ≫ d (truncate.obj (augment C f w)) i (Nat.succ n✝) =
      d C i (Nat.succ n✝) ≫ (fun i => 𝟙 (HomologicalComplex.X C i)) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i n✝ : ℕ
⊢ Nat.succ n✝ + 1 = i →
    𝟙 (HomologicalComplex.X C i) ≫ d (augment C f w) (i + 1) (Nat.succ n✝ + 1) =
      d C i (Nat.succ n✝) ≫ 𝟙 (HomologicalComplex.X C (Nat.succ n✝))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
⊢ ((Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i)) ≫
      Hom.mk fun i => 𝟙 (HomologicalComplex.X C i)) =
    𝟙 (truncate.obj (augment C f w))
[PROOFSTEP]
ext (_ | i)
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X C i))
      Nat.zero =
    Hom.f (𝟙 (truncate.obj (augment C f w))) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
⊢ 𝟙 (HomologicalComplex.X C 0) ≫ 𝟙 (HomologicalComplex.X C 0) = 𝟙 (HomologicalComplex.X C 0)
[PROOFSTEP]
simp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i : ℕ
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X C i))
      (Nat.succ i) =
    Hom.f (𝟙 (truncate.obj (augment C f w))) (Nat.succ i)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i : ℕ
⊢ 𝟙 (HomologicalComplex.X C (Nat.succ i)) ≫ 𝟙 (HomologicalComplex.X C (Nat.succ i)) = 𝟙 (HomologicalComplex.X C (i + 1))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
⊢ ((Hom.mk fun i => 𝟙 (HomologicalComplex.X C i)) ≫
      Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i)) =
    𝟙 C
[PROOFSTEP]
ext (_ | i)
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X C i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i))
      Nat.zero =
    Hom.f (𝟙 C) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
⊢ 𝟙 (HomologicalComplex.X C 0) ≫ 𝟙 (HomologicalComplex.X C 0) = 𝟙 (HomologicalComplex.X C 0)
[PROOFSTEP]
simp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i : ℕ
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X C i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i))
      (Nat.succ i) =
    Hom.f (𝟙 C) (Nat.succ i)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i : ℕ
⊢ 𝟙 (HomologicalComplex.X C (Nat.succ i)) ≫ 𝟙 (HomologicalComplex.X C (Nat.succ i)) =
    𝟙 (HomologicalComplex.X C (Nat.succ i))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ d C (i + 2) 0 = 0
[PROOFSTEP]
rw [C.shape]
[GOAL]
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) (i + 2) 0
[PROOFSTEP]
exact i.succ_succ_ne_one.symm
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i
[PROOFSTEP]
cases i
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero ⟶ X C Nat.zero
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n✝) ⟶ X C (Nat.succ n✝)
[PROOFSTEP]
exact 𝟙 _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) i j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          i ≫
        d C i j =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          j
[PROOFSTEP]
match i with
| 0 | 1 | n + 2 => cases' j with j <;> dsimp [augment, truncate] <;> simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 0 j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          0 ≫
        d C 0 j =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 0 j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          j
[PROOFSTEP]
cases' j with j
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 0 Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          0 ≫
        d C 0 Nat.zero =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 0 Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 0 (Nat.succ j) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          0 ≫
        d C 0 (Nat.succ j) =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 0 (Nat.succ j) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ j)
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 0 + 1 = 0 → 𝟙 (X C 0) ≫ d C 0 0 = 0 ≫ 𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ Nat.succ j + 1 = 0 → 𝟙 (X C 0) ≫ d C 0 (Nat.succ j) = 0 ≫ 𝟙 (X C (j + 1))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 1 j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          1 ≫
        d C 1 j =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 1 j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          j
[PROOFSTEP]
cases' j with j
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 1 Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          1 ≫
        d C 1 Nat.zero =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 1 Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 1 (Nat.succ j) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          1 ≫
        d C 1 (Nat.succ j) =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 1 (Nat.succ j) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ j)
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 0 + 1 = 1 → 𝟙 (X C (0 + 1)) ≫ d C 1 0 = d C 1 0 ≫ 𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ Nat.succ j + 1 = 1 → 𝟙 (X C (0 + 1)) ≫ d C 1 (Nat.succ j) = d C (0 + 1) (j + 1) ≫ 𝟙 (X C (j + 1))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j n : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) (n + 2) j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          (n + 2) ≫
        d C (n + 2) j =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (n + 2) j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          j
[PROOFSTEP]
cases' j with j
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) (n + 2) Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          (n + 2) ≫
        d C (n + 2) Nat.zero =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (n + 2) Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) (n + 2) (Nat.succ j) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          (n + 2) ≫
        d C (n + 2) (Nat.succ j) =
      d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (n + 2) (Nat.succ j) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i))
              i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ j)
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 0 + 1 = n + 2 →
    𝟙 (X C (n + 1 + 1)) ≫ d C (n + 2) 0 =
      (match n + 2, 0 with
        | 1, 0 => d C 1 0
        | Nat.succ i, Nat.succ j => d C (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ Nat.succ j + 1 = n + 2 →
    𝟙 (X C (n + 1 + 1)) ≫ d C (n + 2) (Nat.succ j) =
      (match n + 2, Nat.succ j with
        | 1, 0 => d C 1 0
        | Nat.succ i, Nat.succ j => d C (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (X C (j + 1))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i
[PROOFSTEP]
cases i
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ X C Nat.zero ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ X C (Nat.succ n✝) ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n✝)
[PROOFSTEP]
exact 𝟙 _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) i j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          i ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i j =
      d C i j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          j
[PROOFSTEP]
match i with
| 0 | 1 | n + 2 => cases' j with j <;> dsimp [augment, truncate] <;> simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 0 j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          0 ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 0 j =
      d C 0 j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          j
[PROOFSTEP]
cases' j with j
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 0 Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          0 ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 0 Nat.zero =
      d C 0 Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 0 (Nat.succ j) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          0 ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 0 (Nat.succ j) =
      d C 0 (Nat.succ j) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          (Nat.succ j)
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 0 + 1 = 0 → 𝟙 (X C 0) ≫ 0 = d C 0 0 ≫ 𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ Nat.succ j + 1 = 0 → 𝟙 (X C 0) ≫ 0 = d C 0 (Nat.succ j) ≫ 𝟙 (X C (Nat.succ j))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 1 j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          1 ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 1 j =
      d C 1 j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          j
[PROOFSTEP]
cases' j with j
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 1 Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          1 ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 1 Nat.zero =
      d C 1 Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 1 (Nat.succ j) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          1 ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) 1 (Nat.succ j) =
      d C 1 (Nat.succ j) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          (Nat.succ j)
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 0 + 1 = 1 → 𝟙 (X C (Nat.succ 0)) ≫ d C 1 0 = d C 1 0 ≫ 𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ Nat.succ j + 1 = 1 → 𝟙 (X C (Nat.succ 0)) ≫ d C (0 + 1) (j + 1) = d C 1 (Nat.succ j) ≫ 𝟙 (X C (Nat.succ j))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j n : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) (n + 2) j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          (n + 2) ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (n + 2) j =
      d C (n + 2) j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          j
[PROOFSTEP]
cases' j with j
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) (n + 2) Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          (n + 2) ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (n + 2) Nat.zero =
      d C (n + 2) Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) (n + 2) (Nat.succ j) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          (n + 2) ≫
        d (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (n + 2) (Nat.succ j) =
      d C (n + 2) (Nat.succ j) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i))
              i (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero))
              (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n))) (_ : i = i))
          (Nat.succ j)
[PROOFSTEP]
dsimp [augment, truncate]
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 0 + 1 = n + 2 →
    (𝟙 (X C (Nat.succ (n + 1))) ≫
        match n + 2, 0 with
        | 1, 0 => d C 1 0
        | Nat.succ i, Nat.succ j => d C (i + 1) (j + 1)
        | x, x_1 => 0) =
      d C (n + 2) 0 ≫ 𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ Nat.succ j + 1 = n + 2 →
    (𝟙 (X C (Nat.succ (n + 1))) ≫
        match n + 2, Nat.succ j with
        | 1, 0 => d C 1 0
        | Nat.succ i, Nat.succ j => d C (i + 1) (j + 1)
        | x, x_1 => 0) =
      d C (n + 2) (Nat.succ j) ≫ 𝟙 (X C (Nat.succ j))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ ((Hom.mk fun i =>
        Nat.casesOn (motive := fun t =>
          i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i)) i
          (fun h =>
            (_ : Nat.zero = i) ▸
              𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
          (fun n h =>
            (_ : Nat.succ n = i) ▸
              𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
          (_ : i = i)) ≫
      Hom.mk fun i =>
        Nat.casesOn (motive := fun t =>
          i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i)) i
          (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
          (_ : i = i)) =
    𝟙 (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0))
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i))
      i =
    Hom.f (𝟙 (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0))) i
[PROOFSTEP]
cases i
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i))
      Nat.zero =
    Hom.f (𝟙 (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0))) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ 𝟙 (X C 0) ≫ 𝟙 (X C 0) = 𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i))
      (Nat.succ n✝) =
    Hom.f (𝟙 (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0))) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ 𝟙 (X C (n✝ + 1)) ≫ 𝟙 (X C (Nat.succ n✝)) = 𝟙 (X C (n✝ + 1))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ ((Hom.mk fun i =>
        Nat.casesOn (motive := fun t =>
          i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i)) i
          (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
          (_ : i = i)) ≫
      Hom.mk fun i =>
        Nat.casesOn (motive := fun t =>
          i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i)) i
          (fun h =>
            (_ : Nat.zero = i) ▸
              𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
          (fun n h =>
            (_ : Nat.succ n = i) ▸
              𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
          (_ : i = i)) =
    𝟙 C
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
            (_ : i = i))
      i =
    Hom.f (𝟙 C) i
[PROOFSTEP]
cases i
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
            (_ : i = i))
      Nat.zero =
    Hom.f (𝟙 C) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ 𝟙 (X C 0) ≫ 𝟙 (X C 0) = 𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 1 0) (_ : d C (1 + 1) (0 + 1) ≫ d C (0 + 1) 0 = 0)) (Nat.succ n)))
            (_ : i = i))
      (Nat.succ n✝) =
    Hom.f (𝟙 C) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ 𝟙 (X C (Nat.succ n✝)) ≫ 𝟙 (X C (n✝ + 1)) = 𝟙 (X C (Nat.succ n✝))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
w : ¬ComplexShape.Rel (ComplexShape.up ℕ) i j
⊢ (fun i j => d C (i + 1) (j + 1)) i j = 0
[PROOFSTEP]
apply C.shape
[GOAL]
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
w : ¬ComplexShape.Rel (ComplexShape.up ℕ) i j
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) (i + 1) (j + 1)
[PROOFSTEP]
simpa
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroObject V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ d C 0 1 ≫ d (truncate.obj C) 0 1 = 0
[PROOFSTEP]
aesop
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j : ℕ
s : ¬ComplexShape.Rel (ComplexShape.up ℕ) i j
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      i j =
    0
[PROOFSTEP]
simp at s
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j : ℕ
s : ¬i + 1 = j
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      i j =
    0
[PROOFSTEP]
rcases j with (_ | _ | j)
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
s : ¬i + 1 = Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      i Nat.zero =
    0
[PROOFSTEP]
cases i
[GOAL]
case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
s : ¬i + 1 = Nat.succ Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      i (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
cases i
[GOAL]
case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j : ℕ
s : ¬i + 1 = Nat.succ (Nat.succ j)
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      i (Nat.succ (Nat.succ j)) =
    0
[PROOFSTEP]
cases i
[GOAL]
case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
s : ¬Nat.zero + 1 = Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      Nat.zero Nat.zero =
    0
[PROOFSTEP]
try simp
[GOAL]
case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
s : ¬Nat.zero + 1 = Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      Nat.zero Nat.zero =
    0
[PROOFSTEP]
simp
[GOAL]
case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
n✝ : ℕ
s : ¬Nat.succ n✝ + 1 = Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      (Nat.succ n✝) Nat.zero =
    0
[PROOFSTEP]
try simp
[GOAL]
case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
n✝ : ℕ
s : ¬Nat.succ n✝ + 1 = Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      (Nat.succ n✝) Nat.zero =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
s : ¬Nat.zero + 1 = Nat.succ Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      Nat.zero (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
s : ¬Nat.zero + 1 = Nat.succ Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      Nat.zero (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
n✝ : ℕ
s : ¬Nat.succ n✝ + 1 = Nat.succ Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      (Nat.succ n✝) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
n✝ : ℕ
s : ¬Nat.succ n✝ + 1 = Nat.succ Nat.zero
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      (Nat.succ n✝) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
s : ¬Nat.zero + 1 = Nat.succ (Nat.succ j)
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      Nat.zero (Nat.succ (Nat.succ j)) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
s : ¬Nat.zero + 1 = Nat.succ (Nat.succ j)
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      Nat.zero (Nat.succ (Nat.succ j)) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j n✝ : ℕ
s : ¬Nat.succ n✝ + 1 = Nat.succ (Nat.succ j)
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      (Nat.succ n✝) (Nat.succ (Nat.succ j)) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j n✝ : ℕ
s : ¬Nat.succ n✝ + 1 = Nat.succ (Nat.succ j)
⊢ (fun x x_1 =>
        match x, x_1 with
        | 0, 1 => f
        | Nat.succ i, Nat.succ j => d C i j
        | x, x_2 => 0)
      (Nat.succ n✝) (Nat.succ (Nat.succ j)) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
s : ¬Nat.zero + 1 = Nat.succ Nat.zero
⊢ f = 0
[PROOFSTEP]
simp at s
[GOAL]
case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j n✝ : ℕ
s : ¬Nat.succ n✝ + 1 = Nat.succ (Nat.succ j)
⊢ d C n✝ (Nat.succ j) = 0
[PROOFSTEP]
rw [C.shape]
[GOAL]
case succ.succ.succ.a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j n✝ : ℕ
s : ¬Nat.succ n✝ + 1 = Nat.succ (Nat.succ j)
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) n✝ (Nat.succ j)
[PROOFSTEP]
simp only [ComplexShape.up_Rel]
[GOAL]
case succ.succ.succ.a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j n✝ : ℕ
s : ¬Nat.succ n✝ + 1 = Nat.succ (Nat.succ j)
⊢ ¬n✝ + 1 = Nat.succ j
[PROOFSTEP]
contrapose! s
[GOAL]
case succ.succ.succ.a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j n✝ : ℕ
s : n✝ + 1 = Nat.succ j
⊢ Nat.succ n✝ + 1 = Nat.succ (Nat.succ j)
[PROOFSTEP]
rw [← s]
[GOAL]
case succ.succ.succ.a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j n✝ : ℕ
s : n✝ + 1 = Nat.succ j
⊢ Nat.succ n✝ + 1 = Nat.succ (n✝ + 1)
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j k : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i j
hjk : ComplexShape.Rel (ComplexShape.up ℕ) j k
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i j ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        j k =
    0
[PROOFSTEP]
rcases k with (_ | _ | k)
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i j
hjk : ComplexShape.Rel (ComplexShape.up ℕ) j Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i j ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        j Nat.zero =
    0
[PROOFSTEP]
rcases j with (_ | _ | j)
[GOAL]
case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i j
hjk : ComplexShape.Rel (ComplexShape.up ℕ) j (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i j ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        j (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
rcases j with (_ | _ | j)
[GOAL]
case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i j
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) j (Nat.succ (Nat.succ k))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i j ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        j (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
rcases j with (_ | _ | j)
[GOAL]
case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i Nat.zero
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero =
    0
[PROOFSTEP]
cases i
[GOAL]
case zero.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ Nat.zero)
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) Nat.zero =
    0
[PROOFSTEP]
cases i
[GOAL]
case zero.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ (Nat.succ j))
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) Nat.zero =
    0
[PROOFSTEP]
cases i
[GOAL]
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i Nat.zero
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
cases i
[GOAL]
case succ.zero.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ Nat.zero)
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
cases i
[GOAL]
case succ.zero.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ (Nat.succ j))
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
cases i
[GOAL]
case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i k : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i Nat.zero
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ k))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
cases i
[GOAL]
case succ.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i k : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ Nat.zero)
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ k))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
cases i
[GOAL]
case succ.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i k j : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ (Nat.succ j))
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        i (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
cases i
[GOAL]
case zero.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero =
    0
[PROOFSTEP]
try simp
[GOAL]
case zero.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero =
    0
[PROOFSTEP]
simp
[GOAL]
case zero.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero =
    0
[PROOFSTEP]
try simp
[GOAL]
case zero.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero =
    0
[PROOFSTEP]
simp
[GOAL]
case zero.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) Nat.zero
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) Nat.zero =
    0
[PROOFSTEP]
try simp
[GOAL]
case zero.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) Nat.zero
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) Nat.zero =
    0
[PROOFSTEP]
simp
[GOAL]
case zero.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) Nat.zero
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) Nat.zero =
    0
[PROOFSTEP]
try simp
[GOAL]
case zero.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) Nat.zero
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) Nat.zero =
    0
[PROOFSTEP]
simp
[GOAL]
case zero.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) Nat.zero
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) Nat.zero =
    0
[PROOFSTEP]
try simp
[GOAL]
case zero.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) Nat.zero
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) Nat.zero =
    0
[PROOFSTEP]
simp
[GOAL]
case zero.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) Nat.zero
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) Nat.zero =
    0
[PROOFSTEP]
try simp
[GOAL]
case zero.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) Nat.zero
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) Nat.zero =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.zero.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.zero.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.zero.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.zero.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.zero.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ Nat.zero)
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.zero.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ Nat.zero)
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.zero.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ Nat.zero)
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.zero.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ Nat.zero)
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.zero.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero)
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.zero.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero)
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.zero.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero)
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.zero.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero)
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ Nat.zero) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ k))
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ k))
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ k))
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ k))
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) Nat.zero
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) Nat.zero ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.succ.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ k))
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.succ.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ k))
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.succ.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ k))
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.succ.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ k))
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ Nat.zero)
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ Nat.zero) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ Nat.zero) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.succ.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k))
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.succ.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k))
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        Nat.zero (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.succ.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k))
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
try simp
[GOAL]
case succ.succ.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k j : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k))
n✝ : ℕ
hij : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ (Nat.succ j))
⊢ (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ n✝) (Nat.succ (Nat.succ j)) ≫
      (fun x x_1 =>
          match x, x_1 with
          | 0, 1 => f
          | Nat.succ i, Nat.succ j => d C i j
          | x, x_2 => 0)
        (Nat.succ (Nat.succ j)) (Nat.succ (Nat.succ k)) =
    0
[PROOFSTEP]
simp
[GOAL]
case succ.succ.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
k : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ k))
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
⊢ f ≫ d C 0 (Nat.succ k) = 0
[PROOFSTEP]
cases k
[GOAL]
case succ.succ.succ.zero.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ Nat.zero))
⊢ f ≫ d C 0 (Nat.succ Nat.zero) = 0
[PROOFSTEP]
exact w
[GOAL]
case succ.succ.succ.zero.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
n✝ : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ (Nat.succ n✝)))
⊢ f ≫ d C 0 (Nat.succ (Nat.succ n✝)) = 0
[PROOFSTEP]
rw [C.shape, comp_zero]
[GOAL]
case succ.succ.succ.zero.zero.succ.a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
n✝ : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ (Nat.succ n✝)))
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) 0 (Nat.succ (Nat.succ n✝))
[PROOFSTEP]
simp only [Nat.zero_eq, ComplexShape.up_Rel, zero_add]
[GOAL]
case succ.succ.succ.zero.zero.succ.a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
hij : ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero)
n✝ : ℕ
hjk : ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ Nat.zero) (Nat.succ (Nat.succ (Nat.succ n✝)))
⊢ ¬1 = Nat.succ (Nat.succ n✝)
[PROOFSTEP]
exact (Nat.one_lt_succ_succ _).ne
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i j →
    (fun i => 𝟙 (HomologicalComplex.X C i)) i ≫ d (truncate.obj (augment C f w)) i j =
      d C i j ≫ (fun i => 𝟙 (HomologicalComplex.X C i)) j
[PROOFSTEP]
cases j
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i Nat.zero →
    (fun i => 𝟙 (HomologicalComplex.X C i)) i ≫ d (truncate.obj (augment C f w)) i Nat.zero =
      d C i Nat.zero ≫ (fun i => 𝟙 (HomologicalComplex.X C i)) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
⊢ i + 1 = 0 → 𝟙 (HomologicalComplex.X C i) ≫ d C i 0 = d C i 0 ≫ 𝟙 (HomologicalComplex.X C 0)
[PROOFSTEP]
simp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i n✝ : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ n✝) →
    (fun i => 𝟙 (HomologicalComplex.X C i)) i ≫ d (truncate.obj (augment C f w)) i (Nat.succ n✝) =
      d C i (Nat.succ n✝) ≫ (fun i => 𝟙 (HomologicalComplex.X C i)) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i n✝ : ℕ
⊢ i + 1 = Nat.succ n✝ →
    𝟙 (HomologicalComplex.X C i) ≫ d C i (n✝ + 1) = d C i (Nat.succ n✝) ≫ 𝟙 (HomologicalComplex.X C (Nat.succ n✝))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
⊢ ((Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i)) ≫
      Hom.mk fun i => 𝟙 (HomologicalComplex.X C i)) =
    𝟙 (truncate.obj (augment C f w))
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X C i))
      i =
    Hom.f (𝟙 (truncate.obj (augment C f w))) i
[PROOFSTEP]
cases i
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X C i))
      Nat.zero =
    Hom.f (𝟙 (truncate.obj (augment C f w))) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
⊢ 𝟙 (HomologicalComplex.X C 0) ≫ 𝟙 (HomologicalComplex.X C 0) = 𝟙 (HomologicalComplex.X C 0)
[PROOFSTEP]
simp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X C i))
      (Nat.succ n✝) =
    Hom.f (𝟙 (truncate.obj (augment C f w))) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
n✝ : ℕ
⊢ 𝟙 (HomologicalComplex.X C (Nat.succ n✝)) ≫ 𝟙 (HomologicalComplex.X C (Nat.succ n✝)) =
    𝟙 (HomologicalComplex.X C (n✝ + 1))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
⊢ ((Hom.mk fun i => 𝟙 (HomologicalComplex.X C i)) ≫
      Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i)) =
    𝟙 C
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
i : ℕ
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X C i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i))
      i =
    Hom.f (𝟙 C) i
[PROOFSTEP]
cases i
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X C i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i))
      Nat.zero =
    Hom.f (𝟙 C) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
⊢ 𝟙 (HomologicalComplex.X C 0) ≫ 𝟙 (HomologicalComplex.X C 0) = 𝟙 (HomologicalComplex.X C 0)
[PROOFSTEP]
simp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i => 𝟙 (HomologicalComplex.X C i)) ≫
        Hom.mk fun i => 𝟙 (HomologicalComplex.X (truncate.obj (augment C f w)) i))
      (Nat.succ n✝) =
    Hom.f (𝟙 C) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ HomologicalComplex.X C 0
w : f ≫ d C 0 1 = 0
n✝ : ℕ
⊢ 𝟙 (HomologicalComplex.X C (Nat.succ n✝)) ≫ 𝟙 (HomologicalComplex.X C (Nat.succ n✝)) =
    𝟙 (HomologicalComplex.X C (Nat.succ n✝))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ d C 0 (i + 2) = 0
[PROOFSTEP]
rw [C.shape]
[GOAL]
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) 0 (i + 2)
[PROOFSTEP]
simp only [ComplexShape.up_Rel, zero_add]
[GOAL]
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬1 = i + 2
[PROOFSTEP]
exact (Nat.one_lt_succ_succ _).ne
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i
[PROOFSTEP]
cases i
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero ⟶ X C Nat.zero
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n✝) ⟶ X C (Nat.succ n✝)
[PROOFSTEP]
exact 𝟙 _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          i ≫
        d C i j =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          j
[PROOFSTEP]
rcases j with (_ | _ | j)
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          i ≫
        d C i Nat.zero =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          Nat.zero
[PROOFSTEP]
cases i
[GOAL]
case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ Nat.zero) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          i ≫
        d C i (Nat.succ Nat.zero) =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i (Nat.succ Nat.zero) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ Nat.zero)
[PROOFSTEP]
cases i
[GOAL]
case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ (Nat.succ j)) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          i ≫
        d C i (Nat.succ (Nat.succ j)) =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i (Nat.succ (Nat.succ j)) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ (Nat.succ j))
[PROOFSTEP]
cases i
[GOAL]
case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          Nat.zero ≫
        d C Nat.zero Nat.zero =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ 0 + 1 = 0 →
    𝟙 (X C 0) ≫ d C 0 0 = d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) 0 0 ≫ 𝟙 (X C 0)
[PROOFSTEP]
aesop
[GOAL]
case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ n✝) ≫
        d C (Nat.succ n✝) Nat.zero =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n✝) Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ Nat.succ n✝ + 1 = 0 →
    𝟙 (X C (n✝ + 1)) ≫ d C (Nat.succ n✝) 0 =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n✝) 0 ≫ 𝟙 (X C 0)
[PROOFSTEP]
aesop
[GOAL]
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          Nat.zero ≫
        d C Nat.zero (Nat.succ Nat.zero) =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero (Nat.succ Nat.zero) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ Nat.zero)
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ 0 + 1 = Nat.succ 0 → 𝟙 (X C 0) ≫ d C 0 (Nat.succ 0) = d C 0 1 ≫ 𝟙 (X C (0 + 1))
[PROOFSTEP]
aesop
[GOAL]
case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ Nat.zero) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ n✝) ≫
        d C (Nat.succ n✝) (Nat.succ Nat.zero) =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n✝) (Nat.succ Nat.zero) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ Nat.zero)
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ Nat.succ n✝ + 1 = Nat.succ 0 →
    𝟙 (X C (n✝ + 1)) ≫ d C (Nat.succ n✝) (Nat.succ 0) = d C (n✝ + 1) (0 + 1) ≫ 𝟙 (X C (0 + 1))
[PROOFSTEP]
aesop
[GOAL]
case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ j)) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          Nat.zero ≫
        d C Nat.zero (Nat.succ (Nat.succ j)) =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero (Nat.succ (Nat.succ j)) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ (Nat.succ j))
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j : ℕ
⊢ 0 + 1 = Nat.succ (Nat.succ j) →
    𝟙 (X C 0) ≫ d C 0 (Nat.succ (Nat.succ j)) =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) 0 (Nat.succ (Nat.succ j)) ≫
        𝟙 (X C (Nat.succ j + 1))
[PROOFSTEP]
aesop
[GOAL]
case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j n✝ : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ n✝) (Nat.succ (Nat.succ j)) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ n✝) ≫
        d C (Nat.succ n✝) (Nat.succ (Nat.succ j)) =
      d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n✝) (Nat.succ (Nat.succ j)) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
              (fun h =>
                (_ : Nat.zero = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
              (fun n h =>
                (_ : Nat.succ n = i) ▸
                  𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
              (_ : i = i))
          (Nat.succ (Nat.succ j))
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j n✝ : ℕ
⊢ Nat.succ n✝ + 1 = Nat.succ (Nat.succ j) →
    𝟙 (X C (n✝ + 1)) ≫ d C (Nat.succ n✝) (Nat.succ (Nat.succ j)) = d C (n✝ + 1) (j + 1 + 1) ≫ 𝟙 (X C (Nat.succ j + 1))
[PROOFSTEP]
aesop
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i
[PROOFSTEP]
cases i
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ X C Nat.zero ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ X C (Nat.succ n✝) ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n✝)
[PROOFSTEP]
exact 𝟙 _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i j →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          i ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i j =
      d C i j ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          j
[PROOFSTEP]
rcases j with (_ | _ | j)
[GOAL]
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          i ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i Nat.zero =
      d C i Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          Nat.zero
[PROOFSTEP]
cases' i with i
[GOAL]
case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ Nat.zero) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          i ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i (Nat.succ Nat.zero) =
      d C i (Nat.succ Nat.zero) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          (Nat.succ Nat.zero)
[PROOFSTEP]
cases' i with i
[GOAL]
case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) i (Nat.succ (Nat.succ j)) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          i ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i (Nat.succ (Nat.succ j)) =
      d C i (Nat.succ (Nat.succ j)) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          (Nat.succ (Nat.succ j))
[PROOFSTEP]
cases' i with i
[GOAL]
case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          Nat.zero ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero Nat.zero =
      d C Nat.zero Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ 0 + 1 = 0 →
    𝟙 (X C 0) ≫ d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) 0 0 = d C 0 0 ≫ 𝟙 (X C 0)
[PROOFSTEP]
aesop
[GOAL]
case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ i) Nat.zero →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          (Nat.succ i) ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ i) Nat.zero =
      d C (Nat.succ i) Nat.zero ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          Nat.zero
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ Nat.succ i + 1 = 0 →
    𝟙 (X C (Nat.succ i)) ≫ d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ i) 0 =
      d C (Nat.succ i) 0 ≫ 𝟙 (X C 0)
[PROOFSTEP]
aesop
[GOAL]
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ Nat.zero) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          Nat.zero ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero (Nat.succ Nat.zero) =
      d C Nat.zero (Nat.succ Nat.zero) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          (Nat.succ Nat.zero)
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ 0 + 1 = Nat.succ 0 → 𝟙 (X C 0) ≫ d C 0 1 = d C 0 (Nat.succ 0) ≫ 𝟙 (X C (Nat.succ 0))
[PROOFSTEP]
aesop
[GOAL]
case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ i) (Nat.succ Nat.zero) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          (Nat.succ i) ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ i) (Nat.succ Nat.zero) =
      d C (Nat.succ i) (Nat.succ Nat.zero) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          (Nat.succ Nat.zero)
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ Nat.succ i + 1 = Nat.succ 0 →
    𝟙 (X C (Nat.succ i)) ≫ d C (i + 1) (0 + 1) = d C (Nat.succ i) (Nat.succ 0) ≫ 𝟙 (X C (Nat.succ 0))
[PROOFSTEP]
aesop
[GOAL]
case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) Nat.zero (Nat.succ (Nat.succ j)) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          Nat.zero ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero (Nat.succ (Nat.succ j)) =
      d C Nat.zero (Nat.succ (Nat.succ j)) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          (Nat.succ (Nat.succ j))
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j : ℕ
⊢ 0 + 1 = Nat.succ (Nat.succ j) →
    𝟙 (X C 0) ≫ d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) 0 (Nat.succ (Nat.succ j)) =
      d C 0 (Nat.succ (Nat.succ j)) ≫ 𝟙 (X C (Nat.succ (Nat.succ j)))
[PROOFSTEP]
aesop
[GOAL]
case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j i : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) (Nat.succ i) (Nat.succ (Nat.succ j)) →
    (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          (Nat.succ i) ≫
        d (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ i) (Nat.succ (Nat.succ j)) =
      d C (Nat.succ i) (Nat.succ (Nat.succ j)) ≫
        (fun i =>
            Nat.casesOn (motive := fun t =>
              i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
              (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
              (_ : i = i))
          (Nat.succ (Nat.succ j))
[PROOFSTEP]
dsimp
  -- Porting note: simp can't handle this now but aesop does
[GOAL]
case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j i : ℕ
⊢ Nat.succ i + 1 = Nat.succ (Nat.succ j) →
    𝟙 (X C (Nat.succ i)) ≫ d C (i + 1) (j + 1 + 1) =
      d C (Nat.succ i) (Nat.succ (Nat.succ j)) ≫ 𝟙 (X C (Nat.succ (Nat.succ j)))
[PROOFSTEP]
aesop
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ ((Hom.mk fun i =>
        Nat.casesOn (motive := fun t =>
          i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
          (fun h =>
            (_ : Nat.zero = i) ▸ 𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
          (fun n h =>
            (_ : Nat.succ n = i) ▸
              𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
          (_ : i = i)) ≫
      Hom.mk fun i =>
        Nat.casesOn (motive := fun t =>
          i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
          (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
          (_ : i = i)) =
    𝟙 (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0))
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i))
      i =
    Hom.f (𝟙 (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0))) i
[PROOFSTEP]
cases i
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i))
      Nat.zero =
    Hom.f (𝟙 (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0))) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ 𝟙 (X C 0) ≫ 𝟙 (X C 0) = 𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i))
      (Nat.succ n✝) =
    Hom.f (𝟙 (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0))) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ 𝟙 (X C (n✝ + 1)) ≫ 𝟙 (X C (Nat.succ n✝)) = 𝟙 (X C (n✝ + 1))
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ ((Hom.mk fun i =>
        Nat.casesOn (motive := fun t =>
          i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
          (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
          (_ : i = i)) ≫
      Hom.mk fun i =>
        Nat.casesOn (motive := fun t =>
          i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
          (fun h =>
            (_ : Nat.zero = i) ▸ 𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
          (fun n h =>
            (_ : Nat.succ n = i) ▸
              𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
          (_ : i = i)) =
    𝟙 C
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
            (_ : i = i))
      i =
    Hom.f (𝟙 C) i
[PROOFSTEP]
cases i
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
            (_ : i = i))
      Nat.zero =
    Hom.f (𝟙 C) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ 𝟙 (X C 0) ≫ 𝟙 (X C 0) = 𝟙 (X C 0)
[PROOFSTEP]
simp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X C i ⟶ X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i)) i
            (fun h => (_ : Nat.zero = i) ▸ 𝟙 (X C Nat.zero)) (fun n h => (_ : Nat.succ n = i) ▸ 𝟙 (X C (Nat.succ n)))
            (_ : i = i)) ≫
        Hom.mk fun i =>
          Nat.casesOn (motive := fun t =>
            i = t → (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) i ⟶ X C i)) i
            (fun h =>
              (_ : Nat.zero = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) Nat.zero))
            (fun n h =>
              (_ : Nat.succ n = i) ▸
                𝟙 (X (augment (truncate.obj C) (d C 0 1) (_ : d C 0 1 ≫ d C 1 (1 + 1) = 0)) (Nat.succ n)))
            (_ : i = i))
      (Nat.succ n✝) =
    Hom.f (𝟙 C) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ 𝟙 (X C (Nat.succ n✝)) ≫ 𝟙 (X C (n✝ + 1)) = 𝟙 (X C (Nat.succ n✝))
[PROOFSTEP]
simp