# HG changeset patch
# User wenzelm
# Date 1731525034 -3600
# Node ID 95c9af7483b1c5af27fb31b9ac7417335a33bf96
# Parent  8d2d68c8c051c881b2cd49df5873b99ca629927e
tuned proofs;

diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Chinese_Remainder.thy
--- a/src/HOL/Algebra/Chinese_Remainder.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Chinese_Remainder.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -231,11 +231,13 @@
   shows "(canonical_proj I J) ` carrier R = carrier (RDirProd (R Quot I) (R Quot J))"
   unfolding RDirProd_def DirProd_def FactRing_def A_RCOSETS_def'
 proof (auto simp add: monoid.defs)
-  { fix I i assume "ideal I R" "i \<in> I" hence "I +> i = \<zero>\<^bsub>R Quot I\<^esub>"
-      using a_rcos_zero by (simp add: FactRing_def)
-  } note aux_lemma1 = this
+  have aux_lemma1: "I +> i = \<zero>\<^bsub>R Quot I\<^esub>" if "ideal I R" "i \<in> I" for I i
+    using that a_rcos_zero by (simp add: FactRing_def)
 
-  { fix I i j assume A: "ideal I R" "i \<in> I" "j \<in> carrier R" "i \<oplus> j = \<one>"
+  have aux_lemma2: "I +> j = \<one>\<^bsub>R Quot I\<^esub>"
+    if A: "ideal I R" "i \<in> I" "j \<in> carrier R" "i \<oplus> j = \<one>"
+    for I i j
+  proof -
     have "(I +> i) \<oplus>\<^bsub>R Quot I\<^esub> (I +> j) = I +> \<one>"
       using ring_hom_memE(3)[OF ideal.rcos_ring_hom ideal.Icarr[OF _ A(2)] A(3)] A(1,4) by simp
     moreover have "I +> i = I"
@@ -243,9 +245,9 @@
       by (simp add: A(1-2) abelian_subgroup.a_rcos_const)
     moreover have "I +> j \<in> carrier (R Quot I)" and "I = \<zero>\<^bsub>R Quot I\<^esub>" and "I +> \<one> = \<one>\<^bsub>R Quot I\<^esub>"
       by (auto simp add: FactRing_def A_RCOSETS_def' A(3))
-    ultimately have "I +> j = \<one>\<^bsub>R Quot I\<^esub>"
+    ultimately show ?thesis
       using ring.ring_simprules(8)[OF ideal.quotient_is_ring[OF A(1)]] by simp
-  } note aux_lemma2 = this
+  qed
 
   interpret I: ring "R Quot I" + J: ring "R Quot J"
     using assms(1-2)[THEN ideal.quotient_is_ring] by auto
@@ -418,33 +420,33 @@
   case 0 show ?case
     by (auto simp add: RDirProd_list_carrier FactRing_def A_RCOSETS_def')
 next
-  { fix S :: "'c ring" and T :: "'d ring" and f g
-    assume A: "ring T" "f \<in> ring_hom R S" "g \<in> ring_hom R T" "f ` carrier R \<subseteq> f ` (a_kernel R T g)"
-    have "(\<lambda>a. (f a, g a)) ` carrier R = (f ` carrier R) \<times> (g ` carrier R)"
+  have aux_lemma: "(\<lambda>a. (f a, g a)) ` carrier R = (f ` carrier R) \<times> (g ` carrier R)"
+    if A: "ring T" "f \<in> ring_hom R S" "g \<in> ring_hom R T" "f ` carrier R \<subseteq> f ` (a_kernel R T g)"
+    for S :: "'c ring" and T :: "'d ring" and f g
+  proof
+    show "(\<lambda>a. (f a, g a)) ` carrier R \<subseteq> (f ` carrier R) \<times> (g ` carrier R)"
+      by blast
+  next
+    show "(f ` carrier R) \<times> (g ` carrier R) \<subseteq> (\<lambda>a. (f a, g a)) ` carrier R"
     proof
-      show "(\<lambda>a. (f a, g a)) ` carrier R \<subseteq> (f ` carrier R) \<times> (g ` carrier R)"
+      fix t assume "t \<in> (f ` carrier R) \<times> (g ` carrier R)"
+      then obtain a b where a: "a \<in> carrier R" "f a = fst t" and b: "b \<in> carrier R" "g b = snd t"
+        by auto
+      obtain c where c: "c \<in> a_kernel R T g" "f c = f (a \<ominus> b)"
+        using A(4) minus_closed[OF a(1) b (1)] by auto
+      have "f (c \<oplus> b) = f (a \<ominus> b) \<oplus>\<^bsub>S\<^esub>  f b"
+        using ring_hom_memE(3)[OF A(2)] b c unfolding a_kernel_def' by auto
+      hence "f (c \<oplus> b) = f a"
+        using ring_hom_memE(3)[OF A(2) minus_closed[of a b], of b] a b by algebra
+      moreover have "g (c \<oplus> b) = g b"
+        using ring_hom_memE(1,3)[OF A(3)] b(1) c ring.ring_simprules(8)[OF A(1)]
+        unfolding a_kernel_def' by auto
+      ultimately have "(\<lambda>a. (f a, g a)) (c \<oplus> b) = t" and "c \<oplus> b \<in> carrier R"
+        using a b c unfolding a_kernel_def' by auto
+      thus "t \<in> (\<lambda>a. (f a, g a)) ` carrier R"
         by blast
-    next
-      show "(f ` carrier R) \<times> (g ` carrier R) \<subseteq> (\<lambda>a. (f a, g a)) ` carrier R"
-      proof
-        fix t assume "t \<in> (f ` carrier R) \<times> (g ` carrier R)"
-        then obtain a b where a: "a \<in> carrier R" "f a = fst t" and b: "b \<in> carrier R" "g b = snd t"
-          by auto
-        obtain c where c: "c \<in> a_kernel R T g" "f c = f (a \<ominus> b)"
-          using A(4) minus_closed[OF a(1) b (1)] by auto
-        have "f (c \<oplus> b) = f (a \<ominus> b) \<oplus>\<^bsub>S\<^esub>  f b"
-          using ring_hom_memE(3)[OF A(2)] b c unfolding a_kernel_def' by auto
-        hence "f (c \<oplus> b) = f a"
-          using ring_hom_memE(3)[OF A(2) minus_closed[of a b], of b] a b by algebra
-        moreover have "g (c \<oplus> b) = g b"
-          using ring_hom_memE(1,3)[OF A(3)] b(1) c ring.ring_simprules(8)[OF A(1)]
-          unfolding a_kernel_def' by auto
-        ultimately have "(\<lambda>a. (f a, g a)) (c \<oplus> b) = t" and "c \<oplus> b \<in> carrier R"
-          using a b c unfolding a_kernel_def' by auto
-        thus "t \<in> (\<lambda>a. (f a, g a)) ` carrier R"
-          by blast
-      qed
-    qed } note aux_lemma = this
+    qed
+  qed
 
   let ?map_Quot = "\<lambda>I n. map (\<lambda>i. R Quot (I i)) [0..< Suc n]"
   let ?DirProd = "\<lambda>I n. RDirProd_list (?map_Quot I n)"
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Coset.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -1914,9 +1914,10 @@
     interpret Anormal: normal A "(G Mod H)" using assms by simp
     show "{x \<in> carrier G. H #> x \<in> A} #> x = x <# {x \<in> carrier G. H #> x \<in> A}" if x: "x \<in> carrier G" for x
     proof -
-      { fix y
-        assume y: "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
-        then obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x' \<otimes> x" 
+      have "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
+        if y: "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x" for y
+      proof -
+        from that obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x' \<otimes> x" 
           unfolding r_coset_def by auto
         from x(1) have Hx: "H #> x \<in> carrier (G Mod H)" 
           unfolding FactGroup_def RCOSETS_def by force
@@ -1937,11 +1938,12 @@
         also have "\<dots> = y"
           by (simp add: x x')
         finally have "x \<otimes> (inv x \<otimes> x' \<otimes> x) = y" .
-        with xcoset have "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}" by auto}
-      moreover
-      { fix y
-        assume y: "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
-        then obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x \<otimes> x'" unfolding l_coset_def by auto
+        with xcoset show ?thesis by auto
+      qed
+      moreover have "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
+        if y: "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}" for y
+      proof -
+        from that obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x \<otimes> x'" unfolding l_coset_def by auto
         from x(1) have invx: "inv x \<in> carrier G" 
           by (rule inv_closed)
         hence Hinvx: "H #> (inv x) \<in> carrier (G Mod H)" 
@@ -1960,7 +1962,8 @@
         also have "\<dots> = y"
           by (simp add: x x')
         finally have "x \<otimes> x' \<otimes> inv x \<otimes> x = y".
-        with xcoset have "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x" by auto }
+        with xcoset show ?thesis by auto
+      qed
       ultimately show ?thesis
         by auto
     qed
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Embedded_Algebras.thy
--- a/src/HOL/Algebra/Embedded_Algebras.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Embedded_Algebras.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -1123,14 +1123,14 @@
   assumes "dimension n K E" and "dimension m K E"
   shows "n = m"
 proof -
-  { fix n m assume n: "dimension n K E" and m: "dimension m K E"
-    then obtain Vs
+  have aux_lemma: "n \<le> m" if n: "dimension n K E" and m: "dimension m K E" for n m
+  proof -
+    from that obtain Vs
       where Vs: "set Vs \<subseteq> carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E"
       using exists_base by meson
-    hence "n \<le> m"
+    then show ?thesis
       using independent_length_le_dimension[OF m Vs(2)] Span_base_incl[OF Vs(1)] by auto
-  } note aux_lemma = this
-
+  qed
   show ?thesis
     using aux_lemma[OF assms] aux_lemma[OF assms(2,1)] by simp
 qed
@@ -1166,28 +1166,28 @@
   assumes "dimension n K E" and "independent K Us" "set Us \<subseteq> E"
   shows "\<exists>Vs. length (Vs @ Us) = n \<and> independent K (Vs @ Us) \<and> Span K (Vs @ Us) = E"
 proof -
-  { fix Us k assume "k \<le> n" "independent K Us" "set Us \<subseteq> E" "length Us = k"
-    hence "\<exists>Vs. length (Vs @ Us) = n \<and> independent K (Vs @ Us) \<and> Span K (Vs @ Us) = E"
-    proof (induct arbitrary: Us rule: inc_induct)
-      case base thus ?case
-        using independent_length_eq_dimension[OF assms(1) base(1-2)] by auto
-    next
-      case (step m)
-      have "Span K Us \<subseteq> E"
-        using mono_Span_subset step(4-6) exists_base[OF assms(1)] by blast
-      hence "Span K Us \<subset> E"
-        using independent_length_eq_dimension[OF assms(1) step(4-5)] step(2,6) assms(1) by blast
-      then obtain v where v: "v \<in> E" "v \<notin> Span K Us"
-        using Span_strict_incl exists_base[OF assms(1)] by blast
-      hence "independent K (v # Us)"
-        using space_subgroup_props(1)[OF assms(1)] li_Cons[OF _ v(2) step(4)] by auto
-      then obtain Vs
-        where "length (Vs @ (v # Us)) = n" "independent K (Vs @ (v # Us))" "Span K (Vs @ (v # Us)) = E"
-        using step(3)[of "v # Us"] step(1-2,4-6) v by auto
-      thus ?case
-        by (metis append.assoc append_Cons append_Nil)
-    qed } note aux_lemma = this
-
+  have aux_lemma: "\<exists>Vs. length (Vs @ Us) = n \<and> independent K (Vs @ Us) \<and> Span K (Vs @ Us) = E"
+    if "k \<le> n" "independent K Us" "set Us \<subseteq> E" "length Us = k" for Us k
+    using that
+  proof (induct arbitrary: Us rule: inc_induct)
+    case base
+    thus ?case using independent_length_eq_dimension[OF assms(1) base(1-2)] by auto
+  next
+    case (step m)
+    have "Span K Us \<subseteq> E"
+      using mono_Span_subset step(4-6) exists_base[OF assms(1)] by blast
+    hence "Span K Us \<subset> E"
+      using independent_length_eq_dimension[OF assms(1) step(4-5)] step(2,6) assms(1) by blast
+    then obtain v where v: "v \<in> E" "v \<notin> Span K Us"
+      using Span_strict_incl exists_base[OF assms(1)] by blast
+    hence "independent K (v # Us)"
+      using space_subgroup_props(1)[OF assms(1)] li_Cons[OF _ v(2) step(4)] by auto
+    then obtain Vs
+      where "length (Vs @ (v # Us)) = n" "independent K (Vs @ (v # Us))" "Span K (Vs @ (v # Us)) = E"
+      using step(3)[of "v # Us"] step(1-2,4-6) v by auto
+    thus ?case
+      by (metis append.assoc append_Cons append_Nil)
+  qed
   have "length Us \<le> n"
     using independent_length_le_dimension[OF assms] .
   thus ?thesis
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Exact_Sequence.thy
--- a/src/HOL/Algebra/Exact_Sequence.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Exact_Sequence.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -38,24 +38,23 @@
   assumes "exact_seq (G, F)" and "(i :: nat) < length F"
   shows "exact_seq (drop i G, drop i F)"
 proof-
-  { fix t i assume "exact_seq t" "i < length (snd t)"
-    hence "exact_seq (drop i (fst t), drop i (snd t))"
-    proof (induction arbitrary: i)
-      case (unity G1 G2 f) thus ?case
-        by (simp add: exact_seq.unity)
+  have "exact_seq (drop i (fst t), drop i (snd t))" if "exact_seq t" "i < length (snd t)" for t i
+    using that
+  proof (induction arbitrary: i)
+    case (unity G1 G2 f) thus ?case
+      by (simp add: exact_seq.unity)
+  next
+    case (extension G K l g q H h) show ?case
+    proof (cases)
+      assume "i = 0" thus ?case
+        using exact_seq.extension[OF extension.hyps] by simp
     next
-      case (extension G K l g q H h) show ?case
-      proof (cases)
-        assume "i = 0" thus ?case
-          using exact_seq.extension[OF extension.hyps] by simp
-      next
-        assume "i \<noteq> 0" hence "i \<ge> Suc 0" by simp
-        then obtain k where "k < length (snd (G # K # l, g # q))" "i = Suc k"
-          using Suc_le_D extension.prems by auto
-        thus ?thesis using extension.IH by simp 
-      qed
-    qed }
-
+      assume "i \<noteq> 0" hence "i \<ge> Suc 0" by simp
+      then obtain k where "k < length (snd (G # K # l, g # q))" "i = Suc k"
+        using Suc_le_D extension.prems by auto
+      thus ?thesis using extension.IH by simp 
+    qed
+  qed
   thus ?thesis using assms by auto
 qed
 
@@ -68,18 +67,19 @@
 lemma exact_seq_imp_exact_hom:
    assumes "exact_seq (G1 # l,q) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
    shows "g1 ` (carrier G1) = kernel G2 G3 g2"
-proof-
-  { fix t assume "exact_seq t" and "length (fst t) \<ge> 3 \<and> length (snd t) \<ge> 2"
-    hence "(hd (tl (snd t))) ` (carrier (hd (tl (tl (fst t))))) =
+proof -
+  have "(hd (tl (snd t))) ` (carrier (hd (tl (tl (fst t))))) =
             kernel (hd (tl (fst t))) (hd (fst t)) (hd (snd t))"
-    proof (induction)
-      case (unity G1 G2 f)
-      then show ?case by auto
-    next
-      case (extension G l g q H h)
-      then show ?case by auto
-    qed }
-  thus ?thesis using assms by fastforce
+    if "exact_seq t" and "length (fst t) \<ge> 3 \<and> length (snd t) \<ge> 2" for t
+    using that
+  proof (induction)
+    case (unity G1 G2 f)
+    then show ?case by auto
+  next
+    case (extension G l g q H h)
+    then show ?case by auto
+  qed
+  with assms show ?thesis by fastforce
 qed
 
 lemma exact_seq_imp_exact_hom_arbitrary:
@@ -103,16 +103,15 @@
   assumes "exact_seq ((G # l, q)) \<longlongrightarrow>\<^bsub>g\<^esub> H"
   shows "group_hom G H g"
 proof-
-  { fix t assume "exact_seq t"
-    hence "group_hom (hd (tl (fst t))) (hd (fst t)) (hd(snd t))"
-    proof (induction)
-      case (unity G1 G2 f)
-      then show ?case by auto
-    next
-      case (extension G l g q H h)
-      then show ?case unfolding group_hom_def group_hom_axioms_def by auto
-    qed }
-  note aux_lemma = this
+  have aux_lemma: "group_hom (hd (tl (fst t))) (hd (fst t)) (hd(snd t))" if "exact_seq t" for t
+    using that
+  proof (induction)
+    case (unity G1 G2 f)
+    then show ?case by auto
+  next
+    case (extension G l g q H h)
+    then show ?case unfolding group_hom_def group_hom_axioms_def by auto
+  qed
   show ?thesis using aux_lemma[OF assms]
     by simp
 qed
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -115,8 +115,7 @@
       then show ?thesis
         using \<open>(A,y) \<in> foldSetD D (\<cdot>) e\<close> by auto
     next
-      case (2 x' A' y')
-      note A' = this
+      case A': (2 x' A' y')
       show ?thesis
         using foldSetD.cases [OF \<open>(A,y) \<in> foldSetD D (\<cdot>) e\<close>]
       proof cases
@@ -124,8 +123,7 @@
         then show ?thesis
           using \<open>(A,x) \<in> foldSetD D (\<cdot>) e\<close> by auto
       next
-        case (2 x'' A'' y'')
-        note A'' = this
+        case A'': (2 x'' A'' y'')
         show ?thesis
         proof (cases "x' = x''")
           case True
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Generated_Fields.thy
--- a/src/HOL/Algebra/Generated_Fields.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Generated_Fields.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -121,56 +121,56 @@
     and "I \<subseteq> K"
   shows "generate_field (R\<lparr>carrier := K\<rparr>) I \<subseteq> generate_field (R\<lparr>carrier := H\<rparr>) I"
 proof
-  {fix J assume J_def : "subfield J R" "I \<subseteq> J"
-    have "generate_field (R \<lparr> carrier := J \<rparr>) I \<subseteq> J"
-      using field.mono_generate_field[of "(R\<lparr>carrier := J\<rparr>)" I J] subfield_iff(2)[OF J_def(1)]
-          field.generate_field_in_carrier[of "R\<lparr>carrier := J\<rparr>"]  field_axioms J_def
-      by auto}
-  note incl_HK = this
-  {fix x have "x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I" 
-    proof (induction  rule : generate_field.induct)
-      case one
-        have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub>" by simp
-        moreover have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub>" by simp
-        ultimately show ?case using assms generate_field.one by metis
-    next
-      case (incl h) thus ?case using generate_field.incl by force
-    next
-      case (a_inv h)
-      note hyp = this
-      have "a_inv (R\<lparr>carrier := K\<rparr>) h = a_inv R h" 
-        using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] hyp
-               subring.axioms(1)[OF subfieldE(1)[OF assms(2)]]
-        unfolding comm_group_def a_inv_def by auto
-      moreover have "a_inv (R\<lparr>carrier := H\<rparr>) h = a_inv R h"
-        using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] hyp
-               subring.axioms(1)[OF subfieldE(1)[OF assms(1)]]
-        unfolding  comm_group_def a_inv_def by auto
-      ultimately show ?case using generate_field.a_inv a_inv.IH by fastforce
-    next
-      case (m_inv h) 
-      note hyp = this
-      have h_K : "h \<in> (K - {\<zero>})" using incl_HK[OF assms(2) assms(4)] hyp by auto
-      hence "m_inv (R\<lparr>carrier := K\<rparr>) h = m_inv R h" 
-        using  field.m_inv_mult_of[OF subfield_iff(2)[OF assms(2)]]
-               group.m_inv_consistent[of "mult_of R" "K - {\<zero>}"] field_mult_group units_of_inv
-               subgroup_mult_of subfieldE[OF assms(2)] unfolding mult_of_def apply simp
-        by (metis h_K mult_of_def mult_of_is_Units subgroup.mem_carrier units_of_carrier assms(2))
-      moreover have h_H : "h \<in> (H - {\<zero>})" using incl_HK[OF assms(1) assms(3)] hyp by auto
-      hence "m_inv (R\<lparr>carrier := H\<rparr>) h = m_inv R h"
-        using  field.m_inv_mult_of[OF subfield_iff(2)[OF assms(1)]]
-               group.m_inv_consistent[of "mult_of R" "H - {\<zero>}"] field_mult_group 
-               subgroup_mult_of[OF assms(1)]  unfolding mult_of_def apply simp
-        by (metis h_H field_Units m_inv_mult_of mult_of_is_Units subgroup.mem_carrier units_of_def)
-      ultimately show ?case using generate_field.m_inv m_inv.IH h_H by fastforce
-    next
-      case (eng_add h1 h2)
-      thus ?case using incl_HK assms generate_field.eng_add by force
-    next
-      case (eng_mult h1 h2)
-      thus ?case using generate_field.eng_mult by force
-    qed}
-  thus "\<And>x. x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I"
+  have incl_HK: "generate_field (R \<lparr> carrier := J \<rparr>) I \<subseteq> J"
+    if J_def : "subfield J R" "I \<subseteq> J" for J
+    using field.mono_generate_field[of "(R\<lparr>carrier := J\<rparr>)" I J] subfield_iff(2)[OF J_def(1)]
+      field.generate_field_in_carrier[of "R\<lparr>carrier := J\<rparr>"]  field_axioms J_def
+    by auto
+
+  fix x
+  have "x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I"
+  proof (induction  rule : generate_field.induct)
+    case one
+    have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub>" by simp
+    moreover have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub>" by simp
+    ultimately show ?case using assms generate_field.one by metis
+  next
+    case (incl h)
+    thus ?case using generate_field.incl by force
+  next
+    case (a_inv h)
+    have "a_inv (R\<lparr>carrier := K\<rparr>) h = a_inv R h" 
+      using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] a_inv
+        subring.axioms(1)[OF subfieldE(1)[OF assms(2)]]
+      unfolding comm_group_def a_inv_def by auto
+    moreover have "a_inv (R\<lparr>carrier := H\<rparr>) h = a_inv R h"
+      using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] a_inv
+        subring.axioms(1)[OF subfieldE(1)[OF assms(1)]]
+      unfolding  comm_group_def a_inv_def by auto
+    ultimately show ?case using generate_field.a_inv a_inv.IH by fastforce
+  next
+    case (m_inv h) 
+    have h_K : "h \<in> (K - {\<zero>})" using incl_HK[OF assms(2) assms(4)] m_inv by auto
+    hence "m_inv (R\<lparr>carrier := K\<rparr>) h = m_inv R h" 
+      using  field.m_inv_mult_of[OF subfield_iff(2)[OF assms(2)]]
+        group.m_inv_consistent[of "mult_of R" "K - {\<zero>}"] field_mult_group units_of_inv
+        subgroup_mult_of subfieldE[OF assms(2)] unfolding mult_of_def apply simp
+      by (metis h_K mult_of_def mult_of_is_Units subgroup.mem_carrier units_of_carrier assms(2))
+    moreover have h_H : "h \<in> (H - {\<zero>})" using incl_HK[OF assms(1) assms(3)] m_inv by auto
+    hence "m_inv (R\<lparr>carrier := H\<rparr>) h = m_inv R h"
+      using  field.m_inv_mult_of[OF subfield_iff(2)[OF assms(1)]]
+        group.m_inv_consistent[of "mult_of R" "H - {\<zero>}"] field_mult_group 
+        subgroup_mult_of[OF assms(1)]  unfolding mult_of_def apply simp
+      by (metis h_H field_Units m_inv_mult_of mult_of_is_Units subgroup.mem_carrier units_of_def)
+    ultimately show ?case using generate_field.m_inv m_inv.IH h_H by fastforce
+  next
+    case (eng_add h1 h2)
+    thus ?case using incl_HK assms generate_field.eng_add by force
+  next
+    case (eng_mult h1 h2)
+    thus ?case using generate_field.eng_mult by force
+  qed
+  thus "x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I"
     by auto
 qed
 
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Generated_Groups.thy
--- a/src/HOL/Algebra/Generated_Groups.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Generated_Groups.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -344,23 +344,23 @@
     by (simp add: DG.rcos_sum)
   also have " ... = derived G (carrier G) #> (g2 \<otimes> g1)"
   proof -
