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