simpa [Square, Rectangle] using by ring_nf
case hs
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ [[p.re - i✝, p.re + i✝]] ×ˢ [[p.im - i✝, p.im + i✝]] = ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p i✝
no goals