Theorem: mem_sphere_closed (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 : ℝ
z c : ℂ
r : ℝ
⊢ z ∈ sphere c r → z ∈ closedBall c r
Tactic:
simp only [mem_sphere_iff_norm, Complex.norm_eq_abs, Metric.mem_closedBall]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ Complex.abs (z - c) = r → dist z c ≤ r

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