no goals
α : Type u_2
β : Type ?u.357626
γ : Type ?u.357629
ι : Type ?u.357632
M : Type u_1
M' : Type ?u.357638
N : Type ?u.357641
P : Type ?u.357644
G : Type ?u.357647
H : Type ?u.357650
R : Type ?u.357653
S : Type ?u.357656
inst✝ : Zero M
p : α → Prop
f : α →₀ M
a : α
D : Decidable (p a)
⊢ ↑(filter p f) a = if p a then ↑f a else 0
rw [Subsingleton.elim D] <;> rfl