src/HOL/Analysis/Further_Topology.thy

         have [simp]: "(z*x / z')^n = x^n" if "x \<noteq> 0" for x
           using z' that by (simp add: field_simps \<open>z \<noteq> 0\<close>)
         have [simp]: "cmod (z - z * x / z') = cmod (z' - x)" if "x \<noteq> 0" for x
         proof -
           have "cmod (z - z * x / z') = cmod z * cmod (1 - x / z')"
-            by (metis (no_types) ab_semigroup_mult_class.mult_ac(1) complex_divide_def mult.right_neutral norm_mult right_diff_distrib')
+            by (metis (no_types) ab_semigroup_mult_class.mult_ac(1) divide_complex_def mult.right_neutral norm_mult right_diff_distrib')
           also have "... = cmod z' * cmod (1 - x / z')"
             by (simp add: nz')
           also have "... = cmod (z' - x)"
             by (simp add: \<open>z' \<noteq> 0\<close> diff_divide_eq_iff norm_divide)
           finally show ?thesis .

         have [simp]: "cmod (z' - z' * x / z) = cmod (z - x)" if "x \<noteq> 0" for x
         proof -
           have "cmod (z * (1 - x * inverse z)) = cmod (z - x)"
             by (metis \<open>z \<noteq> 0\<close> diff_divide_distrib divide_complex_def divide_self_if nonzero_eq_divide_eq semiring_normalization_rules(7))
           then show ?thesis
-            by (metis (no_types) mult.assoc complex_divide_def mult.right_neutral norm_mult nz' right_diff_distrib')
+            by (metis (no_types) mult.assoc divide_complex_def mult.right_neutral norm_mult nz' right_diff_distrib')
         qed
         show ?thesis
           unfolding image_def ball_def
           apply safe
           apply simp_all