case inl
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • closedBall x r = closedBall (0 • x) (‖0‖ * r)

case inr
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)
rcases eq_or_ne c 0 with (rfl | hc)
no goals
case inl
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • closedBall x r = closedBall (0 • x) (‖0‖ * r)
simp [hr, zero_smul_set, Set.singleton_zero, ← nonempty_closedBall]
no goals
case inr
𝕜 : Type u_2
E : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)
exact smul_closedBall' hc x r