--- a/src/HOL/Analysis/Lipschitz.thy Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Tue Mar 31 15:51:15 2020 +0200
@@ -684,7 +684,7 @@
from this elim d[of "rx (ry (rt n))"]
have "\<dots> < dist (f (?t n) (?y n)) (f (?t n) (?x n)) / rx (ry (rt (n)))"
using lx'(2) ly'(2) lt'(2) \<open>0 < rx _\<close>
- by (auto simp add: field_split_simps algebra_simps strict_mono_def)
+ by (auto simp add: field_split_simps strict_mono_def)
also have "\<dots> \<le> diameter ?S / n"
by (force intro!: \<open>0 < n\<close> strict_mono_def xy diameter_bounded_bound frac_le
compact_imp_bounded compact t