src/HOL/Analysis/Lipschitz.thy

   obtain d where d: "d>0" "\<And>x'. x'\<in>T \<Longrightarrow> dist x' t < d \<Longrightarrow> dist (g x') (g t) < u"
     by (auto)
   show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on  (cball x u \<inter> X) (f (g t))"
     using d \<open>0 < u\<close>
     by (fastforce intro: exI[where x="(min d u)/2"] exI[where x=L]
-      intro!: less_imp_le[OF d(2)] lipschitz_on_subset[OF l] simp: dist_commute mem_ball mem_cball)
+      intro!: less_imp_le[OF d(2)] lipschitz_on_subset[OF l] simp: dist_commute)
 qed
 
 context
   fixes T::"'a::metric_space set" and X f
   assumes local_lipschitz: "local_lipschitz T X f"

     note \<open>dist x a < ?d\<close>
     also have "?d \<le> u" by simp
     finally have "dist x a < u" .
     then have "x \<in> cball a u \<inter> T"
       using \<open>x \<in> T\<close>
-      by (auto simp: dist_commute mem_cball)
+      by (auto simp: dist_commute)
     have "dist (f x y) (f a b) \<le> dist (f x y) (f x b) + dist (f x b) (f a b)"
       by (rule dist_triangle)
     also have "(L + 1)-lipschitz_on (cball b u \<inter> X) (f x)"
       using L[OF \<open>x \<in> cball a u \<inter> T\<close>]
       by (rule lipschitz_on_le) simp

     from L lt ly lx \<open>lx = ly\<close>
     have
       "eventually (\<lambda>n. ?t n \<in> ball lt u) sequentially"
       "eventually (\<lambda>n. ?y n \<in> ball lx u) sequentially"
       "eventually (\<lambda>n. ?x n \<in> ball lx u) sequentially"
-      by (auto simp: dist_commute Lim mem_ball)
+      by (auto simp: dist_commute Lim)
     moreover have "eventually (\<lambda>n. n > L) sequentially"
       by (metis filterlim_at_top_dense filterlim_real_sequentially)
     ultimately
     have "eventually (\<lambda>_. False) sequentially"
     proof eventually_elim
       case (elim n)
       hence "dist (f (?t n) (?y n)) (f (?t n) (?x n)) \<le> L * dist (?y n) (?x n)"
         using assms xy t
         unfolding dist_norm[symmetric]
-        by (intro lipschitz_onD[OF L(2)]) (auto simp: mem_ball mem_cball)
+        by (intro lipschitz_onD[OF L(2)]) (auto)
       also have "\<dots> \<le> n * dist (?y n) (?x n)"
         using elim by (intro mult_right_mono) auto
       also have "\<dots> \<le> rx (ry (rt n)) * dist (?y n) (?x n)"
         by (intro mult_right_mono[OF _ zero_le_dist])
            (meson lt'(2) lx'(2) ly'(2) of_nat_le_iff order_trans seq_suble)

   obtain u L v M where "0 < u" "(\<And>s. s \<in> cball t u \<inter> A \<Longrightarrow> L-lipschitz_on (cball x u \<inter> B) (f s))"
     "0 < v" "(\<And>s. s \<in> cball t v \<inter> A \<Longrightarrow> M-lipschitz_on (cball x v \<inter> B) (g s))"
     by metis
   then show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> A. L-lipschitz_on (cball x u \<inter> B) (\<lambda>b. (f t b, g t b))"
     by (intro exI[where x="min u v"])
-      (force intro: lipschitz_on_subset intro!: lipschitz_on_Pair simp: mem_cball)
+      (force intro: lipschitz_on_subset intro!: lipschitz_on_Pair)
 qed
 
 lemma local_lipschitz_constI: "local_lipschitz S T (\<lambda>t x. f t)"
   by (auto simp: intro!: local_lipschitzI lipschitz_on_constant intro: exI[where x=1])
 

   have "compact (cball t v \<times> cball x u)" "cball t v \<times> cball x u \<subseteq> T \<times> X"
     by (auto intro!: compact_Times)
   then have "compact (f' ` (cball t v \<times> cball x u))"
     by (auto intro!: compact_continuous_image continuous_on_subset[OF cont_f'])
   then obtain B where B: "B > 0" "\<And>s y. s \<in> cball t v \<Longrightarrow> y \<in> cball x u \<Longrightarrow> norm (f' (s, y)) \<le> B"
-    by (auto dest!: compact_imp_bounded simp: bounded_pos simp: mem_ball)
+    by (auto dest!: compact_imp_bounded simp: bounded_pos)
 
   have lipschitz: "B-lipschitz_on (cball x (min u v) \<inter> X) (f s)" if s: "s \<in> cball t v" for s
   proof -
     note s
     also note \<open>cball t v \<subseteq> T\<close>

     have "norm (f s y - f s z) \<le> B * norm (y - z)"
       if "y \<in> cball x u" "z \<in> cball x u"
       for y z
       using s that
       by (intro differentiable_bound[OF convex_cball deriv])
-        (auto intro!: B  simp: norm_blinfun.rep_eq[symmetric] mem_cball)
+        (auto intro!: B  simp: norm_blinfun.rep_eq[symmetric])
     then show ?thesis
       using \<open>0 < B\<close>
-      by (auto intro!: lipschitz_onI simp: dist_norm mem_cball)
+      by (auto intro!: lipschitz_onI simp: dist_norm)
   qed
   show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)"
-    by (force intro: exI[where x="min u v"] exI[where x=B] intro!: lipschitz simp: u v mem_cball)
+    by (force intro: exI[where x="min u v"] exI[where x=B] intro!: lipschitz simp: u v)
 qed
 
 end