More theorems about limits, including cancellation simprules

--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Oct 09 14:39:10 2019 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Oct 09 15:32:41 2019 +0100
@@ -6632,7 +6632,7 @@
       by (rule tendsto_mult_left [OF tendstoI])
     then have "((\<lambda>u. g u / (u - w)) has_contour_integral 2 * of_real pi * \<i> * g w) (circlepath z r)"
       using has_contour_integral_integral [OF g_cint] tendsto_unique [OF F f_tends_cig] w
-      by (force simp: dist_norm)
+      by fastforce
     then have "((\<lambda>u. g u / (2 * of_real pi * \<i> * (u - w))) has_contour_integral g w) (circlepath z r)"
       using has_contour_integral_div [where c = "2 * of_real pi * \<i>"]
       by (force simp: field_simps)

--- a/src/HOL/Limits.thy	Wed Oct 09 14:39:10 2019 +0100
+++ b/src/HOL/Limits.thy	Wed Oct 09 15:32:41 2019 +0100
@@ -779,14 +779,26 @@
   for c :: "'a::topological_semigroup_mult"
   by (rule tendsto_mult [OF _ tendsto_const])
 
-lemma tendsto_mult_left_iff:
+lemma tendsto_mult_left_iff [simp]:
    "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. c * f x) (c * l) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
   by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"])
 
-lemma tendsto_mult_right_iff:
+lemma tendsto_mult_right_iff [simp]:
    "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. f x * c) (l * c) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
   by (auto simp: tendsto_mult_right dest: tendsto_mult_left [where c = "1/c"])
 
+lemma tendsto_zero_mult_left_iff [simp]:
+  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c \<noteq> 0" shows "(\<lambda>n. c * a n)\<longlonglongrightarrow> 0 \<longleftrightarrow> a \<longlonglongrightarrow> 0"
+  using assms tendsto_mult_left tendsto_mult_left_iff by fastforce
+
+lemma tendsto_zero_mult_right_iff [simp]:
+  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c \<noteq> 0" shows "(\<lambda>n. a n * c)\<longlonglongrightarrow> 0 \<longleftrightarrow> a \<longlonglongrightarrow> 0"
+  using assms tendsto_mult_right tendsto_mult_right_iff by fastforce
+
+lemma tendsto_zero_divide_iff [simp]:
+  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c \<noteq> 0" shows "(\<lambda>n. a n / c)\<longlonglongrightarrow> 0 \<longleftrightarrow> a \<longlonglongrightarrow> 0"
+  using tendsto_zero_mult_right_iff [of "1/c" a] assms by (simp add: field_simps)
+
 lemma lim_const_over_n [tendsto_intros]:
   fixes a :: "'a::real_normed_field"
   shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0"