Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/Generated_Groups.thy
changeset 81438 95c9af7483b1
parent 73932 fd21b4a93043 
--- 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
isabelle