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