no goals
F : Type ?u.252750
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.252762
κ : Type ?u.252765
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H : Finset.Nonempty s✝
f : β → α
inst✝ : DecidableEq β
s : Finset γ
Hs : Finset.Nonempty s
t : γ → Finset β
Ht : ∀ (b : γ), Finset.Nonempty (t b)
c : α
⊢ sup' (Finset.biUnion s t) (_ : Finset.Nonempty (Finset.biUnion s t)) f ≤ c ↔
    (sup' s Hs fun b => sup' (t b) (_ : Finset.Nonempty (t b)) f) ≤ c
simp [@forall_swap _ β]