no goals
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort ?u.6733
inst✝ : Frame α
s t : Set α
a b : α
⊢ sSup s ⊓ sSup t = ⨆ (p : α × α) (_ : p ∈ s ×ˢ t), p.fst ⊓ p.snd
simp only [sSup_eq_iSup, biSup_inf_biSup]