[GOAL]
a : ℝ
⊢ interior {z | z.re ≤ a} = {z | z.re < a}
[PROOFSTEP]
simpa only [interior_Iic] using interior_preimage_re (Iic a)
[GOAL]
a : ℝ
⊢ interior {z | z.im ≤ a} = {z | z.im < a}
[PROOFSTEP]
simpa only [interior_Iic] using interior_preimage_im (Iic a)
[GOAL]
a : ℝ
⊢ interior {z | a ≤ z.re} = {z | a < z.re}
[PROOFSTEP]
simpa only [interior_Ici] using interior_preimage_re (Ici a)
[GOAL]
a : ℝ
⊢ interior {z | a ≤ z.im} = {z | a < z.im}
[PROOFSTEP]
simpa only [interior_Ici] using interior_preimage_im (Ici a)
[GOAL]
a : ℝ
⊢ closure {z | z.re < a} = {z | z.re ≤ a}
[PROOFSTEP]
simpa only [closure_Iio] using closure_preimage_re (Iio a)
[GOAL]
a : ℝ
⊢ closure {z | z.im < a} = {z | z.im ≤ a}
[PROOFSTEP]
simpa only [closure_Iio] using closure_preimage_im (Iio a)
[GOAL]
a : ℝ
⊢ closure {z | a < z.re} = {z | a ≤ z.re}
[PROOFSTEP]
simpa only [closure_Ioi] using closure_preimage_re (Ioi a)
[GOAL]
a : ℝ
⊢ closure {z | a < z.im} = {z | a ≤ z.im}
[PROOFSTEP]
simpa only [closure_Ioi] using closure_preimage_im (Ioi a)
[GOAL]
a : ℝ
⊢ frontier {z | z.re ≤ a} = {z | z.re = a}
[PROOFSTEP]
simpa only [frontier_Iic] using frontier_preimage_re (Iic a)
[GOAL]
a : ℝ
⊢ frontier {z | z.im ≤ a} = {z | z.im = a}
[PROOFSTEP]
simpa only [frontier_Iic] using frontier_preimage_im (Iic a)
[GOAL]
a : ℝ
⊢ frontier {z | a ≤ z.re} = {z | z.re = a}
[PROOFSTEP]
simpa only [frontier_Ici] using frontier_preimage_re (Ici a)
[GOAL]
a : ℝ
⊢ frontier {z | a ≤ z.im} = {z | z.im = a}
[PROOFSTEP]
simpa only [frontier_Ici] using frontier_preimage_im (Ici a)
[GOAL]
a : ℝ
⊢ frontier {z | z.re < a} = {z | z.re = a}
[PROOFSTEP]
simpa only [frontier_Iio] using frontier_preimage_re (Iio a)
[GOAL]
a : ℝ
⊢ frontier {z | z.im < a} = {z | z.im = a}
[PROOFSTEP]
simpa only [frontier_Iio] using frontier_preimage_im (Iio a)
[GOAL]
a : ℝ
⊢ frontier {z | a < z.re} = {z | z.re = a}
[PROOFSTEP]
simpa only [frontier_Ioi] using frontier_preimage_re (Ioi a)
[GOAL]
a : ℝ
⊢ frontier {z | a < z.im} = {z | z.im = a}
[PROOFSTEP]
simpa only [frontier_Ioi] using frontier_preimage_im (Ioi a)
[GOAL]
s t : Set ℝ
⊢ closure (s ×ℂ t) = closure s ×ℂ closure t
[PROOFSTEP]
simpa only [← preimage_eq_preimage equivRealProdClm.symm.toHomeomorph.surjective,
  equivRealProdClm.symm.toHomeomorph.preimage_closure] using @closure_prod_eq _ _ _ _ s t
[GOAL]
s t : Set ℝ
⊢ interior (s ×ℂ t) = interior s ×ℂ interior t
[PROOFSTEP]
rw [Set.reProdIm, Set.reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]
[GOAL]
s t : Set ℝ
⊢ frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t
[PROOFSTEP]
simpa only [← preimage_eq_preimage equivRealProdClm.symm.toHomeomorph.surjective,
  equivRealProdClm.symm.toHomeomorph.preimage_frontier] using frontier_prod_eq s t
[GOAL]
a b : ℝ
⊢ frontier {z | a ≤ z.re ∧ b ≤ z.im} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ b ≤ z.im}
[PROOFSTEP]
simpa only [closure_Ici, frontier_Ici] using frontier_reProdIm (Ici a) (Ici b)
[GOAL]
a b : ℝ
⊢ frontier {z | a ≤ z.re ∧ z.im ≤ b} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}
[PROOFSTEP]
simpa only [closure_Ici, closure_Iic, frontier_Ici, frontier_Iic] using frontier_reProdIm (Ici a) (Iic b)