-    { fix g1 g2 assume g1: "g1 \<in> carrier G" and g2: "g2 \<in> carrier G"
-      have "derived G (carrier G) #> (g1 \<otimes> g2) \<subseteq> derived G (carrier G) #> (g2 \<otimes> g1)"
-      proof
-        fix h assume "h \<in> derived G (carrier G) #> (g1 \<otimes> g2)"
-        then obtain g' where h: "g' \<in> carrier G" "g' \<in> derived G (carrier G)" "h = g' \<otimes> (g1 \<otimes> g2)"
-          using DG.subset unfolding r_coset_def by auto
-        hence "h = g' \<otimes> (g1 \<otimes> g2) \<otimes> (inv g1 \<otimes> inv g2 \<otimes> g2 \<otimes> g1)"
-          using g1 g2 by (simp add: m_assoc)
-        hence "h = (g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2)) \<otimes> (g2 \<otimes> g1)"
-          using h(1) g1 g2 inv_closed m_assoc m_closed by presburger
-        moreover have "g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2 \<in> derived G (carrier G)"
-          using incl[of _ "derived_set G (carrier G)"] g1 g2 unfolding derived_def by blast
-        hence "g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2) \<in> derived G (carrier G)"
-          using DG.m_closed[OF h(2)] by simp
-        ultimately show "h \<in> derived G (carrier G) #> (g2 \<otimes> g1)"
-          unfolding r_coset_def by blast
-      qed }
+    have "derived G (carrier G) #> (g1 \<otimes> g2) \<subseteq> derived G (carrier G) #> (g2 \<otimes> g1)"
+      if g1: "g1 \<in> carrier G" and g2: "g2 \<in> carrier G" for g1 g2
+    proof
+      fix h assume "h \<in> derived G (carrier G) #> (g1 \<otimes> g2)"
+      then obtain g' where h: "g' \<in> carrier G" "g' \<in> derived G (carrier G)" "h = g' \<otimes> (g1 \<otimes> g2)"
+        using DG.subset unfolding r_coset_def by auto
+      hence "h = g' \<otimes> (g1 \<otimes> g2) \<otimes> (inv g1 \<otimes> inv g2 \<otimes> g2 \<otimes> g1)"
+        using g1 g2 by (simp add: m_assoc)
+      hence "h = (g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2)) \<otimes> (g2 \<otimes> g1)"
+        using h(1) g1 g2 inv_closed m_assoc m_closed by presburger
+      moreover have "g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2 \<in> derived G (carrier G)"
+        using incl[of _ "derived_set G (carrier G)"] g1 g2 unfolding derived_def by blast
+      hence "g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2) \<in> derived G (carrier G)"
+        using DG.m_closed[OF h(2)] by simp
+      ultimately show "h \<in> derived G (carrier G) #> (g2 \<otimes> g1)"
+        unfolding r_coset_def by blast
+    qed
     thus ?thesis
       using g1(1) g2(1) by auto
   qed
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Generated_Rings.thy
--- a/src/HOL/Algebra/Generated_Rings.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Generated_Rings.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -109,38 +109,37 @@
     and "I \<subseteq> K"
   shows "generate_ring (R\<lparr>carrier := K\<rparr>) I \<subseteq> generate_ring (R\<lparr>carrier := H\<rparr>) I"
 proof
