no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ j i : ι
x : β i
⊢ erase j (single i x) = if i = j then 0 else single i x
rw [← filter_ne_eq_erase, filter_single, ite_not]