diff --git a/lib/Word_Lib/Word_Lemmas.thy b/lib/Word_Lib/Word_Lemmas.thy
index 20c522c2ce..965ace53e7 100644
--- a/lib/Word_Lib/Word_Lemmas.thy
+++ b/lib/Word_Lib/Word_Lemmas.thy
@@ -496,7 +496,7 @@ next
       ultimately show ?thesis
         using \<open>y < LENGTH('a)\<close>
         by (auto simp add: drop_bit_eq_div word_less_nat_alt unat_div unat_word_ariths
-          shiftr_def shiftl_def)
+                           shiftr_def shiftl_def)
     next
       case False
       with \<open>y < n\<close> have *: \<open>unat x \<noteq> 2 ^ n div 2 ^ y\<close>
@@ -508,8 +508,9 @@ next
       also have \<open>\<dots> \<longleftrightarrow> unat x < 2 ^ n div 2 ^ y\<close>
         using * by (simp add: less_le)
       finally show ?thesis
-      using that \<open>x \<noteq> 0\<close> by (simp flip: push_bit_eq_mult drop_bit_eq_div
-        add: shiftr_def shiftl_def unat_drop_bit_eq word_less_iff_unsigned [where ?'a = nat])
+        using that \<open>x \<noteq> 0\<close>
+        by (simp flip: push_bit_eq_mult drop_bit_eq_div
+                 add: shiftr_def shiftl_def unat_drop_bit_eq word_less_iff_unsigned [where ?'a = nat])
     qed
   qed
 qed
@@ -716,7 +717,8 @@ lemma word_and_notzeroD:
 lemma shiftr_le_0:
   "unat (w::'a::len word) < 2 ^ n \<Longrightarrow> w >> n = (0::'a::len word)"
   by (auto simp add: take_bit_word_eq_self_iff word_less_nat_alt shiftr_def
-    simp flip: take_bit_eq_self_iff_drop_bit_eq_0 intro: ccontr)
+           simp flip: take_bit_eq_self_iff_drop_bit_eq_0
+           intro: ccontr)
 
 lemma of_nat_shiftl:
   "(of_nat x << n) = (of_nat (x * 2 ^ n) :: ('a::len) word)"
@@ -1466,12 +1468,9 @@ lemma mask_shift_sum:
   "\<lbrakk> a \<ge> b; unat n = unat (p AND mask b) \<rbrakk>
    \<Longrightarrow> (p AND NOT(mask a)) + (p AND mask a >> b) * (1 << b) + n = (p :: 'a :: len word)"
   apply (simp add: shiftl_def shiftr_def flip: push_bit_eq_mult take_bit_eq_mask word_unat_eq_iff)
-  apply (subst disjunctive_add)
-   apply (auto simp add: bit_simps)
-  apply (subst disjunctive_add)
-   apply (auto simp add: bit_simps)
-    apply (rule bit_word_eqI)
-  apply (auto simp add: bit_simps)
+  apply (subst disjunctive_add, fastforce simp: bit_simps)+
+  apply (rule bit_word_eqI)
+  apply (fastforce simp: bit_simps)[1]
   done
 
 lemma is_up_compose:
@@ -1586,10 +1585,7 @@ next
     apply (rule impI)
     apply (subst bit_eq_iff)
     apply (simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def)
-    apply (auto simp add: Suc_le_eq)
-    using less_imp_le_nat apply blast
-    using less_imp_le_nat apply blast
-    done
+    by (auto simp add: Suc_le_eq) (meson dual_order.strict_iff_not)+
 qed
 
 lemma scast_ucast_mask_compare:
@@ -1823,11 +1819,7 @@ proof (rule classical)
      apply (insert sdiv_int_range [where a="sint a" and b="sint b"])[1]
      apply (clarsimp simp: word_size)
     apply (insert sdiv_int_range [where a="sint a" and b="sint b"])[1]
-    apply auto
-    apply (cases \<open>size a\<close>)
-     apply simp_all
-    apply (smt (z3) One_nat_def diff_Suc_1 signed_word_eqI sint_int_min sint_range_size wsst_TYs(3))
-    done
+    by (smt (verit, best) One_nat_def signed_word_eqI sint_greater_eq sint_int_min sint_less wsst_TYs(3))
 
   have result_range_simple: "(sint a sdiv sint b \<in> ?range) \<Longrightarrow> ?thesis"
     apply (insert sdiv_int_range [where a="sint a" and b="sint b"])