no goals
α : Type u_1
β : Type ?u.126237
γ : Type ?u.126240
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 ∧ f a ≠ 0
simp