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