diff -r 413a86331bf6 -r 898034c8a799 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Wed Jun 19 10:20:35 2024 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Wed Jun 19 12:13:16 2024 +0200
@@ -10,9 +10,8 @@
 
 text \<open>The combinatorial argument is in theory \<open>Exponent\<close>.\<close>
 
-lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c"
-  for c :: nat
-  by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero)
+lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c" for c :: nat
+  using gr0_conv_Suc by fastforce
 
 locale sylow = group +
   fixes p and a and m and calM and RelM
@@ -30,15 +29,9 @@
   by (auto simp: refl_on_def RelM_def calM_def) (blast intro!: coset_mult_one [symmetric])
 
 lemma RelM_sym: "sym RelM"
-proof (unfold sym_def RelM_def, clarify)
-  fix y g
-  assume "y \<in> calM"
-    and g: "g \<in> carrier G"
-  then have "y = y #> g #> (inv g)"
-    by (simp add: coset_mult_assoc calM_def)
-  then show "\<exists>g'\<in>carrier G. y = y #> g #> g'"
-    by (blast intro: g)
-qed
+  unfolding sym_def RelM_def calM_def
+  using coset_mult_assoc coset_mult_one r_inv_ex
+  by (smt (verit, best) case_prod_conv mem_Collect_eq)
 
 lemma RelM_trans: "trans RelM"
   by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
@@ -62,14 +55,13 @@
 begin
 
 lemma M_subset_calM: "M \<subseteq> calM"
-  by (rule M_in_quot [THEN M_subset_calM_prep])
+  by (simp add: M_in_quot M_subset_calM_prep)
 
 lemma card_M1: "card M1 = p^a"
   using M1_in_M M_subset_calM calM_def by blast
 
 lemma exists_x_in_M1: "\<exists>x. x \<in> M1"
-  using prime_p [THEN prime_gt_Suc_0_nat] card_M1
-  by (metis Suc_lessD card_eq_0_iff empty_subsetI equalityI gr_implies_not0 nat_zero_less_power_iff subsetI)
+  using prime_p [THEN prime_gt_Suc_0_nat] card_M1 one_in_subset by fastforce
 
 lemma M1_subset_G [simp]: "M1 \<subseteq> carrier G"
   using M1_in_M M_subset_calM calM_def mem_Collect_eq subsetCE by blast
@@ -77,25 +69,14 @@
 lemma M1_inj_H: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H"
 proof -
   from exists_x_in_M1 obtain m1 where m1M: "m1 \<in> M1"..
-  have m1: "m1 \<in> carrier G"
-    by (simp add: m1M M1_subset_G [THEN subsetD])
   show ?thesis
   proof
-    show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
-      by (simp add: H_def inj_on_def m1)
+    have "m1 \<in> carrier G"
+      by (simp add: m1M M1_subset_G [THEN subsetD])
+    then show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
+      by (simp add: H_def inj_on_def)
     show "restrict ((\<otimes>) m1) H \<in> H \<rightarrow> M1"
-    proof (rule restrictI)
-      fix z
-      assume zH: "z \<in> H"
-      show "m1 \<otimes> z \<in> M1"
-      proof -
-        from zH
-        have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
-          by (auto simp add: H_def)
-        show ?thesis
-          by (rule subst [OF M1zeq]) (simp add: m1M zG rcosI)
-      qed
-    qed
+      using H_def m1M rcosI by auto
   qed
 qed
 
@@ -108,7 +89,7 @@
 begin
 
 lemma EmptyNotInEquivSet: "{} \<notin> calM // RelM"
-  by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
+  using RelM_equiv in_quotient_imp_non_empty by blast
 
 lemma existsM1inM: "M \<in> calM // RelM \<Longrightarrow> \<exists>M1. M1 \<in> M"
   using RelM_equiv equiv_Eps_in by blast
@@ -131,10 +112,8 @@
   with zero_less_card_calM prime_p
   have "Suc (multiplicity p m) \<le> multiplicity p (card calM)"
     by (intro multiplicity_geI) auto
