no goals
F : Type ?u.455051
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.455063
κ : Type ?u.455066
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
s : Finset γ
t : γ → Finset α
f : α → β
⊢ (⨆ (y : α) (_ : y ∈ Finset.biUnion s t), f y) = ⨆ (x : γ) (_ : x ∈ s) (y : α) (_ : y ∈ t x), f y
simp [@iSup_comm _ α, iSup_and]