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>