-  {fix J assume J_def : "subring J R" "I \<subseteq> J"
-    have "generate_ring (R \<lparr> carrier := J \<rparr>) I \<subseteq> J"
-      using ring.mono_generate_ring[of "(R\<lparr>carrier := J\<rparr>)" I J ] subring_is_ring[OF J_def(1)]
-          ring.generate_ring_in_carrier[of "R\<lparr>carrier := J\<rparr>"]  ring_axioms J_def(2)
-      by auto}
-  note incl_HK = this
-  {fix x have "x \<in> generate_ring (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_ring (R\<lparr>carrier := H\<rparr>) I" 
-    proof (induction  rule : generate_ring.induct)
-      case one
-        have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub>" by simp
-        moreover have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub>" by simp
-        ultimately show ?case using assms generate_ring.one by metis
-    next
-      case (incl h) thus ?case using generate_ring.incl by force
-    next
-      case (a_inv h)
-      note hyp = this
-      have "a_inv (R\<lparr>carrier := K\<rparr>) h = a_inv R h" 
-        using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] hyp
-        unfolding subring_def comm_group_def a_inv_def by auto
-      moreover have "a_inv (R\<lparr>carrier := H\<rparr>) h = a_inv R h"
-        using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] hyp
-        unfolding subring_def comm_group_def a_inv_def by auto
-      ultimately show ?case using generate_ring.a_inv a_inv.IH by fastforce
-    next
-      case (eng_add h1 h2)
-      thus ?case using incl_HK assms generate_ring.eng_add by force
-    next
-      case (eng_mult h1 h2)
-      thus ?case using generate_ring.eng_mult by force
-    qed}
-  thus "\<And>x. x \<in> generate_ring (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_ring (R\<lparr>carrier := H\<rparr>) I"
+  have incl_HK: "generate_ring (R \<lparr> carrier := J \<rparr>) I \<subseteq> J" if J_def : "subring J R" "I \<subseteq> J" for J
+    using ring.mono_generate_ring[of "(R\<lparr>carrier := J\<rparr>)" I J ] subring_is_ring[OF J_def(1)]
+      ring.generate_ring_in_carrier[of "R\<lparr>carrier := J\<rparr>"]  ring_axioms J_def(2)
+    by auto
+
+  fix x
+  have "x \<in> generate_ring (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_ring (R\<lparr>carrier := H\<rparr>) I" 
+  proof (induction  rule : generate_ring.induct)
+    case one
+    have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub>" by simp
+    moreover have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub>" by simp
+    ultimately show ?case using assms generate_ring.one by metis
+  next
+    case (incl h) thus ?case using generate_ring.incl by force
+  next
+    case (a_inv h)
+    have "a_inv (R\<lparr>carrier := K\<rparr>) h = a_inv R h" 
+      using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] a_inv
+      unfolding subring_def comm_group_def a_inv_def by auto
+    moreover have "a_inv (R\<lparr>carrier := H\<rparr>) h = a_inv R h"
+      using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] a_inv
+      unfolding subring_def comm_group_def a_inv_def by auto
+    ultimately show ?case using generate_ring.a_inv a_inv.IH by fastforce
+  next
+    case (eng_add h1 h2)
+    thus ?case using incl_HK assms generate_ring.eng_add by force
+  next
+    case (eng_mult h1 h2)
+    thus ?case using generate_ring.eng_mult by force
+  qed
+  thus "x \<in> generate_ring (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_ring (R\<lparr>carrier := H\<rparr>) I"
     by auto
 qed
 
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -102,8 +102,8 @@
 lemma (in ring) set_add_comm:
   assumes "I \<subseteq> carrier R" "J \<subseteq> carrier R" shows "I <+> J = J <+> I"
 proof -
-  { fix I J assume "I \<subseteq> carrier R" "J \<subseteq> carrier R" hence "I <+> J \<subseteq> J <+> I"
-      using a_comm unfolding set_add_def' by (auto, blast) }
+  have "I <+> J \<subseteq> J <+> I" if "I \<subseteq> carrier R" "J \<subseteq> carrier R" for I J
+    using that a_comm unfolding set_add_def' by (auto, blast)
   thus ?thesis
     using assms by auto
 qed
@@ -262,35 +262,33 @@
   assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R" and notempty: "S \<noteq> {}"
   shows "ideal (\<Inter>S) R"
 proof -
-  { fix x y J
-    assume "\<forall>I\<in>S. x \<in> I" "\<forall>I\<in>S. y \<in> I" and JS: "J \<in> S"
+  have "x \<oplus> y \<in> J" if "\<forall>I\<in>S. x \<in> I" "\<forall>I\<in>S. y \<in> I" and JS: "J \<in> S" for x y J
+  proof -
     interpret ideal J R by (rule Sideals[OF JS])
-    have "x \<oplus> y \<in> J"
-      by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close> \<open>\<forall>I\<in>S. y \<in> I\<close>) }
-  moreover
-    have "\<zero> \<in> J" if "J \<in> S" for J
-      by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1)) 
-  moreover
-  { fix x J
-    assume "\<forall>I\<in>S. x \<in> I" and JS: "J \<in> S"
+    show ?thesis by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close> \<open>\<forall>I\<in>S. y \<in> I\<close>)
+  qed
+  moreover have "\<zero> \<in> J" if "J \<in> S" for J
+    by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1)) 
+  moreover have "\<ominus> x \<in> J" if "\<forall>I\<in>S. x \<in> I" and JS: "J \<in> S" for x J
+  proof -
     interpret ideal J R by (rule Sideals[OF JS])
-    have "\<ominus> x \<in> J"
-      by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close>) }
-  moreover
-  { fix x y J
-    assume "\<forall>I\<in>S. x \<in> I" and ycarr: "y \<in> carrier R" and JS: "J \<in> S"
+    show ?thesis by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close>)
+  qed
+  moreover have "y \<otimes> x \<in> J" "x \<otimes> y \<in> J"
+    if "\<forall>I\<in>S. x \<in> I" and ycarr: "y \<in> carrier R" and JS: "J \<in> S" for x y J
+  proof -
     interpret ideal J R by (rule Sideals[OF JS])
-    have "y \<otimes> x \<in> J" "x \<otimes> y \<in> J" 
-      using I_l_closed I_r_closed JS \<open>\<forall>I\<in>S. x \<in> I\<close> ycarr by blast+ }
-  moreover
-  { fix x
-    assume "\<forall>I\<in>S. x \<in> I"
+    show "y \<otimes> x \<in> J" "x \<otimes> y \<in> J" using I_l_closed I_r_closed JS \<open>\<forall>I\<in>S. x \<in> I\<close> ycarr by blast+
+  qed
+  moreover have "x \<in> carrier R" if "\<forall>I\<in>S. x \<in> I" for x
+    proof -
     obtain I0 where I0S: "I0 \<in> S"
       using notempty by blast
     interpret ideal I0 R by (rule Sideals[OF I0S])
     have "x \<in> I0"
       by (simp add: I0S \<open>\<forall>I\<in>S. x \<in> I\<close>) 
-    with a_subset have "x \<in> carrier R" by fast }
+    with a_subset show ?thesis by fast
+  qed
   ultimately show ?thesis
     by unfold_locales (auto simp: Inter_eq simp flip: a_inv_def)
 qed
@@ -308,17 +306,14 @@
     by (rule ring_axioms)
   show "ideal_axioms (I <+> J) R"
   proof -
-    { fix x i j
-      assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J"
-      from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
-      have "\<exists>h\<in>I. \<exists>k\<in>J. (i \<oplus> j) \<otimes> x = h \<oplus> k"
-        by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI) }
-    moreover
-    { fix x i j
-      assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J"
-      from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
-      have "\<exists>h\<in>I. \<exists>k\<in>J. x \<otimes> (i \<oplus> j) = h \<oplus> k"
-        by (meson iI ideal.I_l_closed idealJ jJ local.idealI r_distr) }
+    have "\<exists>h\<in>I. \<exists>k\<in>J. (i \<oplus> j) \<otimes> x = h \<oplus> k"
+      if xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" for x i j
+      using xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
+      by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI)
+    moreover have "\<exists>h\<in>I. \<exists>k\<in>J. x \<otimes> (i \<oplus> j) = h \<oplus> k"
+      if xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" for x i j
+      using xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
+        by (meson iI ideal.I_l_closed idealJ jJ local.idealI r_distr)
     ultimately show "ideal_axioms (I <+> J) R"
       by (intro ideal_axioms.intro) (auto simp: set_add_defs)
   qed
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Ideal_Product.thy
--- a/src/HOL/Algebra/Ideal_Product.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Ideal_Product.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -273,26 +273,25 @@
                       local.ring_axioms ring.ideal_prod_is_ideal) 
     qed
   qed
-next
-  { fix s J K assume A: "ideal J R" "ideal K R" "s \<in> I \<cdot> J"
-    have "s \<in> I \<cdot> (J <+> K) \<and> s \<in> I \<cdot> (K <+> J)"
-    proof -
-      from \<open>s \<in> I \<cdot> J\<close> have "s \<in> I \<cdot> (J <+> K)"
-      proof (induct s rule: ideal_prod.induct)
-        case (prod i j)
-        hence "(j \<oplus> \<zero>) \<in> J <+> K"
-          using set_add_def'[of R J K]
-                additive_subgroup.zero_closed[OF ideal.axioms(1), of K R] A(2) by auto
-        thus ?case
-          by (metis A(1) additive_subgroup.a_Hcarr ideal.axioms(1) ideal_prod.prod prod r_zero)  
-      next
-        case (sum s1 s2) thus ?case
-          by (simp add: ideal_prod.sum) 
-      qed
-      thus ?thesis
-        by (metis A(1) A(2) ideal_def ring.union_genideal sup_commute) 
-    qed } note aux_lemma = this
 
+  have aux_lemma: "s \<in> I \<cdot> (J <+> K) \<and> s \<in> I \<cdot> (K <+> J)"
+    if A: "ideal J R" "ideal K R" "s \<in> I \<cdot> J" for s J K
+  proof -
+    from \<open>s \<in> I \<cdot> J\<close> have "s \<in> I \<cdot> (J <+> K)"
+    proof (induct s rule: ideal_prod.induct)
+      case (prod i j)
+      hence "(j \<oplus> \<zero>) \<in> J <+> K"
+        using set_add_def'[of R J K]
+          additive_subgroup.zero_closed[OF ideal.axioms(1), of K R] A(2) by auto
+      thus ?case
+        by (metis A(1) additive_subgroup.a_Hcarr ideal.axioms(1) ideal_prod.prod prod r_zero)  
+    next
+      case (sum s1 s2) thus ?case
+        by (simp add: ideal_prod.sum) 
+    qed
+    thus ?thesis
+      by (metis A(1) A(2) ideal_def ring.union_genideal sup_commute) 
+  qed
   show "I \<cdot> J <+> I \<cdot> K \<subseteq> I \<cdot> (J <+> K)"
   proof
     fix s assume "s \<in> I \<cdot> J <+> I \<cdot> K"
@@ -308,19 +307,22 @@
   assumes "ideal I R" "ideal J R"
   shows "I \<cdot> J = J \<cdot> I"
 proof -
-  { fix I J assume A: "ideal I R" "ideal J R"
-    have "I \<cdot> J \<subseteq> J \<cdot> I"
-    proof
-      fix s assume "s \<in> I \<cdot> J" thus "s \<in> J \<cdot> I"
-      proof (induct s rule: ideal_prod.induct)
-        case (prod i j) thus ?case
-          using m_comm[OF ideal.Icarr[OF A(1) prod(1)] ideal.Icarr[OF A(2) prod(2)]]
-          by (simp add: ideal_prod.prod)
-      next
-        case (sum s1 s2) thus ?case by (simp add: ideal_prod.sum) 
-      qed
-    qed }
-  thus ?thesis using assms by blast 
+  have "I \<cdot> J \<subseteq> J \<cdot> I" if A: "ideal I R" "ideal J R" for I J
+  proof
+    fix s
+    assume "s \<in> I \<cdot> J"
+    thus "s \<in> J \<cdot> I"
+    proof (induct s rule: ideal_prod.induct)
+      case (prod i j)
+      thus ?case
+        using m_comm[OF ideal.Icarr[OF A(1) prod(1)] ideal.Icarr[OF A(2) prod(2)]]
+        by (simp add: ideal_prod.prod)
+    next
+      case (sum s1 s2)
+      thus ?case by (simp add: ideal_prod.sum) 
+    qed
+  qed
+  with assms show ?thesis by blast 
 qed
 
 text \<open>The following result would also be true for locale ring\<close>
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Indexed_Polynomials.thy
--- a/src/HOL/Algebra/Indexed_Polynomials.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Indexed_Polynomials.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -285,23 +285,22 @@
   assumes "\<And>P. P \<in> carrier L \<Longrightarrow> carrier_coeff P" and "\<And>P. P \<in> carrier L \<Longrightarrow> index_free P i" and "\<zero>\<^bsub>L\<^esub> = indexed_const \<zero>"
   shows "inj_on (\<lambda>Ps. indexed_eval Ps i) (carrier (poly_ring L))"
 proof -
