no goals
α : Type u_2
β : Type ?u.54850
γ : Type ?u.54853
ι : Sort u_1
inst✝¹ : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝ : Nonempty ι
f : ι → α
c : α
H : ∀ (x : ι), f x ≤ c
⊢ ∀ (b : α), b ∈ range f → b ≤ c
rwa [forall_range_iff]