# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1601927903 -3600
# Node ID 6cacbdb536375e631c56d17f55585952e81fb46a
# Parent  15ea20d8a4d63201272a28291dfbeef05921e6e2
still not quite fixed...

diff -r 15ea20d8a4d6 -r 6cacbdb53637 src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy	Mon Oct 05 18:48:41 2020 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy	Mon Oct 05 20:58:23 2020 +0100
@@ -1366,11 +1366,7 @@
       and p: "polynomial_function p" "path_image p \<subseteq> S"
       and pi: "\<And>f. f holomorphic_on S \<Longrightarrow> contour_integral g f = contour_integral p f"
     using contour_integral_nearby_ends [OF S \<open>path g\<close> pag]
-    apply clarify
-    apply (drule_tac x=g in spec)
-    apply (simp only: assms)
-    apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function)
-    done
+    by (metis cancel_comm_monoid_add_class.diff_cancel g norm_zero path_approx_polynomial_function valid_path_polynomial_function)
   then obtain p' where p': "polynomial_function p'"
     "\<And>x. (p has_vector_derivative (p' x)) (at x)"
     by (blast intro: has_vector_derivative_polynomial_function that)
diff -r 15ea20d8a4d6 -r 6cacbdb53637 src/HOL/Complex_Analysis/Winding_Numbers.thy
--- a/src/HOL/Complex_Analysis/Winding_Numbers.thy	Mon Oct 05 18:48:41 2020 +0100
+++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy	Mon Oct 05 20:58:23 2020 +0100
@@ -41,7 +41,8 @@
       assume e: "e>0"
       obtain p where p: "polynomial_function p \<and>
             pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and> (\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < min e (d/2))"
-        using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "min e (d/2)"] d \<open>0<e\<close> by auto
+        using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "min e (d/2)"] d \<open>0<e\<close>
+        by (metis min_less_iff_conj zero_less_divide_iff zero_less_numeral) 
       have "(\<lambda>w. 1 / (w - z)) holomorphic_on UNIV - {z}"
         by (auto simp: intro!: holomorphic_intros)
       then have "winding_number_prop \<gamma> z e p nn"
@@ -845,7 +846,8 @@
       obtain p where p: "polynomial_function p" "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>"
                  and pg1: "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> cmod (p t - \<gamma> t) < 1)"
                  and pge: "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> cmod (p t - \<gamma> t) < e)"
-        using path_approx_polynomial_function [OF \<gamma>, of "min 1 e"] \<open>e>0\<close> by force
+        using path_approx_polynomial_function [OF \<gamma>, of "min 1 e"] \<open>e>0\<close>
+        by (metis atLeastAtMost_iff min_less_iff_conj zero_less_one)
       have pip: "path_image p \<subseteq> ball 0 (B + 1)"
         using B
         apply (clarsimp simp add: path_image_def dist_norm ball_def)