-  { fix Ps
-    assume "Ps \<in> carrier (poly_ring L)" and "indexed_eval Ps i = indexed_const \<zero>"
-    have "Ps = []"
-    proof (rule ccontr)
-      assume "Ps \<noteq> []"
-      then obtain P' Ps' where Ps: "Ps = P' # Ps'"
-        using list.exhaust by blast
-      with \<open>Ps \<in> carrier (poly_ring L)\<close>
-      have "P' \<noteq> indexed_const \<zero>" and "list_all carrier_coeff Ps" and "list_all (\<lambda>P. index_free P i) Ps"
-        using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def
-        by (simp add: list.pred_set subset_code(1))+
-      then obtain m where "(indexed_eval Ps i) m \<noteq> \<zero>"
-        using exists_indexed_eval_monomial'[of P' Ps'] unfolding Ps by auto
-      hence "indexed_eval Ps i \<noteq> indexed_const \<zero>"
-        unfolding indexed_const_def by auto
-      with \<open>indexed_eval Ps i = indexed_const \<zero>\<close> show False by simp
-    qed } note aux_lemma = this
+  have aux_lemma: "Ps = []"
+    if "Ps \<in> carrier (poly_ring L)" and "indexed_eval Ps i = indexed_const \<zero>" for Ps
+  proof (rule ccontr)
+    assume "\<not> ?thesis"
+    then obtain P' Ps' where Ps: "Ps = P' # Ps'"
+      using list.exhaust by blast
+    with \<open>Ps \<in> carrier (poly_ring L)\<close>
+    have "P' \<noteq> indexed_const \<zero>" and "list_all carrier_coeff Ps" and "list_all (\<lambda>P. index_free P i) Ps"
+      using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def
+      by (simp add: list.pred_set subset_code(1))+
+    then obtain m where "(indexed_eval Ps i) m \<noteq> \<zero>"
+      using exists_indexed_eval_monomial'[of P' Ps'] unfolding Ps by auto
+    hence "indexed_eval Ps i \<noteq> indexed_const \<zero>"
+      unfolding indexed_const_def by auto
+    with \<open>indexed_eval Ps i = indexed_const \<zero>\<close> show False by simp
+  qed
 
   show ?thesis
   proof (rule inj_onI)
@@ -356,9 +355,9 @@
 lemma (in ring) indexed_eval_index_free:
   assumes "list_all (\<lambda>P. index_free P j) Ps" and "i \<noteq> j" shows "index_free (indexed_eval Ps i) j"
 proof -
-  { fix Ps assume "list_all (\<lambda>P. index_free P j) Ps" hence "index_free (indexed_eval_aux Ps i) j"
-      using indexed_padd_index_free[OF indexed_pmult_index_free[OF _ assms(2)]]
-      by (induct Ps) (auto simp add: indexed_zero_def index_free_def) }
+  have "index_free (indexed_eval_aux Ps i) j" if "list_all (\<lambda>P. index_free P j) Ps" for Ps
+    using that indexed_padd_index_free[OF indexed_pmult_index_free[OF _ assms(2)]]
+    by (induct Ps) (auto simp add: indexed_zero_def index_free_def)
   thus ?thesis
     using assms(1) by auto
 qed
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -54,7 +54,7 @@
   show "carrier \<Z> = UNIV" by simp
 
   \<comment> \<open>Operations\<close>
-  { fix x y show "mult \<Z> x y = x * y" by simp }
+  show "mult \<Z> x y = x * y" for x y by simp
   show "one \<Z> = 1" by simp
   show "pow \<Z> x n = x^n" by (induct n) simp_all
 qed
@@ -67,11 +67,8 @@
   then interpret int: comm_monoid \<Z> .
 
   \<comment> \<open>Operations\<close>
-  { fix x y have "mult \<Z> x y = x * y" by simp }
-  note mult = this
-  have one: "one \<Z> = 1" by simp
   show "finprod \<Z> f A = prod f A"
-    by (induct A rule: infinite_finite_induct, auto)
+    by (induct A rule: infinite_finite_induct) auto
 qed
 
 interpretation int: abelian_monoid \<Z>
@@ -88,12 +85,10 @@
   show "carrier \<Z> = UNIV" by simp
 
   \<comment> \<open>Operations\<close>
-  { fix x y show "add \<Z> x y = x + y" by simp }
-  note add = this
-  show zero: "zero \<Z> = 0"
-    by simp
+  show "add \<Z> x y = x + y" for x y by simp
+  show zero: "zero \<Z> = 0" by simp
   show "finsum \<Z> f A = sum f A"
-    by (induct A rule: infinite_finite_induct, auto)
+    by (induct A rule: infinite_finite_induct) auto
 qed
 
 interpretation int: abelian_group \<Z>
@@ -118,17 +113,15 @@
   qed auto
   then interpret int: abelian_group \<Z> .
   \<comment> \<open>Operations\<close>
-  { fix x y have "add \<Z> x y = x + y" by simp }
-  note add = this
+  have add: "add \<Z> x y = x + y" for x y by simp
   have zero: "zero \<Z> = 0" by simp
-  {
-    fix x
+  show a_inv: "a_inv \<Z> x = - x" for x
+  proof -
     have "add \<Z> (- x) x = zero \<Z>"
       by (simp add: add zero)
-    then show "a_inv \<Z> x = - x"
+    then show ?thesis
       by (simp add: int.minus_equality)
-  }
-  note a_inv = this
+  qed
   show "a_minus \<Z> x y = x - y"
     by (simp add: int.minus_eq add a_inv)
 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -216,37 +216,43 @@
  assumes "n > 0"
  shows "(\<Sum>d | d dvd n. phi' d) = n"
 proof -
-  { fix d assume "d dvd n" then obtain q where q: "n = d * q" ..
-    have "card {a. 1 \<le> a \<and> a \<le> d \<and> coprime a d} = card {m \<in> {1 .. n}.  n div gcd m n = d}"
-         (is "card ?RF = card ?F")
-    proof (rule card_bij_eq)
-      { fix a b assume "a * n div d = b * n div d"
-        hence "a * (n div d) = b * (n div d)"
-          using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)
-        hence "a = b" using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>
-          by (simp add: mult.commute nat_mult_eq_cancel1)
-      } thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast
-      { fix a assume a: "a\<in>?RF"
-        hence "a * (n div d) \<ge> 1" using \<open>n>0\<close> dvd_div_ge_1[OF _ \<open>d dvd n\<close>] by simp
-        hence ge_1: "a * n div d \<ge> 1" by (simp add: \<open>d dvd n\<close> div_mult_swap)
-        have le_n: "a * n div d \<le> n" using div_mult_mono a by simp
-        have "gcd (a * n div d) n = n div d * gcd a d"
-          by (simp add: gcd_mult_distrib_nat q ac_simps)
-        hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
-        hence "a * n div d \<in> ?F"
-          using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)
-      } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
-      { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
-        hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
-        hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
-      } thus "inj_on (\<lambda>a. a div gcd a n) ?F" unfolding inj_on_def by blast
-      { fix m assume "m \<in> ?F"
-        hence "m div gcd m n \<in> ?RF" using dvd_div_ge_1
-          by (fastforce simp add: div_le_mono div_gcd_coprime)
-      } thus "(\<lambda>a. a div gcd a n) ` ?F \<subseteq> ?RF" by blast
-    qed force+
-  } hence phi'_eq: "\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"
-      unfolding phi'_def by presburger
+  have "card {a. 1 \<le> a \<and> a \<le> d \<and> coprime a d} = card {m \<in> {1 .. n}.  n div gcd m n = d}"
+    (is "card ?RF = card ?F")
+    if "d dvd n" for d
+  proof (rule card_bij_eq)
+    from that obtain q where q: "n = d * q" ..
+    have "a = b" if "a * n div d = b * n div d" for a b
+    proof -
+      from that have "a * (n div d) = b * (n div d)"
+        using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)
+      then show ?thesis using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>
+        by (simp add: mult.commute nat_mult_eq_cancel1)
+    qed
+    thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast
+    have "a * n div d \<in> ?F" if a: "a\<in>?RF" for a
+    proof -
+      from that have "a * (n div d) \<ge> 1" using \<open>n>0\<close> dvd_div_ge_1[OF _ \<open>d dvd n\<close>] by simp
+      hence ge_1: "a * n div d \<ge> 1" by (simp add: \<open>d dvd n\<close> div_mult_swap)
+      have le_n: "a * n div d \<le> n" using div_mult_mono a by simp
+      have "gcd (a * n div d) n = n div d * gcd a d"
+        by (simp add: gcd_mult_distrib_nat q ac_simps)
+      hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
+      then show ?thesis
+        using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)
+    qed
+    thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
+    have "m = l" if A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n" for m l
+    proof -
+      from that have "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
+      then show ?thesis using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
+    qed
+    thus "inj_on (\<lambda>a. a div gcd a n) ?F" unfolding inj_on_def by blast
+    have "m div gcd m n \<in> ?RF" if "m \<in> ?F" for m
+      using that dvd_div_ge_1  by (fastforce simp add: div_le_mono div_gcd_coprime)
+    thus "(\<lambda>a. a div gcd a n) ` ?F \<subseteq> ?RF" by blast
+  qed force+
+  hence phi'_eq: "\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"
+    unfolding phi'_def by presburger
   have fin: "finite {d. d dvd n}" using dvd_nat_bounds[OF \<open>n>0\<close>] by force
   have "(\<Sum>d | d dvd n. phi' d)
                  = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"
@@ -419,22 +425,23 @@
 proof (rule inj_onI, rule ccontr)
   fix x y :: nat
   assume A: "x \<in> {1 .. ord a}" "y \<in> {1 .. ord a}" "a [^] x = a [^] y" "x\<noteq>y"
-  { assume "x < ord a" "y < ord a"
-    hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce
-  }
-  moreover
-  { assume "x = ord a" "y < ord a"
+  then consider "x < ord a" "y < ord a" | "x = ord a" "y < ord a" | "y = ord a" "x < ord a"
+    by force
+  then show False
+  proof cases
+    case 1
+    then show ?thesis using ord_inj[OF assms] A unfolding inj_on_def by fastforce
+  next
+    case 2
     hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
     hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force
-    hence False using A by fastforce
-  }
-  moreover
-  { assume "y = ord a" "x < ord a"
+    with A show ?thesis by fastforce
+  next
+    case 3
     hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
     hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force
-    hence False using A by fastforce
-  }
-  ultimately show False using A  by force
+    with A show ?thesis by fastforce
+  qed
 qed
 
 lemma (in group) ord_ge_1: 
@@ -462,8 +469,9 @@
   shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
 proof
   show "?R \<subseteq> ?L" by blast
-  { fix y assume "y \<in> ?L"
-    then obtain x::nat where x: "y = a[^]x" by auto
+  have "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" if "y \<in> ?L" for y
+  proof -
+    from that obtain x::nat where x: "y = a[^]x" by auto
     define r q where "r = x mod ord a" and "q = x div ord a"
     then have "x = q * ord a + r"
       by (simp add: div_mult_mod_eq)
@@ -472,8 +480,8 @@
     hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
     have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
     hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
-    hence "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a[^]r\<close> by blast
-  }
+    thus ?thesis using \<open>y=a[^]r\<close> by blast
+  qed
   thus "?L \<subseteq> ?R" by auto
 qed
 
@@ -598,20 +606,21 @@
  assumes "a \<in> carrier G" "ord a \<noteq> 0"
  shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
 proof
- show "?R \<subseteq> ?L" by blast
- { fix y assume "y \<in> ?L"
-   then obtain x::nat where x: "y = a[^]x" by auto
-   define r q where "r = x mod ord a" and "q = x div ord a"
-   then have "x = q * ord a + r"
-     by (simp add: div_mult_mod_eq)
-   hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
-     using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
-   hence "y = a[^]r" using assms by simp
-   have "r < ord a" using assms by (simp add: r_def)
-   hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
-   hence "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a[^]r\<close> by blast
- }
- thus "?L \<subseteq> ?R" by auto
+  show "?R \<subseteq> ?L" by blast
+  have "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" if "y \<in> ?L" for y
+  proof -
+    from that obtain x::nat where x: "y = a[^]x" by auto
+    define r q where "r = x mod ord a" and "q = x div ord a"
+    then have "x = q * ord a + r"
+      by (simp add: div_mult_mod_eq)
+    hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
+      using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
+    hence "y = a[^]r" using assms by simp
+    have "r < ord a" using assms by (simp add: r_def)
+    hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
+    then show ?thesis using \<open>y=a[^]r\<close> by blast
+  qed
+  thus "?L \<subseteq> ?R" by auto
 qed
 
 lemma generate_pow_nat:
@@ -669,8 +678,7 @@
   then show ?thesis
     using \<open>ord a = 0\<close> by auto
 next
-  case False
-  note finite_subgroup = this
+  case finite_subgroup: False
   then have "generate G { a } = (([^]) a) ` {0..ord a - 1}"
     using generate_pow_nat ord_elems_inf_carrier a by auto
   hence "card (generate G {a}) = card {0..ord a - 1}"
