no goals
α : Type u_1
β : Type ?u.502352
γ : Type ?u.502355
ι : Type ?u.502358
M : Type u_2
M' : Type ?u.502364
N : Type ?u.502367
P : Type ?u.502370
G : Type ?u.502373
H : Type ?u.502376
R : Type ?u.502379
S : Type ?u.502382
inst✝ : AddCommMonoid M
p✝ p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (filter p f).support = Finset.filter p f.support
rw [Subsingleton.elim D] <;> rfl
no goals
α : Type u_1
β : Type ?u.502352
γ : Type ?u.502355
ι : Type ?u.502358
M : Type u_2
M' : Type ?u.502364
N : Type ?u.502367
P : Type ?u.502370
G : Type ?u.502373
H : Type ?u.502376
R : Type ?u.502379
S : Type ?u.502382
inst✝ : AddCommMonoid M
p✝ p : α → Prop
D : DecidablePred p
f : α →₀ M
x : α
hx : x ∈ Finset.filter p f.support
⊢ single x (↑(filter p f) x) = single x (↑f x)
rw [filter_apply_pos _ _ (mem_filter.1 hx).2]