diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Lipschitz.thy
--- 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