diff -r 1a5d4586b6b0 -r 0263787a06b4 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sat Dec 04 17:23:42 2021 +0100
+++ b/src/HOL/Deriv.thy	Sat Dec 04 20:30:16 2021 +0000
@@ -1611,7 +1611,7 @@
     and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   obtains \<xi> where "a < \<xi>" "\<xi> < b" "f b - f a = (f' \<xi>) (b - a)"
 proof -
-  have "\<exists>x. a < x \<and> x < b \<and> (\<lambda>y. f' x y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)"
+  have "\<exists>\<xi>. a < \<xi> \<and> \<xi> < b \<and> (\<lambda>y. f' \<xi> y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)"
   proof (intro Rolle_deriv[OF \<open>a < b\<close>])
     fix x
     assume x: "a < x" "x < b"
@@ -1619,12 +1619,8 @@
           has_derivative (\<lambda>y. f' x y - (f b - f a) / (b - a) * y)) (at x)"
       by (intro derivative_intros derf[OF x])
   qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>)
-  then obtain \<xi> where
-    "a < \<xi>" "\<xi> < b" "(\<lambda>y. f' \<xi> y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)" 
-    by metis
   then show ?thesis
-    by (metis (no_types, opaque_lifting) that add.right_neutral add_diff_cancel_left' add_diff_eq \<open>a < b\<close>
-                 less_irrefl nonzero_eq_divide_eq)
+    by (smt (verit, ccfv_SIG) pos_le_divide_eq pos_less_divide_eq that)
 qed
 
 theorem MVT: