apply ((nhds_basis_Icc_pos p.re).prod_same_index_mono (nhds_basis_Icc_pos p.im) ?_ ?_).congr
z w : ℂ
c : ℝ
p : ℂ
⊢ (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (fun x => 0 < x) fun x => ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p x
case hp
z w : ℂ
c : ℝ
p : ℂ
⊢ ∀ (i : ℝ), 0 < i ↔ 0 < i

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

z w : ℂ
c : ℝ
p : ℂ
⊢ MonotoneOn (fun ε => Icc (p.re - ε) (p.re + ε)) {i | 0 < i}

z w : ℂ
c : ℝ
p : ℂ
⊢ MonotoneOn (fun ε => Icc (p.im - ε) (p.im + ε)) {i | 0 < i}