diff -r 785615e37846 -r 451f428c5814 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Thu Apr 10 17:07:18 2025 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Fri Apr 11 21:56:56 2025 +0100
@@ -2810,7 +2810,7 @@
         by simp
     qed
     have "\<exists>!x \<in> ?D. ?u x = x"
-    proof (rule banach_fix)
+    proof (rule Banach_fix)
       show "cball 0 \<delta> \<noteq> {}"
         using \<open>0 < \<delta>\<close> by auto
       show "(\<lambda>x. x + (y - f x)) ` cball 0 \<delta> \<subseteq> cball 0 \<delta>"