Theorem: circleMap_nz (Ray/Analytic/Uniform.lean)

State before:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
⊢ circleMap c (↑r) θ - c ≠ 0
Tactic:
simp only [circleMap_sub_center, Ne, circleMap_eq_center_iff, NNReal.coe_eq_zero]
State after:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
⊢ ¬r = 0

State before:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
⊢ ¬r = 0
Tactic:
intro h
State after:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
h : r = 0
⊢ False

State before:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
h : r = 0
⊢ False
Tactic:
rw [h] at rp
State after:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : 0 > 0
h : r = 0
⊢ False

State before:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : 0 > 0
h : r = 0
⊢ False
Tactic:
simp only [gt_iff_lt, not_lt_zero'] at rp
State after:
no goals