@@ -952,12 +960,14 @@
   have set_eq2: "{x \<in> carrier (mult_of R) . group.ord (mult_of R) x = d}
                 = (\<lambda> n . a[^]n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" (is "?L = ?R")
   proof
-    { fix x assume x: "x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d"
-      hence "x \<in> {x \<in> carrier (mult_of R). x [^] d = \<one>}"
+    have "x \<in> ?R" if x: "x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d" for x
+    proof -
+      from that have "x \<in> {x \<in> carrier (mult_of R). x [^] d = \<one>}"
         by (simp add: G.pow_ord_eq_1[of x, symmetric])
       then obtain n where n: "x = a[^]n \<and> n \<in> {1 .. d}" using set_eq1 by blast
-      hence "x \<in> ?R" using x by fast
-    } thus "?L \<subseteq> ?R" by blast
+      then show ?thesis using x by fast
+    qed
+    thus "?L \<subseteq> ?R" by blast
     show "?R \<subseteq> ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)
   qed
   have "inj_on (\<lambda> n . a[^]n) {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}"
@@ -994,27 +1004,30 @@
     using fin finite by (subst card_UN_disjoint) auto
   also have "?U = carrier (mult_of R)"
   proof
-    { fix x assume x: "x \<in> carrier (mult_of R)"
-      hence x': "x\<in>carrier (mult_of R)" by simp
+    have "x \<in> ?U" if x: "x \<in> carrier (mult_of R)" for x
+    proof -
+      from that have x': "x\<in>carrier (mult_of R)" by simp
       then have "group.ord (mult_of R) x dvd order (mult_of R)"
         using G.ord_dvd_group_order by blast
-      hence "x \<in> ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
-    } thus "carrier (mult_of R) \<subseteq> ?U" by blast
+      then show ?thesis
+        using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
+    qed
+    thus "carrier (mult_of R) \<subseteq> ?U" by blast
   qed auto
   also have "card ... = order (mult_of R)"
     using order_mult_of finite' by (simp add: order_def)
   finally have sum_Ns_eq: "(\<Sum>d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .
 
-  { fix d assume d: "d dvd order (mult_of R)"
-    have "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<le> phi' d"
-    proof cases
-      assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger
-      next
-      assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<noteq> 0"
-      hence "\<exists>a \<in> carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
-      thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
-    qed
-  }
+  have "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<le> phi' d"
+    if d: "d dvd order (mult_of R)" for d
+  proof (cases "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = 0")
+    case True
+    thus ?thesis by presburger
+  next
+    case False
+    hence "\<exists>a \<in> carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
+    thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
+  qed
   hence all_le: "\<And>i. i \<in> {d. d dvd order (mult_of R) }
         \<Longrightarrow> (\<lambda>i. card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = i}) i \<le> (\<lambda>i. phi' i) i" by fast
   hence le: "(\<Sum>i | i dvd order (mult_of R). ?N i)
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Polynomial_Divisibility.thy
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -735,27 +735,25 @@
   assumes "subring K R" and "p \<in> carrier (K[X])" and "q \<in> carrier (K[X])"
   shows "p \<sim>\<^bsub>K[X]\<^esub> q \<Longrightarrow> length p = length q"
 proof -
-  { fix p q
-    assume p: "p \<in> carrier (K[X])" and q: "q \<in> carrier (K[X])" and "p \<sim>\<^bsub>K[X]\<^esub> q"
-    have "length p \<le> length q"
-    proof (cases "q = []")
-      case True with \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p = []"
-        unfolding associated_def True factor_def univ_poly_def by auto
-      thus ?thesis
-        using True by simp
-    next
-      case False
-      from \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p divides\<^bsub>K [X]\<^esub> q"
-        unfolding associated_def by simp
-      hence "p divides\<^bsub>poly_ring R\<^esub> q"
-        using carrier_polynomial[OF assms(1)]
-        unfolding factor_def univ_poly_carrier univ_poly_mult by auto
-      with \<open>q \<noteq> []\<close> have "degree p \<le> degree q"
-        using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp
-      with \<open>q \<noteq> []\<close> show ?thesis
-        by (cases "p = []", auto simp add: Suc_leI le_diff_iff)
-    qed
-  } note aux_lemma = this
+  have aux_lemma: "length p \<le> length q"
+    if p: "p \<in> carrier (K[X])" and q: "q \<in> carrier (K[X])" and "p \<sim>\<^bsub>K[X]\<^esub> q" for p q
+  proof (cases "q = []")
+    case True with \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p = []"
+      unfolding associated_def True factor_def univ_poly_def by auto
+    thus ?thesis
+      using True by simp
+  next
+    case False
+    from \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p divides\<^bsub>K [X]\<^esub> q"
+      unfolding associated_def by simp
+    hence "p divides\<^bsub>poly_ring R\<^esub> q"
+      using carrier_polynomial[OF assms(1)]
+      unfolding factor_def univ_poly_carrier univ_poly_mult by auto
+    with \<open>q \<noteq> []\<close> have "degree p \<le> degree q"
+      using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp
+    with \<open>q \<noteq> []\<close> show ?thesis
+      by (cases "p = []", auto simp add: Suc_leI le_diff_iff)
+  qed
 
   interpret UP: domain "K[X]"
     using univ_poly_is_domain[OF assms(1)] .
@@ -896,21 +894,23 @@
   interpret UP: domain "K[X]"
     using univ_poly_is_domain[OF assms(1)] .
 
-  { fix q r
-    assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
-    hence not_zero: "q \<noteq> []" "r \<noteq> []"
+  have aux_lemma1: "degree q + degree r = 1" "q \<noteq> []" "r \<noteq> []"
+    if q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" for q r
+  proof -
+    from that have not_zero: "q \<noteq> []" "r \<noteq> []"
       by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
     have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
       using not_zero poly_mult_degree_eq[OF assms(1)] q r
       by (simp add: univ_poly_carrier univ_poly_mult)
-    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
+    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] show "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
       using not_zero by auto
-  } note aux_lemma1 = this
+  qed
 
-  { fix q r
-    assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
-      and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
-    hence "length q = Suc (Suc 0)" and "length r = Suc 0"
+  have aux_lemma2: "r \<in> Units (K[X])"
+    if q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
+    and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0" for q r
+  proof -
+    from that have "length q = Suc (Suc 0)" and "length r = Suc 0"
       by (linarith, metis add.right_neutral add_eq_if length_0_conv)
     from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
       by (metis length_0_conv length_Cons list.exhaust nat.inject)
@@ -933,9 +933,9 @@
     moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
       using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
       unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
-    ultimately have "r \<in> Units (K[X])"
+    ultimately show ?thesis
       using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
-  } note aux_lemma2 = this
+  qed
 
   fix q r
   assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and qr: "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
@@ -1264,24 +1264,24 @@
   interpret UP: domain "poly_ring R"
     using univ_poly_is_domain[OF carrier_is_subring] .
 
-  { fix p q
-    assume p: "p \<in> carrier (poly_ring R)" and q: "q \<in> carrier (poly_ring R)" and pq: "p \<sim>\<^bsub>poly_ring R\<^esub> q"
-    have "is_root p x \<Longrightarrow> is_root q x"
-    proof -
-      assume is_root: "is_root p x"
-      then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
-        using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
-      moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
-        using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
-      ultimately have "[ \<one>, \<ominus> x ] pdivides q"
-        using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
-      with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
-        using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
-              pdivides_imp_is_root[of q x]
-        by fastforce  
-    qed
-  }
-
+  have "is_root q x"
+    if p: "p \<in> carrier (poly_ring R)"
+    and q: "q \<in> carrier (poly_ring R)"
+    and pq: "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+    and is_root: "is_root p x"
+    for p q
+  proof -
+    from is_root have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
+      using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
+    moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+      using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
+    ultimately have "[ \<one>, \<ominus> x ] pdivides q"
+      using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
+    with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
+      using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
+        pdivides_imp_is_root[of q x]
+      by fastforce  
+  qed
   then show ?thesis
     using assms UP.associated_sym[OF assms(3)] by blast 
 qed
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Polynomials.thy
--- a/src/HOL/Algebra/Polynomials.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Polynomials.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -217,29 +217,30 @@
   hence deg_eq: "degree p1 = degree p2"
     using degree_def'[OF assms(1)] degree_def'[OF assms(2)] by auto
   thus "p1 = p2"
-  proof (cases)
-    assume "p1 \<noteq> [] \<and> p2 \<noteq> []"
+  proof (cases "p1 \<noteq> [] \<and> p2 \<noteq> []")
+    case True
     hence "length p1 = length p2"
       using deg_eq by (simp add: Nitpick.size_list_simp(2)) 
     thus ?thesis
       using coeff_iff_length_cond[of p1 p2] coeff_eq by simp
   next
-    { fix p1 p2 assume A: "p1 = []" "coeff p1 = coeff p2" "polynomial K p2"
-      have "p2 = []"
-      proof (rule ccontr)
-        assume "p2 \<noteq> []"
-        hence "(coeff p2) (degree p2) \<noteq> \<zero>"
-          using A(3) unfolding polynomial_def
-          by (metis coeff.simps(2) list.collapse)
-        moreover have "(coeff p1) ` UNIV = { \<zero> }"
-          using A(1) by auto
-        hence "(coeff p2) ` UNIV = { \<zero> }"
-          using A(2) by simp
-        ultimately show False
-          by blast
-      qed } note aux_lemma = this
-    assume "\<not> (p1 \<noteq> [] \<and> p2 \<noteq> [])"
-    hence "p1 = [] \<or> p2 = []" by simp
+    case False
+    have aux_lemma: "p2 = []"
+      if A: "p1 = []" "coeff p1 = coeff p2" "polynomial K p2"
+      for p1 p2
+    proof (rule ccontr)
+      assume "p2 \<noteq> []"
+      hence "(coeff p2) (degree p2) \<noteq> \<zero>"
+        using A(3) unfolding polynomial_def
+        by (metis coeff.simps(2) list.collapse)
+      moreover have "(coeff p1) ` UNIV = { \<zero> }"
+        using A(1) by auto
+      hence "(coeff p2) ` UNIV = { \<zero> }"
+        using A(2) by simp
+      ultimately show False
+        by blast
+    qed
+    from False have "p1 = [] \<or> p2 = []" by simp
     thus ?thesis
       using assms coeff_eq aux_lemma[of p1 p2] aux_lemma[of p2 p1] by auto
   qed
@@ -409,20 +410,19 @@
   assumes "set p1 \<subseteq> K" and "set p2 \<subseteq> K"
   shows "polynomial K (poly_add p1 p2)"
 proof -
-  { fix p1 p2 assume A: "set p1 \<subseteq> K" "set p2 \<subseteq> K" "length p1 \<ge> length p2"
-    hence "polynomial K (poly_add p1 p2)"
-    proof -
-      define p2' where "p2' = (replicate (length p1 - length p2) \<zero>) @ p2"
-      hence "set p2' \<subseteq> K" and "length p1 = length p2'"
-        using A(2-3) subringE(2)[OF K] by auto
-      hence "set (map2 (\<oplus>) p1 p2') \<subseteq> K"
-        using A(1) subringE(7)[OF K]
-        by (induct p1) (auto, metis set_ConsD subsetD set_zip_leftD set_zip_rightD)
-      thus ?thesis
-        unfolding p2'_def using normalize_gives_polynomial A(3) by simp
-    qed }
-  thus ?thesis
-    using assms by auto
+  have "polynomial K (poly_add p1 p2)"
+    if A: "set p1 \<subseteq> K" "set p2 \<subseteq> K" "length p1 \<ge> length p2" for p1 p2
+  proof -
+    define p2' where "p2' = (replicate (length p1 - length p2) \<zero>) @ p2"
+    hence "set p2' \<subseteq> K" and "length p1 = length p2'"
+      using A(2-3) subringE(2)[OF K] by auto
+    hence "set (map2 (\<oplus>) p1 p2') \<subseteq> K"
+      using A(1) subringE(7)[OF K]
+      by (induct p1) (auto, metis set_ConsD subsetD set_zip_leftD set_zip_rightD)
+    thus ?thesis
+      unfolding p2'_def using normalize_gives_polynomial A(3) by simp
+  qed
+  thus ?thesis using assms by auto
 qed
 
 lemma poly_add_closed: "\<lbrakk> polynomial K p1; polynomial K p2 \<rbrakk> \<Longrightarrow> polynomial K (poly_add p1 p2)"
@@ -432,29 +432,28 @@
   assumes "polynomial K p1" "polynomial K p2" and "length p1 \<noteq> length p2"
   shows "length (poly_add p1 p2) = max (length p1) (length p2)"
 proof -
