Theorem: center_not_in_sphere (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : z ∈ sphere c r
⊢ z - c ≠ 0
Tactic:
simp only [mem_sphere_iff_norm, Complex.norm_eq_abs] at zs
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : Complex.abs (z - c) = r
⊢ z - c ≠ 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : Complex.abs (z - c) = r
⊢ z - c ≠ 0
Tactic:
rw [←Complex.abs.ne_zero_iff, zs]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : Complex.abs (z - c) = r
⊢ r ≠ 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : Complex.abs (z - c) = r
⊢ r ≠ 0
Tactic:
exact rp.ne'
State after:
no goals