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