F : Type ?u.248430
α : Type u_2
β : Type u_1
γ : Type ?u.248439
ι : Type ?u.248442
κ : Type ?u.248445
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
h : b ∈ s
⊢ ↑(f b) ≤ sup s (WithBot.some ∘ f)
F : Type ?u.248430
α : Type u_2
β : Type u_1
γ : Type ?u.248439
ι : Type ?u.248442
κ : Type ?u.248445
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
h : b ∈ s
⊢ f b ≤ sup' s (_ : ∃ x, x ∈ s) f
rw [← WithBot.coe_le_coe, coe_sup']
no goals
F : Type ?u.248430
α : Type u_2
β : Type u_1
γ : Type ?u.248439
ι : Type ?u.248442
κ : Type ?u.248445
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
h : b ∈ s
⊢ ↑(f b) ≤ sup s (WithBot.some ∘ f)
exact le_sup (f := fun c => WithBot.some (f c)) h