intros
case hs
z w : ℂ
c : ℝ
p : ℂ
⊢ ∀ (i : ℝ),
    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✝
⊢ Icc (p.re - i✝) (p.re + i✝) ×ˢ Icc (p.im - i✝) (p.im + i✝) = ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p i✝