simp [prodMk_inf'_inf']
case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
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 ×ˢ v).inf' ⋯ id = (u.inf' hu id, v.inf' hv id)
no goals