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