diff -r f424e164d752 -r 5e315defb038 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Analysis/Infinite_Products.thy	Mon May 11 11:15:41 2020 +0100
@@ -1185,7 +1185,7 @@
 lemma raw_has_prod_Suc_iff: "raw_has_prod f M (a * f M) \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0"
 proof -
   have "raw_has_prod f M (a * f M) \<longleftrightarrow> (\<lambda>i. \<Prod>j\<le>Suc i. f (j+M)) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
-    by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def)
+    by (subst filterlim_sequentially_Suc) (simp add: raw_has_prod_def)
   also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
     by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod.atLeast1_atMost_eq lessThan_Suc_atMost
                   del: prod.cl_ivl_Suc)
@@ -1238,7 +1238,7 @@
   proof -
     have "(\<lambda>n. \<Prod>i\<in>{0..Suc n}. f (i + M)) \<longlonglongrightarrow> L"
       using M_L 
-      apply (subst (asm) LIMSEQ_Suc_iff[symmetric]) 
+      apply (subst (asm) filterlim_sequentially_Suc[symmetric]) 
       using atLeast0AtMost by auto
     then have "(\<lambda>n. f M * (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L"
       apply (subst (asm) prod.atLeast0_atMost_Suc_shift)