-  { fix p1 p2 assume A: "polynomial K p1" "polynomial K p2" "length p1 > length p2"
-    hence "length (poly_add p1 p2) = max (length p1) (length p2)"
-    proof -
-      let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
-      have p1: "p1 \<noteq> []" and p2: "?p2 \<noteq> []"
-        using A(3) by auto
-      then have "zip p1 (replicate (length p1 - length p2) \<zero> @ p2) = zip (lead_coeff p1 # tl p1) (lead_coeff (replicate (length p1 - length p2) \<zero> @ p2) # tl (replicate (length p1 - length p2) \<zero> @ p2))"
-        by auto
-      hence "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1 \<oplus> lead_coeff ?p2"
-        by simp
-      moreover have "lead_coeff p1 \<in> carrier R"
-        using p1 A(1) lead_coeff_in_carrier[OF K, of "hd p1" "tl p1"] by auto
-      ultimately have "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1"
-        using A(3) by auto
-      moreover have "lead_coeff p1 \<noteq> \<zero>"
-        using p1 A(1) unfolding polynomial_def by simp
-      ultimately have "length (normalize (map2 (\<oplus>) p1 ?p2)) = length p1"
-        using normalize_length_eq by auto
-      thus ?thesis
-        using A(3) by auto
-    qed }
-  thus ?thesis
-    using assms by auto
+  have "length (poly_add p1 p2) = max (length p1) (length p2)"
+    if A: "polynomial K p1" "polynomial K p2" "length p1 > length p2" for p1 p2
+  proof -
+    let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
+    have p1: "p1 \<noteq> []" and p2: "?p2 \<noteq> []"
+      using A(3) by auto
+    then have "zip p1 (replicate (length p1 - length p2) \<zero> @ p2) =
+        zip (lead_coeff p1 # tl p1) (lead_coeff (replicate (length p1 - length p2) \<zero> @ p2) # tl (replicate (length p1 - length p2) \<zero> @ p2))"
+      by auto
+    hence "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1 \<oplus> lead_coeff ?p2"
+      by simp
+    moreover have "lead_coeff p1 \<in> carrier R"
+      using p1 A(1) lead_coeff_in_carrier[OF K, of "hd p1" "tl p1"] by auto
+    ultimately have "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1"
+      using A(3) by auto
+    moreover have "lead_coeff p1 \<noteq> \<zero>"
+      using p1 A(1) unfolding polynomial_def by simp
+    ultimately have "length (normalize (map2 (\<oplus>) p1 ?p2)) = length p1"
+      using normalize_length_eq by auto
+    thus ?thesis using A(3) by auto
+  qed
+  thus ?thesis using assms by auto
 qed
 
 lemma poly_add_degree_eq:
@@ -471,10 +470,10 @@
 
 lemma poly_add_length_le: "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
 proof -
-  { fix p1 p2 :: "'a list" assume A: "length p1 \<ge> length p2"
-    let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
-    have "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
-      using normalize_length_le[of "map2 (\<oplus>) p1 ?p2"] A by auto }
+  have "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
+    if "length p1 \<ge> length p2" for p1 p2 :: "'a list"
+    using normalize_length_le[of "map2 (\<oplus>) p1 ((replicate (length p1 - length p2) \<zero>) @ p2)"] that
+    by auto
   thus ?thesis
     by (metis le_cases max.commute poly_add.simps)
 qed
@@ -582,57 +581,58 @@
   assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
   shows "poly_add p1 p2 = poly_add (normalize p1) p2"
 proof -
-  { fix n p1 p2 assume "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
-    hence "poly_add p1 p2 = poly_add ((replicate n \<zero>) @ p1) p2"
-    proof (induction n)
-      case 0 thus ?case by simp
-    next
-      { fix p1 p2 :: "'a list"
-        assume in_carrier: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
-        have "poly_add p1 p2 = poly_add (\<zero> # p1) p2"
-        proof -
-          have "length p1 \<ge> length p2 \<Longrightarrow> ?thesis"
-          proof -
-            assume A: "length p1 \<ge> length p2"
-            let ?p2 = "\<lambda>n. (replicate n \<zero>) @ p2"
-            have "poly_add p1 p2 = normalize (map2 (\<oplus>) (\<zero> # p1) (\<zero> # ?p2 (length p1 - length p2)))"
-              using A by simp
-            also have " ... = normalize (map2 (\<oplus>) (\<zero> # p1) (?p2 (length (\<zero> # p1) - length p2)))"
-              by (simp add: A Suc_diff_le)
-            also have " ... = poly_add (\<zero> # p1) p2"
-              using A by simp
-            finally show ?thesis .
-          qed
+  have aux_lemma: "poly_add p1 p2 = poly_add ((replicate n \<zero>) @ p1) p2"
+    if "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+    for n p1 p2
+    using that
+  proof (induction n)
+    case 0
+    thus ?case by simp
+  next
+    case (Suc n)
+    have aux_lemma: "poly_add p1 p2 = poly_add (\<zero> # p1) p2"
+      if in_carrier: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+      for p1 p2
+    proof -
+      have "length p1 \<ge> length p2 \<Longrightarrow> ?thesis"
+      proof -
+        assume A: "length p1 \<ge> length p2"
+        let ?p2 = "\<lambda>n. (replicate n \<zero>) @ p2"
+        have "poly_add p1 p2 = normalize (map2 (\<oplus>) (\<zero> # p1) (\<zero> # ?p2 (length p1 - length p2)))"
+          using A by simp
+        also have " ... = normalize (map2 (\<oplus>) (\<zero> # p1) (?p2 (length (\<zero> # p1) - length p2)))"
+          by (simp add: A Suc_diff_le)
+        also have " ... = poly_add (\<zero> # p1) p2"
+          using A by simp
+        finally show ?thesis .
+      qed
+      moreover have "length p2 > length p1 \<Longrightarrow> ?thesis"
+      proof -
+        assume A: "length p2 > length p1"
+        let ?f = "\<lambda>n p. (replicate n \<zero>) @ p"
+        have "poly_add p1 p2 = poly_add p2 p1"
+          using A by simp
+        also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - length p1) p1))"
+          using A by simp
+        also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - Suc (length p1)) (\<zero> # p1)))"
+          by (metis A Suc_diff_Suc append_Cons replicate_Suc replicate_app_Cons_same)
+        also have " ... = poly_add p2 (\<zero> # p1)"
+          using A by simp
+        also have " ... = poly_add (\<zero> # p1) p2"
+          using poly_add_comm[of p2 "\<zero> # p1"] in_carrier by auto
+        finally show ?thesis .
+      qed
+      ultimately show ?thesis by auto
+    qed
 
-          moreover have "length p2 > length p1 \<Longrightarrow> ?thesis"
-          proof -
-            assume A: "length p2 > length p1"
-            let ?f = "\<lambda>n p. (replicate n \<zero>) @ p"
-            have "poly_add p1 p2 = poly_add p2 p1"
-              using A by simp
-            also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - length p1) p1))"
-              using A by simp
-            also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - Suc (length p1)) (\<zero> # p1)))"
-              by (metis A Suc_diff_Suc append_Cons replicate_Suc replicate_app_Cons_same)
-            also have " ... = poly_add p2 (\<zero> # p1)"
-              using A by simp
-            also have " ... = poly_add (\<zero> # p1) p2"
-              using poly_add_comm[of p2 "\<zero> # p1"] in_carrier by auto
-            finally show ?thesis .
-          qed
-
-          ultimately show ?thesis by auto
-        qed } note aux_lemma = this
-
-      case (Suc n)
-      hence in_carrier: "set (replicate n \<zero> @ p1) \<subseteq> carrier R"
-        by auto
-      have "poly_add p1 p2 = poly_add (replicate n \<zero> @ p1) p2"
-        using Suc by simp
-      also have " ... = poly_add (replicate (Suc n) \<zero> @ p1) p2"
-        using aux_lemma[OF in_carrier Suc(3)] by simp
-      finally show ?case .
-    qed } note aux_lemma = this
+    from Suc have in_carrier: "set (replicate n \<zero> @ p1) \<subseteq> carrier R"
+      by auto
+    have "poly_add p1 p2 = poly_add (replicate n \<zero> @ p1) p2"
+      using Suc by simp
+    also have " ... = poly_add (replicate (Suc n) \<zero> @ p1) p2"
+      using aux_lemma[OF in_carrier Suc(3)] by simp
+    finally show ?case .
+  qed
 
   have "poly_add p1 p2 =
         poly_add ((replicate (length p1 - length (normalize p1)) \<zero>) @ normalize p1) p2"
@@ -935,29 +935,29 @@
   assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
   shows "poly_mult p1 p2 = poly_mult ((replicate n \<zero>) @ p1) p2"
 proof -
-  { fix p1 p2 assume A: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
-    hence "poly_mult p1 p2 = poly_mult (\<zero> # p1) p2"
-    proof -
-      let ?a_p2 = "(map ((\<otimes>) \<zero>) p2) @ (replicate (length p1) \<zero>)"
-      have "?a_p2 = replicate (length p2 + length p1) \<zero>"
-        using A(2) by (induction p2) (auto)
-      hence "poly_mult (\<zero> # p1) p2 = poly_add (replicate (length p2 + length p1) \<zero>) (poly_mult p1 p2)"
-        by simp
-      also have " ... = poly_add (normalize (replicate (length p2 + length p1) \<zero>)) (poly_mult p1 p2)"
-        using poly_add_normalize(1)[of "replicate (length p2 + length p1) \<zero>" "poly_mult p1 p2"]
-              poly_mult_in_carrier[OF A] by force
-      also have " ... = poly_mult p1 p2"
-        using poly_add_zero(2)[OF _ poly_mult_is_polynomial[OF _ A]] carrier_is_subring
-              normalize_replicate_zero[of "length p2 + length p1" "[]"] by simp
-      finally show ?thesis by auto
-    qed } note aux_lemma = this
-  
+  have aux_lemma: "poly_mult p1 p2 = poly_mult (\<zero> # p1) p2"
+    if A: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R" for p1 p2
+  proof -
+    let ?a_p2 = "(map ((\<otimes>) \<zero>) p2) @ (replicate (length p1) \<zero>)"
+    have "?a_p2 = replicate (length p2 + length p1) \<zero>"
+      using A(2) by (induction p2) (auto)
+    hence "poly_mult (\<zero> # p1) p2 = poly_add (replicate (length p2 + length p1) \<zero>) (poly_mult p1 p2)"
+      by simp
+    also have " ... = poly_add (normalize (replicate (length p2 + length p1) \<zero>)) (poly_mult p1 p2)"
+      using poly_add_normalize(1)[of "replicate (length p2 + length p1) \<zero>" "poly_mult p1 p2"]
+            poly_mult_in_carrier[OF A] by force
+    also have " ... = poly_mult p1 p2"
+      using poly_add_zero(2)[OF _ poly_mult_is_polynomial[OF _ A]] carrier_is_subring
+            normalize_replicate_zero[of "length p2 + length p1" "[]"] by simp
+    finally show ?thesis by auto
+  qed
   from assms show ?thesis
   proof (induction n)
-    case 0 thus ?case by simp
+    case 0
+    thus ?case by simp
   next
-    case (Suc n) thus ?case
-      using aux_lemma[of "replicate n \<zero> @ p1" p2] by force
+    case (Suc n)
+    thus ?case using aux_lemma[of "replicate n \<zero> @ p1" p2] by force
   qed
 qed
 
@@ -1896,14 +1896,15 @@
   assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" and "a \<in> carrier R"
   shows "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
 proof -
-  { fix p q assume A: "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" "length p \<ge> length q"
-    hence "eval (poly_add p ((replicate (length p - length q) \<zero>) @ q)) a =
+  have aux_lemma: "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
+    if A: "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" "length p \<ge> length q" for p q
+  proof -
+    from that have "eval (poly_add p ((replicate (length p - length q) \<zero>) @ q)) a =
          (eval p a) \<oplus> (eval ((replicate (length p - length q) \<zero>) @ q) a)"
       using eval_poly_add_aux[OF A(1) _ _ assms(3), of "(replicate (length p - length q) \<zero>) @ q"] by force
-    hence "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
-      using eval_replicate[OF A(2) assms(3)] A(3) by auto }
-  note aux_lemma = this
-
+    then show "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
+      using eval_replicate[OF A(2) assms(3)] A(3) by auto
+  qed
   have ?thesis if "length q \<ge> length p"
     using assms(1-2)[THEN eval_in_carrier[OF _ assms(3)]] poly_add_comm[OF assms(1-2)]
           aux_lemma[OF assms(2,1) that]
@@ -1978,8 +1979,12 @@
   case Nil thus ?case
     using eval_in_carrier[OF assms(2-3)] by simp
 next
-  { fix n b assume b: "b \<in> carrier R"
-    hence "set (map ((\<otimes>) b) q) \<subseteq> carrier R" and "set (replicate n \<zero>) \<subseteq> carrier R"
+  case (Cons b p)
+
+  have aux_lemma: "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval (monom b n) a) \<otimes> (eval q a)"
+    if b: "b \<in> carrier R" for n b
+  proof -
+    from that have "set (map ((\<otimes>) b) q) \<subseteq> carrier R" and "set (replicate n \<zero>) \<subseteq> carrier R"
       using assms(2) by (induct q) (auto)
     hence "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval ((map ((\<otimes>) b) q)) a) \<otimes> (a [^] n) \<oplus> \<zero>"
       using eval_append[OF _ _ assms(3), of "map ((\<otimes>) b) q" "replicate n \<zero>"] 
@@ -1990,12 +1995,11 @@
       by simp
     also have " ... = (b \<otimes> (a [^] n)) \<otimes> (eval q a)"
       using eval_in_carrier[OF assms(2-3)] b assms(3) m_assoc m_comm by auto
-    finally have "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval (monom b n) a) \<otimes> (eval q a)"
-      using eval_monom[OF b assms(3)] by simp }
-  note aux_lemma = this
+    finally show ?thesis
+      using eval_monom[OF b assms(3)] by simp
+  qed
 
-  case (Cons b p)
-  hence in_carrier:
+  from Cons have in_carrier:
     "eval (monom b (length p)) a \<in> carrier R" "eval p a \<in> carrier R" "eval q a \<in> carrier R" "b \<in> carrier R"
     using eval_in_carrier monom_in_carrier assms by auto
   have set_map: "set ((map ((\<otimes>) b) q) @ (replicate (length p) \<zero>)) \<subseteq> carrier R"
