src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy

   have "\<And>i. eventually (\<lambda>x. f x $ i \<in> A i) net"
     using assms A by (rule topological_tendstoD)
   hence "eventually (\<lambda>x. \<forall>i. f x $ i \<in> A i) net"
     by (rule eventually_all_finite)
   thus "eventually (\<lambda>x. f x \<in> S) net"
-    by (rule eventually_elim1, simp add: S)
+    by (rule eventually_mono, simp add: S)
 qed
 
 lemma tendsto_vec_lambda [tendsto_intros]:
   assumes "\<And>i. ((\<lambda>x. f x i) ---> a i) net"
   shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net"