rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
⊢ supClosure s ×ˢ supClosure t ≤ supClosure (s ×ˢ t)
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.sup' hu id, v.sup' hv id) ∈ supClosure (s ×ˢ t)