∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : ConditionallyCompleteLattice β] {f : α → β} [Nonempty α]
  [MeasurableSingletonClass α] [Finite α],
  BddAbove (Set.range f) → essSup f (ProbabilityTheory.uniformOn Set.univ) = ⨆ a, f a