Theorem: ne_center_of_not_mem_closed_ball (RMT4/defs.lean)

State before:
u : ℂ
U V W : Set ℂ
w : ℂ
r : ℝ
hr : 0 ≤ r
z : ℂ
hz : z ∈ (closedBall w r)ᶜ
⊢ z ≠ w
Tactic:
contrapose! hz
State after:
u : ℂ
U V W : Set ℂ
w : ℂ
r : ℝ
hr : 0 ≤ r
z : ℂ
hz : z = w
⊢ z ∉ (closedBall w r)ᶜ

State before:
u : ℂ
U V W : Set ℂ
w : ℂ
r : ℝ
hr : 0 ≤ r
z : ℂ
hz : z = w
⊢ z ∉ (closedBall w r)ᶜ
Tactic:
simp [hz, hr]
State after:
no goals