-  then have "multiplicity p m < multiplicity p (card calM)" by simp
-  also have "multiplicity p m = multiplicity p (card calM)"
-    by (simp add: const_p_fac prime_p zero_less_m card_calM)
-  finally show False by simp
+  then show False
+    by (simp add: card_calM const_p_fac prime_p zero_less_m)
 qed
 
 lemma finite_calM: "finite calM"
@@ -171,7 +150,7 @@
   show "H \<subseteq> carrier G"
     using H_into_carrier_G by blast
   show "\<And>a. a \<in> H \<Longrightarrow> inv a \<in> H"
-    by (metis H_I H_into_carrier_G H_m_closed M1_subset_G Units_eq Units_inv_closed Units_inv_inv coset_mult_inv1 in_H_imp_eq)
+    by (metis H_I H_into_carrier_G M1_subset_G coset_mult_assoc coset_mult_one in_H_imp_eq inv_closed r_inv)
   show "\<And>a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
     by (blast intro: H_m_closed)
 qed (use H_not_empty in auto)
@@ -237,12 +216,12 @@
     assume eq: "H #> ?inv x = H #> ?inv y" and xy: "x \<in> M" "y \<in> M"
     have "x = M1 #> ?inv x"
       by (simp add: M_elem_map_eq \<open>x \<in> M\<close>)
-    also have "... = M1 #> ?inv y"
+    also have "\<dots> = M1 #> ?inv y"
     proof (rule coset_mult_inv1 [OF in_H_imp_eq [OF coset_join1]])
       show "H #> ?inv x \<otimes> inv (?inv y) = H"
         by (simp add: H_into_carrier_G M_elem_map_carrier xy coset_mult_inv2 eq subsetI)
     qed (simp_all add: H_is_subgroup M_elem_map_carrier xy)
-    also have "... = y"
+    also have "\<dots> = y"
       using M_elem_map_eq \<open>y \<in> M\<close> by simp
     finally show "x=y" .
   qed
@@ -279,7 +258,7 @@
     assume eq: "M1 #> ?inv x = M1 #> ?inv y" and xy: "x \<in> rcosets H" "y \<in> rcosets H"
     have "x = H #> ?inv x"
       by (simp add: H_elem_map_eq \<open>x \<in> rcosets H\<close>)
-    also have "... = H #> ?inv y"
+    also have "\<dots> = H #> ?inv y"
     proof (rule coset_mult_inv1 [OF coset_join2])
       show "?inv x \<otimes> inv (?inv y) \<in> carrier G"
         by (simp add: H_elem_map_carrier \<open>x \<in> rcosets H\<close> \<open>y \<in> rcosets H\<close>)
@@ -288,7 +267,7 @@
       show "H \<subseteq> carrier G"
         by (simp add: H_is_subgroup subgroup.subset)
     qed (simp_all add: H_is_subgroup H_elem_map_carrier xy)
-    also have "... = y"
+    also have "\<dots> = y"
       by (simp add: H_elem_map_eq \<open>y \<in> rcosets H\<close>)
     finally show "x=y" .
   qed
@@ -305,7 +284,7 @@
 
 lemma cardMeqIndexH: "card M = card (rcosets H)"
   using inj_M_GmodH inj_GmodH_M
-  by (blast intro: card_bij finite_M H_is_subgroup rcosets_subset_PowG [THEN finite_subset])
+  by (metis H_is_subgroup card_bij finite_G finite_M finite_UnionD rcosets_part_G)
 
 lemma index_lem: "card M * card H = order G"
   by (simp add: cardMeqIndexH lagrange H_is_subgroup)
@@ -314,9 +293,10 @@
 proof (rule antisym)
   show "p^a \<le> card H"
   proof (rule dvd_imp_le)
-    show "p ^ a dvd card H"
-      apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
+    have "p ^ (a + multiplicity p m) dvd card M * card H"
       by (simp add: index_lem multiplicity_dvd order_G power_add)
+    then show "p ^ a dvd card H"
+      using div_combine not_dvd_M prime_p by blast
     show "0 < card H"
       by (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
   qed