no goals
s t : Set ℝ
⊢ frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t
simpa only [← preimage_eq_preimage equivRealProdClm.symm.toHomeomorph.surjective,
  equivRealProdClm.symm.toHomeomorph.preimage_frontier] using frontier_prod_eq s t