Theorem: Complex.nhds_hasBasis_square (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z w : ℂ
c : ℝ
p : ℂ
⊢ (𝓝 p).HasBasis (fun x => 0 < x) fun x => Square p x
Tactic:
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
State after:
z w : ℂ
c : ℝ
p : ℂ
⊢ (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (fun x => 0 < x) fun x => ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p x

State before:
z w : ℂ
c : ℝ
p : ℂ
⊢ (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (fun x => 0 < x) fun x => ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p x
Tactic:
apply ((nhds_basis_Icc_pos p.re).prod_same_index_mono (nhds_basis_Icc_pos p.im) ?_ ?_).congr
State after:
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}

State before:
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}
Tactic:
all_goals exact (antitone_const_tsub.Icc (monotone_id.const_add _)).monotoneOn _
State after:
no goals

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

State before:
case hp
z w : ℂ
c : ℝ
p : ℂ
⊢ ∀ (i : ℝ), 0 < i ↔ 0 < i
Tactic:
intro
State after:
case hp
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
⊢ 0 < i✝ ↔ 0 < i✝

State before:
case hp
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
⊢ 0 < i✝ ↔ 0 < i✝
Tactic:
rfl
State after:
no goals

State before:
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
Tactic:
intros
State after:
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✝

State before:
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✝
Tactic:
rw [← uIcc_of_lt (by linarith), ← uIcc_of_lt (by linarith)]
State after:
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✝

State before:
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✝
Tactic:
simpa [Square, Rectangle] using by ring_nf
State after:
no goals

State before:
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ p.re - i✝ < p.re + i✝
Tactic:
linarith
State after:
no goals

State before:
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ p.im - i✝ < p.im + i✝
Tactic:
linarith
State after:
no goals

State before:
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ [[(p.re - i✝, p.im - i✝), (p.re + i✝, p.im + i✝)]] = [[(-i✝ + p.re, -i✝ + p.im), (i✝ + p.re, i✝ + p.im)]]
Tactic:
ring_nf
State after:
no goals

State before:
z w : ℂ
c : ℝ
p : ℂ
⊢ MonotoneOn (fun ε => Icc (p.im - ε) (p.im + ε)) {i | 0 < i}
Tactic:
exact (antitone_const_tsub.Icc (monotone_id.const_add _)).monotoneOn _
State after:
no goals