F : Type ?u.247090
α : Type u_2
β : Type u_1
γ : Type ?u.247099
ι : Type ?u.247102
κ : Type ?u.247105
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
hs : ∀ (b : β), b ∈ s → f b ≤ a
⊢ sup s (WithBot.some ∘ f) ≤ ↑a
F : Type ?u.247090
α : Type u_2
β : Type u_1
γ : Type ?u.247099
ι : Type ?u.247102
κ : Type ?u.247105
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
hs : ∀ (b : β), b ∈ s → f b ≤ a
⊢ sup' s H f ≤ a
rw [← WithBot.coe_le_coe, coe_sup']
no goals
F : Type ?u.247090
α : Type u_2
β : Type u_1
γ : Type ?u.247099
ι : Type ?u.247102
κ : Type ?u.247105
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
hs : ∀ (b : β), b ∈ s → f b ≤ a
⊢ sup s (WithBot.some ∘ f) ≤ ↑a
exact Finset.sup_le fun b h => WithBot.coe_le_coe.2 <| hs b h