case inl
α : Type ?u.306784
β : Type ?u.306787
γ : Type ?u.306790
ι : Type ?u.306793
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.306886
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0

case inr
α : Type ?u.306784
β : Type ?u.306787
γ : Type ?u.306790
ι : Type ?u.306793
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.306886
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r
α : Type ?u.306784
β : Type ?u.306787
γ : Type ?u.306790
ι : Type ?u.306793
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.306886
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (closedBall x r) = ball x r
rcases eq_or_ne r 0 with (rfl | hr)
no goals
case inl
α : Type ?u.306784
β : Type ?u.306787
γ : Type ?u.306790
ι : Type ?u.306793
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.306886
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0
rw [closedBall_zero, ball_zero, interior_singleton]
no goals
case inr
α : Type ?u.306784
β : Type ?u.306787
γ : Type ?u.306790
ι : Type ?u.306793
inst✝⁶ : NormedField α
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type ?u.306886
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r
exact interior_closedBall x hr