A couple of new lemmas

--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed Apr 09 22:45:04 2025 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Apr 10 17:07:18 2025 +0100
@@ -223,27 +223,17 @@
   assumes "a \<noteq> 0"
   shows   "(\<lambda>x. a *\<^sub>R x) ` cball c r = cball (a *\<^sub>R c :: 'a :: real_normed_vector) (\<bar>a\<bar> * r)"
 proof -
-  have 1: "(\<lambda>x. a *\<^sub>R x) ` cball c r \<subseteq> cball (a *\<^sub>R c) (\<bar>a\<bar> * r)" if "a \<noteq> 0" for a r and c :: 'a
-  proof safe
-    fix x
-    assume x: "x \<in> cball c r"
-    have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)"
-      by (auto simp: dist_norm)
-    also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)"
-      by (simp add: algebra_simps)
-    finally show "a *\<^sub>R x \<in> cball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
-      using that x by (auto simp: dist_norm)
-  qed
-
+  have *: "(\<lambda>x. a *\<^sub>R x) ` cball c r \<subseteq> cball (a *\<^sub>R c) (\<bar>a\<bar> * r)" for a r and c :: 'a
+    by (auto simp: dist_norm simp flip: scaleR_right_diff_distrib intro!: mult_left_mono)
   have "cball (a *\<^sub>R c) (\<bar>a\<bar> * r) = (\<lambda>x. a *\<^sub>R x) ` (\<lambda>x. inverse a *\<^sub>R x) ` cball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
     unfolding image_image using assms by simp
   also have "\<dots> \<subseteq> (\<lambda>x. a *\<^sub>R x) ` cball (inverse a *\<^sub>R (a *\<^sub>R c)) (\<bar>inverse a\<bar> * (\<bar>a\<bar> * r))"
-    using assms by (intro image_mono 1) auto
+    using "*" by blast
   also have "\<dots> = (\<lambda>x. a *\<^sub>R x) ` cball c r"
     using assms by (simp add: algebra_simps)
   finally have "cball (a *\<^sub>R c) (\<bar>a\<bar> * r) \<subseteq> (\<lambda>x. a *\<^sub>R x) ` cball c r" .
   moreover from assms have "(\<lambda>x. a *\<^sub>R x) ` cball c r \<subseteq> cball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
-    by (intro 1) auto
+    using "*" by blast
   ultimately show ?thesis by blast
 qed
 
@@ -251,27 +241,54 @@
   assumes "a \<noteq> 0"
   shows   "(\<lambda>x. a *\<^sub>R x) ` ball c r = ball (a *\<^sub>R c :: 'a :: real_normed_vector) (\<bar>a\<bar> * r)"
 proof -
-  have 1: "(\<lambda>x. a *\<^sub>R x) ` ball c r \<subseteq> ball (a *\<^sub>R c) (\<bar>a\<bar> * r)" if "a \<noteq> 0" for a r and c :: 'a
-  proof safe
-    fix x
-    assume x: "x \<in> ball c r"
-    have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)"
-      by (auto simp: dist_norm)
-    also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)"
-      by (simp add: algebra_simps)
-    finally show "a *\<^sub>R x \<in> ball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
-      using that x by (auto simp: dist_norm)
-  qed
-
+  have *: "(\<lambda>x. a *\<^sub>R x) ` ball c r \<subseteq> ball (a *\<^sub>R c) (\<bar>a\<bar> * r)" if "a \<noteq> 0" for a r and c :: 'a
+    using that by (auto simp: dist_norm simp flip: scaleR_right_diff_distrib)
   have "ball (a *\<^sub>R c) (\<bar>a\<bar> * r) = (\<lambda>x. a *\<^sub>R x) ` (\<lambda>x. inverse a *\<^sub>R x) ` ball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
     unfolding image_image using assms by simp
   also have "\<dots> \<subseteq> (\<lambda>x. a *\<^sub>R x) ` ball (inverse a *\<^sub>R (a *\<^sub>R c)) (\<bar>inverse a\<bar> * (\<bar>a\<bar> * r))"
-    using assms by (intro image_mono 1) auto
+    using assms by (intro image_mono *) auto
   also have "\<dots> = (\<lambda>x. a *\<^sub>R x) ` ball c r"
     using assms by (simp add: algebra_simps)
   finally have "ball (a *\<^sub>R c) (\<bar>a\<bar> * r) \<subseteq> (\<lambda>x. a *\<^sub>R x) ` ball c r" .
   moreover from assms have "(\<lambda>x. a *\<^sub>R x) ` ball c r \<subseteq> ball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
