∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Monotone f → ∀ (s : Finset α) (h : (Finset.image f s).Nonempty), (Finset.image f s).max' h = f (s.max' ⋯)