src/HOL/Analysis/Infinite_Sum.thy

       by (metis dist_commute dist_norm)
     then obtain F where "norm (a - sum f F) \<le> \<epsilon>"
       and "finite F" and "F \<subseteq> A"
       by (simp add: atomize_elim)
     hence "norm a \<le> norm (sum f F) + \<epsilon>"
-      by (smt norm_triangle_sub)
+      by (metis add.commute diff_add_cancel dual_order.refl norm_triangle_mono)
     also have "\<dots> \<le> sum (\<lambda>x. norm (f x)) F + \<epsilon>"
       using norm_sum by auto
     also have "\<dots> \<le> n + \<epsilon>"
       apply (rule add_right_mono)
       apply (rule has_sum_mono_neutral[where A=F and B=A and f=\<open>\<lambda>x. norm (f x)\<close> and g=\<open>\<lambda>x. norm (f x)\<close>])

       by (metis (no_types, lifting) eventually_mono filterlim_iff finite_subsets_at_top_neq_bot tendsto_Lim)
     then obtain X where "(\<Sum>x\<in>X. norm (f x)) \<in> S"
       by blast
     hence "(\<Sum>x\<in>X. norm (f x)) < 0"
       unfolding S_def by auto      
-    thus False using sumpos by smt
+    thus False by (simp add: leD sumpos)
   qed
   have "\<exists>!h. (sum (\<lambda>x. norm (f x)) \<longlongrightarrow> h) (finite_subsets_at_top A)"
     using t_def finite_subsets_at_top_neq_bot tendsto_unique by blast
   hence "t = (Topological_Spaces.Lim (finite_subsets_at_top A) (sum (\<lambda>x. norm (f x))))"
     using t_def unfolding Topological_Spaces.Lim_def