-    by (intro 1) auto
+    by (intro *) auto
+  ultimately show ?thesis by blast
+qed
+
+lemma sphere_scale:
+  assumes "a \<noteq> 0"
+  shows   "(\<lambda>x. a *\<^sub>R x) ` sphere c r = sphere (a *\<^sub>R c :: 'a :: real_normed_vector) (\<bar>a\<bar> * r)"
+proof -
+  have *: "(\<lambda>x. a *\<^sub>R x) ` sphere c r \<subseteq> sphere (a *\<^sub>R c) (\<bar>a\<bar> * r)" for a r and c :: 'a
+    by (metis (no_types, opaque_lifting) scaleR_right_diff_distrib dist_norm image_subsetI mem_sphere norm_scaleR)
+  have "sphere (a *\<^sub>R c) (\<bar>a\<bar> * r) = (\<lambda>x. a *\<^sub>R x) ` (\<lambda>x. inverse a *\<^sub>R x) ` sphere (a *\<^sub>R c) (\<bar>a\<bar> * r)"
+    unfolding image_image using assms by simp
+  also have "\<dots> \<subseteq> (\<lambda>x. a *\<^sub>R x) ` sphere (inverse a *\<^sub>R (a *\<^sub>R c)) (\<bar>inverse a\<bar> * (\<bar>a\<bar> * r))"
+    using "*" by blast
+  also have "\<dots> = (\<lambda>x. a *\<^sub>R x) ` sphere c r"
+    using assms by (simp add: algebra_simps)
+  finally have "sphere (a *\<^sub>R c) (\<bar>a\<bar> * r) \<subseteq> (\<lambda>x. a *\<^sub>R x) ` sphere c r" .
+  moreover have "(\<lambda>x. a *\<^sub>R x) ` sphere c r \<subseteq> sphere (a *\<^sub>R c) (\<bar>a\<bar> * r)"
+    using "*" by blast
+  ultimately show ?thesis by blast
+qed
+
+text \<open>As above, but scaled by a complex number\<close>
+lemma sphere_cscale:
+  assumes "a \<noteq> 0"
+  shows   "(\<lambda>x. a * x) ` sphere c r = sphere (a * c :: complex) (cmod a * r)"
+proof -
+  have *: "(\<lambda>x. a * x) ` sphere c r \<subseteq> sphere (a * c) (cmod a * r)" for a r c
+    using dist_mult_left by fastforce
+  have "sphere (a * c) (cmod a * r) = (\<lambda>x. a * x) ` (\<lambda>x. inverse a * x) ` sphere (a * c) (cmod a * r)"
+    by (simp add: image_image inverse_eq_divide)
+  also have "\<dots> \<subseteq> (\<lambda>x. a * x) ` sphere (inverse a * (a * c)) (cmod (inverse a) * (cmod a * r))"
+    using "*" by blast
+  also have "\<dots> = (\<lambda>x. a * x) ` sphere c r"
+    using assms by (simp add: field_simps flip: norm_mult)
+  finally have "sphere (a * c) (cmod a * r) \<subseteq> (\<lambda>x. a * x) ` sphere c r" .
+  moreover have "(\<lambda>x. a * x) ` sphere c r \<subseteq> sphere (a * c) (cmod a * r)"
+    using "*" by blast
   ultimately show ?thesis by blast
 qed
 

--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Wed Apr 09 22:45:04 2025 +0200
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Thu Apr 10 17:07:18 2025 +0100
@@ -2356,14 +2356,6 @@
   shows   "zorder f z = 0 \<longleftrightarrow> f z \<noteq> 0"
   using assms zorder_eq_0I zorder_pos_iff' by fastforce
 
-lemma dist_mult_left:
-  "dist (a * b) (a * c :: 'a :: real_normed_field) = norm a * dist b c"
-  unfolding dist_norm right_diff_distrib [symmetric] norm_mult by simp
-
-lemma dist_mult_right:
-  "dist (b * a) (c * a :: 'a :: real_normed_field) = norm a * dist b c"
-  using dist_mult_left[of a b c] by (simp add: mult_ac)
-
 lemma zorder_scale:
   assumes "f analytic_on {a * z}" "eventually (\<lambda>w. f w \<noteq> 0) (at (a * z))" "a \<noteq> 0"
   shows "zorder (\<lambda>w. f (a * w)) z = zorder f (a * z)"

--- a/src/HOL/Real_Vector_Spaces.thy	Wed Apr 09 22:45:04 2025 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Apr 10 17:07:18 2025 +0100
@@ -796,6 +796,14 @@
 
 class real_normed_field = real_field + real_normed_div_algebra
 
+lemma dist_mult_left:
+  "dist (a * b) (a * c :: 'a :: real_normed_field) = norm a * dist b c"
+  unfolding dist_norm right_diff_distrib [symmetric] norm_mult by simp
+
+lemma dist_mult_right:
+  "dist (b * a) (c * a :: 'a :: real_normed_field) = norm a * dist b c"
+  using dist_mult_left[of a b c] by (simp add: mult_ac)
+
 instance real_normed_div_algebra < real_normed_algebra_1
 proof
   show "norm (x * y) \<le> norm x * norm y" for x y :: 'a