no goals
s t : Set ℝ
⊢ closure (s ×ℂ t) = closure s ×ℂ closure t
simpa only [← preimage_eq_preimage equivRealProdClm.symm.toHomeomorph.surjective,
  equivRealProdClm.symm.toHomeomorph.preimage_closure] using @closure_prod_eq _ _ _ _ s t