diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Filter.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -1287,6 +1287,10 @@
 translations
   "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
 
+lemma filterlim_filtercomapI: "filterlim f F G \<Longrightarrow> filterlim (\<lambda>x. f (g x)) F (filtercomap g G)"
+  unfolding filterlim_def
+  by (metis order_trans filtermap_filtercomap filtermap_filtermap filtermap_mono)
+
 lemma filterlim_top [simp]: "filterlim f top F"
   by (simp add: filterlim_def)