no goals
α : Type u_2
β : Type u_1
γ : Type ?u.39
inst✝ : ConditionallyCompleteLattice α
s✝ t : Set α
a✝ b : α
s : Finset β
hs : Finset.Nonempty s
f : β → α
a : α
⊢ sup' s hs f ≤ a ↔ sSup (f '' ↑s) ≤ a
simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (hs.to_set.image f)]