no goals
α : Type u_1
β : Type ?u.56049
γ : Type ?u.56052
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : LE α
S : Set (UpperSet α)
s t : UpperSet α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ ↑(⨆ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), ↑(f i j)
simp_rw [coe_iSup]