rw [← uIcc_of_lt (by linarith), ← uIcc_of_lt (by linarith)]
case hs
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ Icc (p.re - i✝) (p.re + i✝) ×ˢ Icc (p.im - i✝) (p.im + i✝) = ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p i✝
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✝