∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Div α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] {s t : Finset α} {f : α → β} {a : β}, ((s / t).sup f ≤ a) = ∀ x ∈ s, ∀ y ∈ t, f (x / y) ≤ a