no goals
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ closedBall x r = ↑(ContinuousLinearEquiv.symm toEuclidean) '' Metric.closedBall (↑toEuclidean x) r
rw [toEuclidean.image_symm_eq_preimage, closedBall_eq_preimage]