α : Type u_1
β : Type ?u.5502
γ : Type ?u.5505
s : Finset α
hs : Finset.Nonempty s
a✝ a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ support (uniformOfFinset s (_ : ∃ x, x ∈ s)) ↔ x ∈ ↑s
α : Type u_1
β : Type ?u.5502
γ : Type ?u.5505
s : Finset α
hs : Finset.Nonempty s
a : α
⊢ ∀ (x : α), x ∈ support (uniformOfFinset s hs) ↔ x ∈ ↑s
let ⟨a, ha⟩ := hs
no goals
α : Type u_1
β : Type ?u.5502
γ : Type ?u.5505
s : Finset α
hs : Finset.Nonempty s
a✝ a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ support (uniformOfFinset s (_ : ∃ x, x ∈ s)) ↔ x ∈ ↑s
simp [mem_support_iff, Finset.ne_empty_of_mem ha]