@@ -2183,43 +2187,52 @@
   interpret UP: domain "K[X]"
     using univ_poly_is_domain[OF assms(1)] .
 
-  { fix l assume "set l \<subseteq> K"
-    hence "poly_of_const a \<in> carrier (K[X])" if "a \<in> set l" for a
+  have aux_lemma1: "set (?map_norm l) \<subseteq> carrier (K[X])" if "set l \<subseteq> K" for l
+  proof -
+    from that have "poly_of_const a \<in> carrier (K[X])" if "a \<in> set l" for a
       using that normalize_gives_polynomial[of "[ a ]" K]
       unfolding univ_poly_carrier poly_of_const_def by auto
-    hence "set (?map_norm l) \<subseteq> carrier (K[X])"
-      by auto }
-  note aux_lemma1 = this
+    then show ?thesis by auto
+  qed
 
-  { fix q l assume set_l: "set l \<subseteq> K" and q: "q \<in> carrier (K[X])"
-    from set_l have "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \<zero>) @ l)) q" for n
-    proof (induct n, simp)
-      case (Suc n)
-      from \<open>set l \<subseteq> K\<close> have set_replicate: "set ((replicate n \<zero>) @ l) \<subseteq> K"
-        using subringE(2)[OF assms(1)] by (induct n) (auto)
-      have step: "UP.eval (?map_norm l') q = UP.eval (?map_norm (\<zero> # l')) q" if "set l' \<subseteq> K" for l'
-        using UP.eval_in_carrier[OF aux_lemma1[OF that]] q unfolding poly_of_const_def
-        by (simp, simp add: sym[OF univ_poly_zero[of R K]])
-      have "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \<zero>) @ l)) q"
-        using Suc by simp
-      also have " ... = UP.eval (map poly_of_const ((replicate (Suc n) \<zero>) @ l)) q"
-        using step[OF set_replicate] by simp
-      finally show ?case .
-    qed }
-  note aux_lemma2 = this
+  have aux_lemma2: "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \<zero>) @ l)) q"
+    if set_l: "set l \<subseteq> K" and q: "q \<in> carrier (K[X])"
+    for n q l
+    using set_l
+  proof (induct n)
+    case 0
+    then show ?case by simp
+  next
+    case (Suc n)
+    from \<open>set l \<subseteq> K\<close> have set_replicate: "set ((replicate n \<zero>) @ l) \<subseteq> K"
+      using subringE(2)[OF assms(1)] by (induct n) (auto)
+    have step: "UP.eval (?map_norm l') q = UP.eval (?map_norm (\<zero> # l')) q" if "set l' \<subseteq> K" for l'
+      using UP.eval_in_carrier[OF aux_lemma1[OF that]] q unfolding poly_of_const_def
+      by (simp, simp add: sym[OF univ_poly_zero[of R K]])
+    have "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \<zero>) @ l)) q"
+      using Suc by simp
+    also have " ... = UP.eval (map poly_of_const ((replicate (Suc n) \<zero>) @ l)) q"
+      using step[OF set_replicate] by simp
+    finally show ?case .
+  qed
 
-  { fix q l assume "set l \<subseteq> K" and q: "q \<in> carrier (K[X])"
+  have aux_lemma3: "UP.eval (?map_norm l) q = UP.eval (?map_norm (normalize l)) q"
+    if "set l \<subseteq> K" and q: "q \<in> carrier (K[X])" for q l
+  proof -
     from \<open>set l \<subseteq> K\<close> have set_norm: "set (normalize l) \<subseteq> K"
       by (induct l) (auto)
-    have "UP.eval (?map_norm l) q = UP.eval (?map_norm (normalize l)) q"
+    show ?thesis
       using aux_lemma2[OF set_norm q, of "length l - length (local.normalize l)"]
-      unfolding sym[OF normalize_trick[of l]] .. }
-  note aux_lemma3 = this
+      unfolding sym[OF normalize_trick[of l]] ..
+  qed
 
   from \<open>p \<in> carrier (K[X])\<close> show ?thesis
   proof (induct "length p" arbitrary: p rule: less_induct)
     case less thus ?case
-    proof (cases p, simp add: univ_poly_zero)
+    proof (cases p)
+      case Nil
+      then show ?thesis by (simp add: univ_poly_zero)
+    next
       case (Cons a l)
       hence a: "a \<in> carrier R - { \<zero> }" and set_l: "set l \<subseteq> carrier R" "set l \<subseteq> K"
         using less(2) subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Ring_Divisibility.thy
--- a/src/HOL/Algebra/Ring_Divisibility.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Ring_Divisibility.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -518,22 +518,22 @@
   assumes "C \<noteq> {}" "subset.chain { I. ideal I R } C"
   shows "\<Union>C \<in> C"
 proof -
-  { fix S assume "finite S" "S \<subseteq> \<Union>C"
-    hence "\<exists>I. I \<in> C \<and> S \<subseteq> I"
-    proof (induct S)
-      case empty thus ?case
-        using assms(1) by blast
-    next
-      case (insert s S)
-      then obtain I where I: "I \<in> C" "S \<subseteq> I"
-        by blast
-      moreover obtain I' where I': "I' \<in> C" "s \<in> I'"
-        using insert(4) by blast
-      ultimately have "I \<subseteq> I' \<or> I' \<subseteq> I"
-        using assms unfolding pred_on.chain_def by blast
-      thus ?case
-        using I I' by blast
-    qed } note aux_lemma = this
+  have aux_lemma: "\<exists>I. I \<in> C \<and> S \<subseteq> I" if "finite S" "S \<subseteq> \<Union>C" for S
+    using that
+  proof (induct S)
+    case empty
+    thus ?case using assms(1) by blast
+  next
+    case (insert s S)
+    then obtain I where I: "I \<in> C" "S \<subseteq> I"
+      by blast
+    moreover obtain I' where I': "I' \<in> C" "s \<in> I'"
+      using insert(4) by blast
+    ultimately have "I \<subseteq> I' \<or> I' \<subseteq> I"
+      using assms unfolding pred_on.chain_def by blast
+    thus ?case
+      using I I' by blast
+  qed
 
   obtain S where S: "finite S" "S \<subseteq> carrier R" "\<Union>C = Idl S"
     using finetely_gen[OF chain_Union_is_ideal[OF assms(2)]] assms(1) by auto
@@ -805,27 +805,27 @@
   assumes "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
   shows "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b \<longleftrightarrow> d gcdof a b"
 proof -
-  { fix a b d
-    assume in_carrier: "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
-       and ideal_eq: "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b"
-    have "d gcdof a b"
-    proof (auto simp add: isgcd_def)
-      have "a \<in> PIdl d" and "b \<in> PIdl d"
-        using in_carrier(1-2)[THEN cgenideal_ideal] additive_subgroup.zero_closed[OF ideal.axioms(1)]
-              in_carrier(1-2)[THEN cgenideal_self] in_carrier(1-2)
-        unfolding ideal_eq set_add_def' by force+
-      thus "d divides a" and "d divides b"
-        using in_carrier(1,2)[THEN to_contain_is_to_divide[OF in_carrier(3)]]
-              cgenideal_minimal[OF cgenideal_ideal[OF in_carrier(3)]] by simp+
-    next
-      fix c assume c: "c \<in> carrier R" "c divides a" "c divides b"
-      hence "PIdl a \<subseteq> PIdl c" and "PIdl b \<subseteq> PIdl c"
-        using to_contain_is_to_divide in_carrier by auto
-      hence "PIdl a <+>\<^bsub>R\<^esub> PIdl b \<subseteq> PIdl c"
-        by (metis Un_subset_iff c(1) in_carrier(1-2) cgenideal_ideal genideal_minimal union_genideal)
-      thus "c divides d"
-        using ideal_eq to_contain_is_to_divide[OF c(1) in_carrier(3)] by simp
-    qed } note aux_lemma = this
+  have aux_lemma: "d gcdof a b"
+    if in_carrier: "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
+    and ideal_eq: "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b"
+    for a b d
+  proof (auto simp add: isgcd_def)
+    have "a \<in> PIdl d" and "b \<in> PIdl d"
+      using in_carrier(1-2)[THEN cgenideal_ideal] additive_subgroup.zero_closed[OF ideal.axioms(1)]
+            in_carrier(1-2)[THEN cgenideal_self] in_carrier(1-2)
+      unfolding ideal_eq set_add_def' by force+
+    thus "d divides a" and "d divides b"
+      using in_carrier(1,2)[THEN to_contain_is_to_divide[OF in_carrier(3)]]
+            cgenideal_minimal[OF cgenideal_ideal[OF in_carrier(3)]] by simp+
+  next
+    fix c assume c: "c \<in> carrier R" "c divides a" "c divides b"
+    hence "PIdl a \<subseteq> PIdl c" and "PIdl b \<subseteq> PIdl c"
+      using to_contain_is_to_divide in_carrier by auto
+    hence "PIdl a <+>\<^bsub>R\<^esub> PIdl b \<subseteq> PIdl c"
+      by (metis Un_subset_iff c(1) in_carrier(1-2) cgenideal_ideal genideal_minimal union_genideal)
+    thus "c divides d"
+      using ideal_eq to_contain_is_to_divide[OF c(1) in_carrier(3)] by simp
+  qed
 
   have "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b \<Longrightarrow> d gcdof a b"
     using aux_lemma assms by simp
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/SndIsomorphismGrp.thy
--- a/src/HOL/Algebra/SndIsomorphismGrp.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/SndIsomorphismGrp.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -119,15 +119,14 @@
   have "group ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
     by (simp add: H_contained_in_set_mult normal.factorgroup_is_group normal_axioms 
         normal_restrict_supergroup normal_set_mult_subgroup)
-  moreover
-  { fix g
-    assume g: "g \<in> S"
-    with g have "g \<in> H <#> S"
+  moreover have "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)" if g: "g \<in> S" for g
+  proof -
+    from g that have "g \<in> H <#> S"
       using S_contained_in_set_mult by blast
-    hence "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)" 
-      unfolding FactGroup_def RCOSETS_def r_coset_def by auto }
-  moreover
-  have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> H #> x \<otimes> y = H #> x <#> (H #> y)"
+    thus "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)" 
+      unfolding FactGroup_def RCOSETS_def r_coset_def by auto
+  qed
+  moreover have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> H #> x \<otimes> y = H #> x <#> (H #> y)"
     using normal.rcos_sum normal_axioms subgroup.mem_carrier subgrpS by fastforce
   ultimately show ?thesis
     by (auto simp: group_hom_def group_hom_axioms_def hom_def)
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/Sym_Groups.thy
--- a/src/HOL/Algebra/Sym_Groups.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Sym_Groups.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -207,19 +207,22 @@
   shows "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
                      swapidseq_ext A' n p' \<and> p = (transpose a b) \<circ> p'"
 proof -
-  { fix A n k and p :: "'a \<Rightarrow> 'a"
-    assume "swapidseq_ext A n p" "n = Suc k"
-    hence "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
-                       swapidseq_ext A' k p' \<and> p = (transpose a b) \<circ> p'"
-    proof (induction, simp)
-      case single thus ?case
-        by (metis Un_insert_right insert_iff insert_is_Un swapidseq_ext.single)
-    next
-      case comp thus ?case
-        by blast 
-    qed }
-  thus ?thesis
-    using assms by simp
+  have "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
+                     swapidseq_ext A' k p' \<and> p = (transpose a b) \<circ> p'"
+    if "swapidseq_ext A n p" "n = Suc k"
+    for A n k and p :: "'a \<Rightarrow> 'a"
+    using that
+  proof (induction)
+    case empty
+    thus ?case by simp
+  next
+    case single
+    thus ?case by (metis Un_insert_right insert_iff insert_is_Un swapidseq_ext.single)
+  next
+    case comp
+    thus ?case by blast 
+  qed
+  thus ?thesis using assms by simp
 qed
 
 lemma swapidseq_ext_backwards':
@@ -369,61 +372,61 @@
   proof
     show "generate (alt_group n) (three_cycles n) \<subseteq> carrier (alt_group n)"
       using A.generate_subgroup_incl[OF three_cycles_incl A.subgroup_self] .
-  next
     show "carrier (alt_group n) \<subseteq> generate (alt_group n) (three_cycles n)"
     proof
-      { fix q :: "nat \<Rightarrow> nat" and a b c
-        assume "a \<noteq> b" "b \<noteq> c" "{ a, b, c } \<subseteq> {1..n}" 
-        have "cycle_of_list [a, b, c] \<in> generate (alt_group n) (three_cycles n)"
-        proof (cases)
-          assume "c = a"
-          hence "cycle_of_list [ a, b, c ] = id"
-            by (simp add: swap_commute)
-          thus "cycle_of_list [ a, b, c ] \<in> generate (alt_group n) (three_cycles n)"
-            using one[of "alt_group n"] unfolding alt_group_one by simp
-        next
-          assume "c \<noteq> a"
-          have "distinct [a, b, c]"
-            using \<open>a \<noteq> b\<close> and \<open>b \<noteq> c\<close> and \<open>c \<noteq> a\<close> by auto
-          with \<open>{ a, b, c } \<subseteq> {1..n}\<close>
-          show "cycle_of_list [ a, b, c ] \<in> generate (alt_group n) (three_cycles n)"
-            by (intro incl, fastforce)
-        qed } note aux_lemma1 = this
+      have aux_lemma1: "cycle_of_list [a, b, c] \<in> generate (alt_group n) (three_cycles n)"
+        if "a \<noteq> b" "b \<noteq> c" "{ a, b, c } \<subseteq> {1..n}"
+        for q :: "nat \<Rightarrow> nat" and a b c
+      proof (cases)
+        assume "c = a"
+        hence "cycle_of_list [ a, b, c ] = id"
+          by (simp add: swap_commute)
+        thus "cycle_of_list [ a, b, c ] \<in> generate (alt_group n) (three_cycles n)"
+          using one[of "alt_group n"] unfolding alt_group_one by simp
+      next
+        assume "c \<noteq> a"
+        have "distinct [a, b, c]"
+          using \<open>a \<noteq> b\<close> and \<open>b \<noteq> c\<close> and \<open>c \<noteq> a\<close> by auto
+        with \<open>{ a, b, c } \<subseteq> {1..n}\<close>
+        show "cycle_of_list [ a, b, c ] \<in> generate (alt_group n) (three_cycles n)"
+          by (intro incl) fastforce
+      qed
     
