no goals
α : Type u_1
β : Type ?u.473976
γ : Type ?u.473979
ι : Type ?u.473982
M : Type u_2
M' : Type ?u.473988
N : Type ?u.473991
P : Type ?u.473994
G : Type ?u.473997
H : Type ?u.474000
R : Type ?u.474003
S : Type ?u.474006
inst✝ : Zero M
p : α → Prop
f : α →₀ M
D : DecidablePred p
⊢ (filter p f).support = Finset.filter p f.support
rw [Subsingleton.elim D] <;> rfl