no goals
α : Type u_1
β : Type ?u.474229
γ : Type ?u.474232
ι : Type ?u.474235
M : Type u_2
M' : Type ?u.474241
N : Type ?u.474244
P : Type ?u.474247
G : Type ?u.474250
H : Type ?u.474253
R : Type ?u.474256
S : Type ?u.474259
inst✝ : Zero M
p : α → Prop
f : α →₀ M
⊢ filter p 0 = 0
classical rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]
no goals
α : Type u_1
β : Type ?u.474229
γ : Type ?u.474232
ι : Type ?u.474235
M : Type u_2
M' : Type ?u.474241
N : Type ?u.474244
P : Type ?u.474247
G : Type ?u.474250
H : Type ?u.474253
R : Type ?u.474256
S : Type ?u.474259
inst✝ : Zero M
p : α → Prop
f : α →₀ M
⊢ filter p 0 = 0
rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]