-      { fix S :: "nat set" and q :: "nat \<Rightarrow> nat"
-        assume seq: "swapidseq_ext S (Suc (Suc 0)) q" and S: "S \<subseteq> {1..n}"
-        have "q \<in> generate (alt_group n) (three_cycles n)"
-        proof -
-          obtain a b q' where ab: "a \<noteq> b" "a \<in> S" "b \<in> S"
-            and q': "swapidseq_ext S (Suc 0) q'" "q = (transpose a b) \<circ> q'"
-            using swapidseq_ext_backwards'[OF seq] by auto 
-          obtain c d where cd: "c \<noteq> d" "c \<in> S" "d \<in> S"
-            and q: "q = (transpose a b) \<circ> (Fun.swap c d id)"
-            using swapidseq_ext_backwards'[OF q'(1)]
-                  swapidseq_ext_zero_imp_id
-            unfolding q'(2)
-            by fastforce
+      have aux_lemma2: "q \<in> generate (alt_group n) (three_cycles n)"
+        if seq: "swapidseq_ext S (Suc (Suc 0)) q" and S: "S \<subseteq> {1..n}"
+        for S :: "nat set" and q :: "nat \<Rightarrow> nat"
+      proof -
+        obtain a b q' where ab: "a \<noteq> b" "a \<in> S" "b \<in> S"
+          and q': "swapidseq_ext S (Suc 0) q'" "q = (transpose a b) \<circ> q'"
+          using swapidseq_ext_backwards'[OF seq] by auto 
+        obtain c d where cd: "c \<noteq> d" "c \<in> S" "d \<in> S"
+          and q: "q = (transpose a b) \<circ> (Fun.swap c d id)"
+          using swapidseq_ext_backwards'[OF q'(1)]
+            swapidseq_ext_zero_imp_id
+          unfolding q'(2)
+          by fastforce
 
-          consider (eq) "b = c" | (ineq) "b \<noteq> c" by auto
-          thus ?thesis
-          proof cases
-            case eq then have "q = cycle_of_list [ a, b, d ]"
-              unfolding q by simp
-            moreover have "{ a, b, d } \<subseteq> {1..n}"
-              using ab cd S by blast
-            ultimately show ?thesis
-              using aux_lemma1[OF ab(1)] cd(1) eq by simp
-          next
-            case ineq
-            hence "q = cycle_of_list [ a, b, c ] \<circ> cycle_of_list [ b, c, d ]"
-              unfolding q by (simp add: swap_nilpotent o_assoc)
-            moreover have "{ a, b, c } \<subseteq> {1..n}" and "{ b, c, d } \<subseteq> {1..n}"
-              using ab cd S by blast+
-            ultimately show ?thesis
-              using eng[OF aux_lemma1[OF ab(1) ineq] aux_lemma1[OF ineq cd(1)]]
-              unfolding alt_group_mult by simp
-          qed
-        qed } note aux_lemma2 = this
+        consider (eq) "b = c" | (ineq) "b \<noteq> c" by auto
+        thus ?thesis
+        proof cases
+          case eq
+          then have "q = cycle_of_list [ a, b, d ]"
+            unfolding q by simp
+          moreover have "{ a, b, d } \<subseteq> {1..n}"
+            using ab cd S by blast
+          ultimately show ?thesis
+            using aux_lemma1[OF ab(1)] cd(1) eq by simp
+        next
+          case ineq
+          hence "q = cycle_of_list [ a, b, c ] \<circ> cycle_of_list [ b, c, d ]"
+            unfolding q by (simp add: swap_nilpotent o_assoc)
+          moreover have "{ a, b, c } \<subseteq> {1..n}" and "{ b, c, d } \<subseteq> {1..n}"
+            using ab cd S by blast+
+          ultimately show ?thesis
+            using eng[OF aux_lemma1[OF ab(1) ineq] aux_lemma1[OF ineq cd(1)]]
+            unfolding alt_group_mult by simp
+        qed
+      qed
       
       fix p assume "p \<in> carrier (alt_group n)" then have p: "p permutes {1..n}" "evenperm p"
         unfolding alt_group_carrier by auto
@@ -464,66 +467,67 @@
   show "derived (alt_group n) (carrier (alt_group n)) \<subseteq> carrier (alt_group n)"
     using group.derived_in_carrier[OF alt_group_is_group] by simp
 next
-  { fix p assume "p \<in> three_cycles n" have "p \<in> derived (alt_group n) (carrier (alt_group n))"
-    proof -
-      obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}"
-        using \<open>p \<in> three_cycles n\<close> by auto
-      then obtain a b c where cs_def: "cs = [ a, b, c ]"
-        using stupid_lemma[OF cs(3)] by blast
-      have "card (set cs) = 3"
-        using cs(2-3)
-        by (simp add: distinct_card)
+  have aux_lemma: "p \<in> derived (alt_group n) (carrier (alt_group n))"
+    if "p \<in> three_cycles n" for p
+  proof -
+    obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}"
+      using \<open>p \<in> three_cycles n\<close> by auto
+    then obtain a b c where cs_def: "cs = [ a, b, c ]"
+      using stupid_lemma[OF cs(3)] by blast
+    have "card (set cs) = 3"
+      using cs(2-3)
+      by (simp add: distinct_card)
 
-      have "set cs \<noteq> {1..n}"
-        using assms cs(3) unfolding sym[OF distinct_card[OF cs(2)]] by auto
-      then obtain d where d: "d \<notin> set cs" "d \<in> {1..n}"
-        using cs(4) by blast
+    have "set cs \<noteq> {1..n}"
+      using assms cs(3) unfolding sym[OF distinct_card[OF cs(2)]] by auto
+    then obtain d where d: "d \<notin> set cs" "d \<in> {1..n}"
+      using cs(4) by blast
 
-      hence "cycle (d # cs)" and "length (d # cs) = 4" and "card {1..n} = n"
-        using cs(2-3) by auto 
-      hence "set (d # cs) \<noteq> {1..n}"
-        using assms unfolding sym[OF distinct_card[OF \<open>cycle (d # cs)\<close>]]
-        by (metis Suc_n_not_le_n eval_nat_numeral(3)) 
-      then obtain e where e: "e \<notin> set (d # cs)" "e \<in> {1..n}"
-        using d cs(4) by (metis insert_subset list.simps(15) subsetI subset_antisym) 
+    hence "cycle (d # cs)" and "length (d # cs) = 4" and "card {1..n} = n"
+      using cs(2-3) by auto 
+    hence "set (d # cs) \<noteq> {1..n}"
+      using assms unfolding sym[OF distinct_card[OF \<open>cycle (d # cs)\<close>]]
+      by (metis Suc_n_not_le_n eval_nat_numeral(3)) 
+    then obtain e where e: "e \<notin> set (d # cs)" "e \<in> {1..n}"
+      using d cs(4) by (metis insert_subset list.simps(15) subsetI subset_antisym) 
 
-      define q where "q = (Fun.swap d e id) \<circ> (Fun.swap b c id)"
-      hence "bij q"
-        by (simp add: bij_comp)
-      moreover have "q b = c" and "q c = b"
-        using d(1) e(1) unfolding q_def cs_def by simp+
-      moreover have "q a = a"
-        using d(1) e(1) cs(2) unfolding q_def cs_def by auto
-      ultimately have "q \<circ> p \<circ> (inv' q) = cycle_of_list [ a, c, b ]"
-        using conjugation_of_cycle[OF cs(2), of q]
-        unfolding sym[OF cs(1)] unfolding cs_def by simp
-      also have " ... = p \<circ> p"
-        using cs(2) unfolding cs(1) cs_def
-        by (simp add: comp_swap swap_commute transpose_comp_triple) 
-      finally have "q \<circ> p \<circ> (inv' q) = p \<circ> p" .
-      moreover have "bij p"
-        unfolding cs(1) cs_def by (simp add: bij_comp)
-      ultimately have p: "q \<circ> p \<circ> (inv' q) \<circ> (inv' p) = p"
-        by (simp add: bijection.intro bijection.inv_comp_right comp_assoc)
+    define q where "q = (Fun.swap d e id) \<circ> (Fun.swap b c id)"
+    hence "bij q"
+      by (simp add: bij_comp)
+    moreover have "q b = c" and "q c = b"
+      using d(1) e(1) unfolding q_def cs_def by simp+
+    moreover have "q a = a"
+      using d(1) e(1) cs(2) unfolding q_def cs_def by auto
+    ultimately have "q \<circ> p \<circ> (inv' q) = cycle_of_list [ a, c, b ]"
+      using conjugation_of_cycle[OF cs(2), of q]
+      unfolding sym[OF cs(1)] unfolding cs_def by simp
+    also have " ... = p \<circ> p"
+      using cs(2) unfolding cs(1) cs_def
+      by (simp add: comp_swap swap_commute transpose_comp_triple) 
+    finally have "q \<circ> p \<circ> (inv' q) = p \<circ> p" .
+    moreover have "bij p"
+      unfolding cs(1) cs_def by (simp add: bij_comp)
+    ultimately have p: "q \<circ> p \<circ> (inv' q) \<circ> (inv' p) = p"
+      by (simp add: bijection.intro bijection.inv_comp_right comp_assoc)
 
-      have "swapidseq (Suc (Suc 0)) q"
-        using comp_Suc[OF comp_Suc[OF id], of b c d e] e(1) cs(2)  unfolding q_def cs_def by auto
-      hence "evenperm q"
-        using even_Suc_Suc_iff evenperm_unique by blast
-      moreover have "q permutes { d, e, b, c }"
-        unfolding q_def by (simp add: permutes_compose permutes_swap_id)
-      hence "q permutes {1..n}"
-        using cs(4) d(2) e(2) permutes_subset unfolding cs_def by fastforce
-      ultimately have "q \<in> carrier (alt_group n)"
-        unfolding alt_group_carrier by simp
-      moreover have "p \<in> carrier (alt_group n)"
-        using \<open>p \<in> three_cycles n\<close> three_cycles_incl by blast
-      ultimately have "p \<in> derived_set (alt_group n) (carrier (alt_group n))"
-        using p alt_group_inv_equality unfolding alt_group_mult
-        by (metis (no_types, lifting) UN_iff singletonI)
-      thus "p \<in> derived (alt_group n) (carrier (alt_group n))"
-        unfolding derived_def by (rule incl)
-    qed } note aux_lemma = this
+    have "swapidseq (Suc (Suc 0)) q"
+      using comp_Suc[OF comp_Suc[OF id], of b c d e] e(1) cs(2)  unfolding q_def cs_def by auto
+    hence "evenperm q"
+      using even_Suc_Suc_iff evenperm_unique by blast
+    moreover have "q permutes { d, e, b, c }"
+      unfolding q_def by (simp add: permutes_compose permutes_swap_id)
+    hence "q permutes {1..n}"
+      using cs(4) d(2) e(2) permutes_subset unfolding cs_def by fastforce
+    ultimately have "q \<in> carrier (alt_group n)"
+      unfolding alt_group_carrier by simp
+    moreover have "p \<in> carrier (alt_group n)"
+      using \<open>p \<in> three_cycles n\<close> three_cycles_incl by blast
+    ultimately have "p \<in> derived_set (alt_group n) (carrier (alt_group n))"
+      using p alt_group_inv_equality unfolding alt_group_mult
+      by (metis (no_types, lifting) UN_iff singletonI)
+    thus "p \<in> derived (alt_group n) (carrier (alt_group n))"
+      unfolding derived_def by (rule incl)
+  qed
 
   interpret A: group "alt_group n"
     using alt_group_is_group .
diff -r 8d2d68c8c051 -r 95c9af7483b1 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Nov 13 20:10:34 2024 +0100
@@ -408,20 +408,16 @@
   assumes R1: "p \<in> carrier P" and R2: "q \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p"
 proof (rule up_eqI)
   fix n
-  {
-    fix k and a b :: "nat=>'a"
-    assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
-    then have "k <= n ==>
-      (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
-      (is "_ \<Longrightarrow> ?eq k")
-    proof (induct k)
-      case 0 then show ?case by (simp add: Pi_def)
-    next
-      case (Suc k) then show ?case
-        by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
-    qed
-  }
-  note l = this
+  have l: "(\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))" (is "?eq k")
+    if "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R" and "k <= n"
+    for k and a b :: "nat=>'a"
+  using that
+  proof (induct k)
+    case 0 then show ?case by (simp add: Pi_def)
+  next
+    case (Suc k) then show ?case
+      by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
+  qed
   from R1 R2 show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n =  coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
     unfolding coeff_mult [OF R1 R2, of n]
     unfolding coeff_mult [OF R2 R1, of n]