Theorem: square_mem_nhds (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
⊢ Square p c ∈ 𝓝 p
Tactic:
wlog hc_pos : 0 < c generalizing c with h
State after:
case inr
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
h : ∀ {c : ℝ}, c ≠ 0 → 0 < c → Square p c ∈ 𝓝 p
hc_pos : ¬0 < c
⊢ Square p c ∈ 𝓝 p

z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
hc_pos : 0 < c
⊢ Square p c ∈ 𝓝 p

State before:
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
hc_pos : 0 < c
⊢ Square p c ∈ 𝓝 p
Tactic:
exact (nhds_hasBasis_square p).mem_of_mem hc_pos
State after:
no goals

State before:
case inr
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
h : ∀ {c : ℝ}, c ≠ 0 → 0 < c → Square p c ∈ 𝓝 p
hc_pos : ¬0 < c
⊢ Square p c ∈ 𝓝 p
Tactic:
rw [← square_neg]
State after:
case inr
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
h : ∀ {c : ℝ}, c ≠ 0 → 0 < c → Square p c ∈ 𝓝 p
hc_pos : ¬0 < c
⊢ Square p (-c) ∈ 𝓝 p

State before:
case inr
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
h : ∀ {c : ℝ}, c ≠ 0 → 0 < c → Square p c ∈ 𝓝 p
hc_pos : ¬0 < c
⊢ Square p (-c) ∈ 𝓝 p
Tactic:
exact h (neg_ne_zero.mpr hc) <| neg_pos.mpr <| hc.lt_of_le <| not_lt.mp hc_pos
State after:
no goals