no goals
F : Type ?u.39437
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.39449
κ : Type ?u.39452
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq β
s : Finset γ
t : γ → Finset β
c : α
⊢ sup (Finset.biUnion s t) f ≤ c ↔ (sup s fun x => sup (t x) f) ≤ c
simp [@forall_swap _ β]