no goals
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort u_1
inst✝ : Frame α
s t : Set α
a✝ b : α
f : (i : ι) → κ i → α
a : α
⊢ (a ⊓ ⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), a ⊓ f i j
simp only [inf_iSup_eq]