case zero
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
⊢ dTo ((single₀ V).obj X) Nat.zero = 0

case succ
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
n✝ : ℕ
⊢ dTo ((single₀ V).obj X) (Nat.succ n✝) = 0
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
i : ℕ
⊢ dTo ((single₀ V).obj X) i = 0
cases i
case zero.h
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) Nat.zero) Nat.zero
case zero
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
⊢ dTo ((single₀ V).obj X) Nat.zero = 0
rw [dTo_eq_zero]
no goals
case zero.h
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) Nat.zero) Nat.zero
simp
case succ
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
n✝ : ℕ
⊢ (xPrevIso ((single₀ V).obj X) (_ : n✝ + 1 = n✝ + 1)).hom ≫ d ((single₀ V).obj X) n✝ (n✝ + 1) = 0
case succ
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
n✝ : ℕ
⊢ dTo ((single₀ V).obj X) (Nat.succ n✝) = 0
erw [dTo_eq ((single₀ V).obj X) rfl]
no goals
case succ
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
n✝ : ℕ
⊢ (xPrevIso ((single₀ V).obj X) (_ : n✝ + 1 = n✝ + 1)).hom ≫ d ((single₀ V).obj X) n✝ (n✝ + 1) = 0
simp