diff -r 94bc8f62c835 -r 07c51801c2ea src/HOL/Library/Interval.thy
--- a/src/HOL/Library/Interval.thy	Mon Aug 26 22:14:19 2024 +0100
+++ b/src/HOL/Library/Interval.thy	Fri Aug 30 10:16:48 2024 +0100
@@ -564,16 +564,7 @@
   using that
   apply transfer
   apply (clarsimp simp add: Let_def)
-  apply (intro conjI)
-         apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-        apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-       apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-      apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-     apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-    apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-   apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-  apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-  done
+  by (smt (verit, best) linorder_le_cases max.coboundedI1 max.coboundedI2 min.absorb1 min.coboundedI2 mult_left_mono mult_left_mono_neg)
 
 lemma set_of_distrib_left:
   "set_of (B * (A1 + A2)) \<subseteq> set_of (B * A1 + B * A2)"
@@ -595,19 +586,7 @@
   "set_of ((A1 + A2) * B) \<subseteq> set_of (A1 * B + A2 * B)"
   for A1 A2 B :: "'a::{linordered_ring, real_normed_algebra, linear_continuum_topology} interval"
   unfolding set_of_times set_of_plus set_plus_def
-  apply clarsimp
-  subgoal for b a1 a2
-    apply (rule exI[where x="a1 * b"])
-    apply (rule conjI)
-    subgoal by force
-    subgoal
-      apply (rule exI[where x="a2 * b"])
-      apply (rule conjI)
-      subgoal by force
-      subgoal by (simp add: algebra_simps)
-      done
-    done
-  done
+  using distrib_right by blast
 
 lemma set_of_mul_inc_left:
   "set_of (A * B) \<subseteq> set_of (A' * B)"
@@ -671,10 +650,7 @@
       mult_bounds_enclose_zero1 mult_bounds_enclose_zero2)
 
 instance "interval" :: ("{linordered_semiring, zero, times}") mult_zero
-  apply standard
-  subgoal by transfer auto
-  subgoal by transfer auto
-  done
+  by (standard; transfer; auto)
 
 lift_definition min_interval::"'a::linorder interval \<Rightarrow> 'a interval \<Rightarrow> 'a interval" is
   "\<lambda>(l1, u1). \<lambda>(l2, u2). (min l1 l2, min u1 u2)"