src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

     with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
       unfolding continuous_within tendsto_def eventually_within by auto
     have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
       using x(2) `d>0` by simp
     hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
-    proof (rule eventually_elim1)
-      fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
+    proof eventually_elim
+      case (elim n) thus ?case
         using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
     qed
   }
   thus ?rhs unfolding tendsto_iff unfolding tendsto_def by simp
 next