no goals
M : Type u
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x x_1 => x • x_1) c ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r
rw [preimage_smul, smul_closedBall]