diff --git a/Mathlib/Analysis/NormedSpace/Pointwise.lean b/Mathlib/Analysis/NormedSpace/Pointwise.lean
index bca79c21b02e0..aa635cc5c708e 100644
--- a/Mathlib/Analysis/NormedSpace/Pointwise.lean
+++ b/Mathlib/Analysis/NormedSpace/Pointwise.lean
@@ -112,14 +112,11 @@ theorem smul_closedBall' {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) :
   simp only [← ball_union_sphere, Set.smul_set_union, _root_.smul_ball hc, smul_sphere' hc]
 #align smul_closed_ball' smul_closedBall'
 
-theorem Metric.Bounded.smul {s : Set E} (hs : Bounded s) (c : 𝕜) : Bounded (c • s) := by
-  obtain ⟨R, hR⟩ : ∃ R : ℝ, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le
-  refine' bounded_iff_forall_norm_le.2 ⟨‖c‖ * R, fun z hz => _⟩
-  obtain ⟨y, ys, rfl⟩ : ∃ y : E, y ∈ s ∧ c • y = z := mem_smul_set.1 hz
-  calc
-    ‖c • y‖ = ‖c‖ * ‖y‖ := norm_smul _ _
-    _ ≤ ‖c‖ * R := mul_le_mul_of_nonneg_left (hR y ys) (norm_nonneg _)
-#align metric.bounded.smul Metric.Bounded.smul
+/-- Image of a bounded set in a normed space under scalar multiplication by a constant is
+bounded. See also `Metric.Bounded.smul` for a similar lemma about an isometric action. -/
+theorem Metric.Bounded.smul₀ {s : Set E} (hs : Bounded s) (c : 𝕜) : Bounded (c • s) :=
+  (lipschitzWith_smul c).bounded_image hs
+#align metric.bounded.smul Metric.Bounded.smul₀
 
 /-- If `s` is a bounded set, then for small enough `r`, the set `{x} + r • s` is contained in any
 fixed neighborhood of `x`. -/
diff --git a/Mathlib/Topology/MetricSpace/IsometricSMul.lean b/Mathlib/Topology/MetricSpace/IsometricSMul.lean
index 009c301963c7b..44abf0fe90bbb 100644
--- a/Mathlib/Topology/MetricSpace/IsometricSMul.lean
+++ b/Mathlib/Topology/MetricSpace/IsometricSMul.lean
@@ -425,6 +425,15 @@ theorem nndist_div_left [Group G] [PseudoMetricSpace G] [IsometricSMul G G]
 
 namespace Metric
 
+/-- If `G` acts isometrically on `X`, then the image of a bounded set in `X` under scalar
+multiplication by `c : G` is bounded. See also `Metric.Bounded.smul₀` for a similar lemma about
+normed spaces. -/
+@[to_additive "Given an additive isometric action of `G` on `X`, the image of a bounded set in `X`
+under translation by `c : G` is bounded"]
+theorem Bounded.smul [PseudoMetricSpace X] [SMul G X] [IsometricSMul G X] {s : Set X}
+    (hs : Bounded s) (c : G) : Bounded (c • s) :=
+  (isometry_smul X c).lipschitz.bounded_image hs
+
 variable [PseudoMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X]
 
 @[to_additive (attr := simp)]