adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 09:41:29 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 09:56:34 2010 -0700
@@ -5336,7 +5336,7 @@
     unfolding dist_norm
     apply (auto simp add: pos_divide_less_eq mult_strict_left_mono)
     unfolding continuous_on
-    by (intro ballI tendsto_intros, simp, assumption)+
+    by (intro ballI tendsto_intros, simp)+
 next
   have *:"\<bar>e / d\<bar> > 0" "\<bar>d / e\<bar> >0" using assms using divide_pos_pos by auto
   show ?cth unfolding homeomorphic_minimal
@@ -5346,7 +5346,7 @@
     unfolding dist_norm
     apply (auto simp add: pos_divide_le_eq)
     unfolding continuous_on
-    by (intro ballI tendsto_intros, simp, assumption)+
+    by (intro ballI tendsto_intros, simp)+
 qed
 
 text{* "Isometry" (up to constant bounds) of injective linear map etc.           *}