V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
j : ℕ
⊢ (xPrevIso ((single₀ V).obj X) (_ : j + 1 = j + 1)).hom ≫ d ((single₀ V).obj X) (j + 1) j = 0
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
j : ℕ
⊢ dTo ((single₀ V).obj X) j = 0
rw [dTo_eq ((single₀ V).obj X) rfl]
no goals
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
X : V
j : ℕ
⊢ (xPrevIso ((single₀ V).obj X) (_ : j + 1 = j + 1)).hom ≫ d ((single₀ V).obj X) (j + 1) j = 0
simp