[GOAL]
E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
w : E
⊢ w ∈ sphere 0 r → -w ∈ sphere 0 r
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
i : SeminormedAddCommGroup E
r✝ r : ℝ
w : E
⊢ w ∈ ball 0 r → -w ∈ ball 0 r
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
i : SeminormedAddCommGroup E
r✝ r : ℝ
w : E
⊢ w ∈ closedBall 0 r → -w ∈ closedBall 0 r
[PROOFSTEP]
simp
