no goals
F : Type ?u.467741
α : Type u_1
β : Type u_2
γ : Type ?u.467750
ι : Type ?u.467753
κ : Type ?u.467756
s : Finset α
f : α → Set β
x : α
h : x ∈ s
⊢ f x ≤ ⨆ (_ : x ∈ s), f x
simp only [h, iSup_pos, le_refl]