no goals
α : Type u_1
β : Type ?u.124309
γ : Type ?u.124312
f : α → ℝ≥0∞
s : Finset α
h : ∑ a in s, f a = 1
h' : ∀ (a : α), ¬a ∈ s → f a = 0
a : α
⊢ a ∈ support (ofFinset f s h h') ↔ a ∈ ↑s ∩ Function.support f
simpa [mem_support_iff] using mt (h' a)