suffices (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (0 < .) (equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p .)
  by simpa only [← nhds_prod_eq, Homeomorph.map_nhds_eq, Homeomorph.image_preimage]
    using this.map equivRealProdCLM.symm.toHomeomorph
z w : ℂ
c : ℝ
p : ℂ
⊢ (𝓝 p).HasBasis (fun x => 0 < x) fun x => Square p x
z w : ℂ
c : ℝ
p : ℂ
⊢ (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (fun x => 0 < x) fun x => ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p x