[STATEMENT]
lemma flatten_set_group:
  assumes group:"group G"
  assumes inj:"inj_on rep (carrier G)"
  shows "group (flatten G rep)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group.group (flatten G rep)
[PROOF STEP]
proof (rule groupI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
 2. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 5. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
 2. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 5. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
assume x:"x \<in> carrier (flatten G rep)" and y:"y \<in> carrier (flatten G rep)"
[PROOF STATE]
proof (state)
this:
x \<in> carrier (flatten G rep)
y \<in> carrier (flatten G rep)

goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
 2. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 5. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
define g h
    where "g = the_inv_into (carrier G) rep x"
      and "h = the_inv_into (carrier G) rep y"
[PROOF STATE]
proof (state)
this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y

goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
 2. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 5. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "x \<otimes>\<^bsub>flatten G rep\<^esub> y = rep (g \<otimes>\<^bsub>G\<^esub> h)"
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y

goal (1 subgoal):
 1. x \<otimes>\<^bsub>flatten G rep\<^esub> y = rep (g \<otimes>\<^bsub>G\<^esub> h)
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y

goal (1 subgoal):
 1. x \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> y = rep (g \<otimes>\<^bsub>G\<^esub> h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y = rep (g \<otimes>\<^bsub>G\<^esub> h)

goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
 2. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 5. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y = rep (g \<otimes>\<^bsub>G\<^esub> h)

goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
 2. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 5. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
from g_def h_def
[PROOF STATE]
proof (chain)
picking this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
[PROOF STEP]
have "g \<in> carrier G" "h \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y

goal (1 subgoal):
 1. g \<in> carrier G &&& h \<in> carrier G
[PROOF STEP]
using inj x y the_inv_into_into
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
inj_on rep (carrier G)
x \<in> carrier (flatten G rep)
y \<in> carrier (flatten G rep)
\<lbrakk>inj_on ?f ?A; ?x \<in> ?f ` ?A; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> the_inv_into ?A ?f ?x \<in> ?B

goal (1 subgoal):
 1. g \<in> carrier G &&& h \<in> carrier G
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
inj_on rep (carrier G)
x \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
y \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
\<lbrakk>inj_on ?f ?A; ?x \<in> ?f ` ?A; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> the_inv_into ?A ?f ?x \<in> ?B

goal (1 subgoal):
 1. g \<in> carrier G &&& h \<in> carrier G
[PROOF STEP]
by (metis partial_object.select_convs(1) subset_refl)+
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
h \<in> carrier G

goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
 2. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 5. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
h \<in> carrier G

goal (1 subgoal):
 1. g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G
[PROOF STEP]
by (metis group group.is_monoid monoid.m_closed)
[PROOF STATE]
proof (state)
this:
g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G

goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
 2. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 5. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "rep (g \<otimes>\<^bsub>G\<^esub> h) \<in> carrier (flatten G rep)"
[PROOF STATE]
proof (prove)
using this:
g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G

goal (1 subgoal):
 1. rep (g \<otimes>\<^bsub>G\<^esub> h) \<in> carrier (flatten G rep)
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G

goal (1 subgoal):
 1. rep (g \<otimes>\<^bsub>G\<^esub> h) \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rep (g \<otimes>\<^bsub>G\<^esub> h) \<in> carrier (flatten G rep)

goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
 2. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 5. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y = rep (g \<otimes>\<^bsub>G\<^esub> h)
rep (g \<otimes>\<^bsub>G\<^esub> h) \<in> carrier (flatten G rep)
[PROOF STEP]
show "x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)"
[PROOF STATE]
proof (prove)
using this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y = rep (g \<otimes>\<^bsub>G\<^esub> h)
rep (g \<otimes>\<^bsub>G\<^esub> h) \<in> carrier (flatten G rep)

goal (1 subgoal):
 1. x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)

goal (4 subgoals):
 1. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 2. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
 2. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 4. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
show "\<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
[PROOF STEP]
by (simp add: group group.is_monoid)
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
fix x y z
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
assume x:"x \<in> carrier (flatten G rep)" and y:"y \<in> carrier (flatten G rep)" and z:"z \<in> carrier (flatten G rep)"
[PROOF STATE]
proof (state)
this:
x \<in> carrier (flatten G rep)
y \<in> carrier (flatten G rep)
z \<in> carrier (flatten G rep)

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
define g h k
    where "g = the_inv_into (carrier G) rep x"
      and "h = the_inv_into (carrier G) rep y"
      and "k = the_inv_into (carrier G) rep z"
[PROOF STATE]
proof (state)
this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
k = the_inv_into (carrier G) rep z

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes> \<^bsub>flatten G rep\<^esub> z"
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
k = the_inv_into (carrier G) rep z

goal (1 subgoal):
 1. x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = rep (g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>flatten G rep\<^esub> z
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
k = the_inv_into (carrier G) rep z

goal (1 subgoal):
 1. x \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> y \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> z = rep (g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = rep (g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>flatten G rep\<^esub> z

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = rep (g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>flatten G rep\<^esub> z

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
have "\<dots> = rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep (g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>flatten G rep\<^esub> z = rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k)
[PROOF STEP]
using k_def
[PROOF STATE]
proof (prove)
using this:
k = the_inv_into (carrier G) rep z

goal (1 subgoal):
 1. rep (g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>flatten G rep\<^esub> z = rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k)
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
k = the_inv_into (carrier G) rep z

goal (1 subgoal):
 1. rep (g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> z = rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rep (g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>flatten G rep\<^esub> z = rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k)

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rep (g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>flatten G rep\<^esub> z = rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k)

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
from g_def h_def k_def
[PROOF STATE]
proof (chain)
picking this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
k = the_inv_into (carrier G) rep z
[PROOF STEP]
have ghkG:"g \<in> carrier G" "h \<in> carrier G" "k \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
k = the_inv_into (carrier G) rep z

goal (1 subgoal):
 1. g \<in> carrier G &&& h \<in> carrier G &&& k \<in> carrier G
[PROOF STEP]
using inj x y z the_inv_into_into
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
k = the_inv_into (carrier G) rep z
inj_on rep (carrier G)
x \<in> carrier (flatten G rep)
y \<in> carrier (flatten G rep)
z \<in> carrier (flatten G rep)
\<lbrakk>inj_on ?f ?A; ?x \<in> ?f ` ?A; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> the_inv_into ?A ?f ?x \<in> ?B

goal (1 subgoal):
 1. g \<in> carrier G &&& h \<in> carrier G &&& k \<in> carrier G
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
h = the_inv_into (carrier G) rep y
k = the_inv_into (carrier G) rep z
inj_on rep (carrier G)
x \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
y \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
z \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
\<lbrakk>inj_on ?f ?A; ?x \<in> ?f ` ?A; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> the_inv_into ?A ?f ?x \<in> ?B

goal (1 subgoal):
 1. g \<in> carrier G &&& h \<in> carrier G &&& k \<in> carrier G
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
h \<in> carrier G
k \<in> carrier G

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence gh:"g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G" and hk:"h \<otimes>\<^bsub>G\<^esub> k \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
h \<in> carrier G
k \<in> carrier G

goal (1 subgoal):
 1. g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G &&& h \<otimes>\<^bsub>G\<^esub> k \<in> carrier G
[PROOF STEP]
by (metis group group.is_monoid monoid.m_closed)+
[PROOF STATE]
proof (state)
this:
g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G
h \<otimes>\<^bsub>G\<^esub> k \<in> carrier G

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k) = rep ((g \<otimes>\<^bsub>G\<^esub> h) \<otimes>\<^bsub>G\<^esub> k)"
[PROOF STATE]
proof (prove)
using this:
g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G
h \<otimes>\<^bsub>G\<^esub> k \<in> carrier G

goal (1 subgoal):
 1. rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k) = rep (g \<otimes>\<^bsub>G\<^esub> h \<otimes>\<^bsub>G\<^esub> k)
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G
h \<otimes>\<^bsub>G\<^esub> k \<in> carrier G

goal (1 subgoal):
 1. rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k) = rep (g \<otimes>\<^bsub>G\<^esub> h \<otimes>\<^bsub>G\<^esub> k)
[PROOF STEP]
using inj the_inv_into_f_f
[PROOF STATE]
proof (prove)
using this:
g \<otimes>\<^bsub>G\<^esub> h \<in> carrier G
h \<otimes>\<^bsub>G\<^esub> k \<in> carrier G
inj_on rep (carrier G)
\<lbrakk>inj_on ?f ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> the_inv_into ?A ?f (?f ?x) = ?x

goal (1 subgoal):
 1. rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k) = rep (g \<otimes>\<^bsub>G\<^esub> h \<otimes>\<^bsub>G\<^esub> k)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k) = rep (g \<otimes>\<^bsub>G\<^esub> h \<otimes>\<^bsub>G\<^esub> k)

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rep (the_inv_into (carrier G) rep (rep (g \<otimes>\<^bsub>G\<^esub> h)) \<otimes>\<^bsub>G\<^esub> k) = rep (g \<otimes>\<^bsub>G\<^esub> h \<otimes>\<^bsub>G\<^esub> k)

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
have "\<dots> = rep (g \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep (g \<otimes>\<^bsub>G\<^esub> h \<otimes>\<^bsub>G\<^esub> k) = rep (g \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k))
[PROOF STEP]
using group group.is_monoid ghkG monoid.m_assoc
[PROOF STATE]
proof (prove)
using this:
Group.group G
Group.group ?G \<Longrightarrow> Group.monoid ?G
g \<in> carrier G
h \<in> carrier G
k \<in> carrier G
\<lbrakk>Group.monoid ?G; ?x \<in> carrier ?G; ?y \<in> carrier ?G; ?z \<in> carrier ?G\<rbrakk> \<Longrightarrow> ?x \<otimes>\<^bsub>?G\<^esub> ?y \<otimes>\<^bsub>?G\<^esub> ?z = ?x \<otimes>\<^bsub>?G\<^esub> (?y \<otimes>\<^bsub>?G\<^esub> ?z)

goal (1 subgoal):
 1. rep (g \<otimes>\<^bsub>G\<^esub> h \<otimes>\<^bsub>G\<^esub> k) = rep (g \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rep (g \<otimes>\<^bsub>G\<^esub> h \<otimes>\<^bsub>G\<^esub> k) = rep (g \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k))

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rep (g \<otimes>\<^bsub>G\<^esub> h \<otimes>\<^bsub>G\<^esub> k) = rep (g \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k))

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
have "\<dots> = x \<otimes>\<^bsub>flatten G rep\<^esub> (rep (h \<otimes>\<^bsub>G\<^esub> k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep (g \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k)) = x \<otimes>\<^bsub>flatten G rep\<^esub> rep (h \<otimes>\<^bsub>G\<^esub> k)
[PROOF STEP]
unfolding g_def flatten_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k)) = x \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> rep (h \<otimes>\<^bsub>G\<^esub> k)
[PROOF STEP]
using hk inj the_inv_into_f_f
[PROOF STATE]
proof (prove)
using this:
h \<otimes>\<^bsub>G\<^esub> k \<in> carrier G
inj_on rep (carrier G)
\<lbrakk>inj_on ?f ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> the_inv_into ?A ?f (?f ?x) = ?x

goal (1 subgoal):
 1. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k)) = x \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> rep (h \<otimes>\<^bsub>G\<^esub> k)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rep (g \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k)) = x \<otimes>\<^bsub>flatten G rep\<^esub> rep (h \<otimes>\<^bsub>G\<^esub> k)

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rep (g \<otimes>\<^bsub>G\<^esub> (h \<otimes>\<^bsub>G\<^esub> k)) = x \<otimes>\<^bsub>flatten G rep\<^esub> rep (h \<otimes>\<^bsub>G\<^esub> k)

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
have "\<dots> = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes>\<^bsub>flatten G rep\<^esub> rep (h \<otimes>\<^bsub>G\<^esub> k) = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
[PROOF STEP]
unfolding h_def k_def flatten_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> rep (the_inv_into (carrier G) rep y \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep z) = x \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> (y \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> z)
[PROOF STEP]
using x y
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier (flatten G rep)
y \<in> carrier (flatten G rep)

goal (1 subgoal):
 1. x \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> rep (the_inv_into (carrier G) rep y \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep z) = x \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> (y \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> z)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x \<otimes>\<^bsub>flatten G rep\<^esub> rep (h \<otimes>\<^bsub>G\<^esub> k) = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)

goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (flatten G rep); y \<in> carrier (flatten G rep); z \<in> carrier (flatten G rep)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 3. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
[PROOF STEP]
show "x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)"
[PROOF STATE]
proof (prove)
using this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)

goal (1 subgoal):
 1. x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
assume x:"x \<in> carrier (flatten G rep)"
[PROOF STATE]
proof (state)
this:
x \<in> carrier (flatten G rep)

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
define g where "g = the_inv_into (carrier G) rep x"
[PROOF STATE]
proof (state)
this:
g = the_inv_into (carrier G) rep x

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence gG:"g \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x

goal (1 subgoal):
 1. g \<in> carrier G
[PROOF STEP]
using inj x
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
inj_on rep (carrier G)
x \<in> carrier (flatten G rep)

goal (1 subgoal):
 1. g \<in> carrier G
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
inj_on rep (carrier G)
x \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>

goal (1 subgoal):
 1. g \<in> carrier G
[PROOF STEP]
using the_inv_into_into
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
inj_on rep (carrier G)
x \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
\<lbrakk>inj_on ?f ?A; ?x \<in> ?f ` ?A; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> the_inv_into ?A ?f ?x \<in> ?B

goal (1 subgoal):
 1. g \<in> carrier G
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
g \<in> carrier G

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
have "\<one>\<^bsub>G\<^esub> \<in> (carrier G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>G\<^esub> \<in> carrier G
[PROOF STEP]
by (simp add: group group.is_monoid)
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>G\<^esub> \<in> carrier G

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "the_inv_into (carrier G) rep (\<one>\<^bsub>flatten G rep\<^esub>) = \<one>\<^bsub>G\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<one>\<^bsub>G\<^esub> \<in> carrier G

goal (1 subgoal):
 1. the_inv_into (carrier G) rep \<one>\<^bsub>flatten G rep\<^esub> = \<one>\<^bsub>G\<^esub>
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
\<one>\<^bsub>G\<^esub> \<in> carrier G

goal (1 subgoal):
 1. the_inv_into (carrier G) rep \<one>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> = \<one>\<^bsub>G\<^esub>
[PROOF STEP]
using the_inv_into_f_f inj
[PROOF STATE]
proof (prove)
using this:
\<one>\<^bsub>G\<^esub> \<in> carrier G
\<lbrakk>inj_on ?f ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> the_inv_into ?A ?f (?f ?x) = ?x
inj_on rep (carrier G)

goal (1 subgoal):
 1. the_inv_into (carrier G) rep \<one>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> = \<one>\<^bsub>G\<^esub>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
the_inv_into (carrier G) rep \<one>\<^bsub>flatten G rep\<^esub> = \<one>\<^bsub>G\<^esub>

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "\<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (\<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> g)"
[PROOF STATE]
proof (prove)
using this:
the_inv_into (carrier G) rep \<one>\<^bsub>flatten G rep\<^esub> = \<one>\<^bsub>G\<^esub>

goal (1 subgoal):
 1. \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (\<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> g)
[PROOF STEP]
unfolding flatten_def g_def
[PROOF STATE]
proof (prove)
using this:
the_inv_into (carrier G) rep \<one>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> = \<one>\<^bsub>G\<^esub>

goal (1 subgoal):
 1. \<one>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> x = rep (\<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (\<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> g)

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (\<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> g)

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
have "\<dots> = rep g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep (\<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> g) = rep g
[PROOF STEP]
using gG group
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
Group.group G

goal (1 subgoal):
 1. rep (\<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> g) = rep g
[PROOF STEP]
by (metis group.is_monoid monoid.l_one)
[PROOF STATE]
proof (state)
this:
rep (\<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> g) = rep g

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rep (\<one>\<^bsub>G\<^esub> \<otimes>\<^bsub>G\<^esub> g) = rep g

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
have "\<dots> = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep g = x
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep (the_inv_into (carrier G) rep x) = x
[PROOF STEP]
using inj x f_the_inv_into_f
[PROOF STATE]
proof (prove)
using this:
inj_on rep (carrier G)
x \<in> carrier (flatten G rep)
\<lbrakk>inj_on ?f ?A; ?y \<in> ?f ` ?A\<rbrakk> \<Longrightarrow> ?f (the_inv_into ?A ?f ?y) = ?y

goal (1 subgoal):
 1. rep (the_inv_into (carrier G) rep x) = x
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
inj_on rep (carrier G)
x \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
\<lbrakk>inj_on ?f ?A; ?y \<in> ?f ` ?A\<rbrakk> \<Longrightarrow> ?f (the_inv_into ?A ?f ?y) = ?y

goal (1 subgoal):
 1. rep (the_inv_into (carrier G) rep x) = x
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
rep g = x

goal (2 subgoals):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
 2. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
[PROOF STEP]
show "\<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x"
[PROOF STATE]
proof (prove)
using this:
\<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x

goal (1 subgoal):
 1. \<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
from group inj
[PROOF STATE]
proof (chain)
picking this:
Group.group G
inj_on rep (carrier G)
[PROOF STEP]
have hom:"rep \<in> hom G (flatten G rep)"
[PROOF STATE]
proof (prove)
using this:
Group.group G
inj_on rep (carrier G)

goal (1 subgoal):
 1. rep \<in> hom G (flatten G rep)
[PROOF STEP]
using flatten_set_group_hom
[PROOF STATE]
proof (prove)
using this:
Group.group G
inj_on rep (carrier G)
\<lbrakk>Group.group ?G; inj_on ?rep (carrier ?G)\<rbrakk> \<Longrightarrow> ?rep \<in> hom ?G (flatten ?G ?rep)

goal (1 subgoal):
 1. rep \<in> hom G (flatten G rep)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rep \<in> hom G (flatten G rep)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
assume x:"x \<in> carrier (flatten G rep)"
[PROOF STATE]
proof (state)
this:
x \<in> carrier (flatten G rep)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
define g where "g = the_inv_into (carrier G) rep x"
[PROOF STATE]
proof (state)
this:
g = the_inv_into (carrier G) rep x

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence gG:"g \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x

goal (1 subgoal):
 1. g \<in> carrier G
[PROOF STEP]
using inj x
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
inj_on rep (carrier G)
x \<in> carrier (flatten G rep)

goal (1 subgoal):
 1. g \<in> carrier G
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
inj_on rep (carrier G)
x \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>

goal (1 subgoal):
 1. g \<in> carrier G
[PROOF STEP]
using the_inv_into_into
[PROOF STATE]
proof (prove)
using this:
g = the_inv_into (carrier G) rep x
inj_on rep (carrier G)
x \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
\<lbrakk>inj_on ?f ?A; ?x \<in> ?f ` ?A; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> the_inv_into ?A ?f ?x \<in> ?B

goal (1 subgoal):
 1. g \<in> carrier G
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
g \<in> carrier G

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence invG:"inv\<^bsub>G\<^esub> g \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G

goal (1 subgoal):
 1. inv\<^bsub>G\<^esub> g \<in> carrier G
[PROOF STEP]
by (metis group group.inv_closed)
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<^esub> g \<in> carrier G

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "rep (inv\<^bsub>G\<^esub> g) \<in> carrier (flatten G rep)"
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G\<^esub> g \<in> carrier G

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<in> carrier (flatten G rep)
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G\<^esub> g \<in> carrier G

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rep (inv\<^bsub>G\<^esub> g) \<in> carrier (flatten G rep)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rep (inv\<^bsub>G\<^esub> g) \<in> carrier (flatten G rep)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
have "rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> (rep g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> rep g
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> the_inv_into (carrier G) rep x) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> the_inv_into (carrier G) rep x) \<otimes>\<^bsub>flatten G rep\<^esub> rep (the_inv_into (carrier G) rep x)
[PROOF STEP]
using f_the_inv_into_f inj x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>inj_on ?f ?A; ?y \<in> ?f ` ?A\<rbrakk> \<Longrightarrow> ?f (the_inv_into ?A ?f ?y) = ?y
inj_on rep (carrier G)
x \<in> carrier (flatten G rep)

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> the_inv_into (carrier G) rep x) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> the_inv_into (carrier G) rep x) \<otimes>\<^bsub>flatten G rep\<^esub> rep (the_inv_into (carrier G) rep x)
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>inj_on ?f ?A; ?y \<in> ?f ` ?A\<rbrakk> \<Longrightarrow> ?f (the_inv_into ?A ?f ?y) = ?y
inj_on rep (carrier G)
x \<in> carrier \<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> the_inv_into (carrier G) rep x) \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> x = rep (inv\<^bsub>G\<^esub> the_inv_into (carrier G) rep x) \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> rep (the_inv_into (carrier G) rep x)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> rep g

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g \<otimes>\<^bsub>G\<^esub> g)"
[PROOF STATE]
proof (prove)
using this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> rep g

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g \<otimes>\<^bsub>G\<^esub> g)
[PROOF STEP]
using hom
[PROOF STATE]
proof (prove)
using this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> rep g
rep \<in> hom G (flatten G rep)

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g \<otimes>\<^bsub>G\<^esub> g)
[PROOF STEP]
unfolding hom_def
[PROOF STATE]
proof (prove)
using this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> rep g
rep \<in> {h \<in> carrier G \<rightarrow> carrier (flatten G rep). \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>flatten G rep\<^esub> h y}

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g \<otimes>\<^bsub>G\<^esub> g)
[PROOF STEP]
using gG invG hom_def
[PROOF STATE]
proof (prove)
using this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> rep g
rep \<in> {h \<in> carrier G \<rightarrow> carrier (flatten G rep). \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>flatten G rep\<^esub> h y}
g \<in> carrier G
inv\<^bsub>G\<^esub> g \<in> carrier G
hom ?G ?H = {h \<in> carrier ?G \<rightarrow> carrier ?H. \<forall>x\<in>carrier ?G. \<forall>y\<in>carrier ?G. h (x \<otimes>\<^bsub>?G\<^esub> y) = h x \<otimes>\<^bsub>?H\<^esub> h y}

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g \<otimes>\<^bsub>G\<^esub> g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g \<otimes>\<^bsub>G\<^esub> g)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep \<one>\<^bsub>G\<^esub>"
[PROOF STATE]
proof (prove)
using this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g \<otimes>\<^bsub>G\<^esub> g)

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep \<one>\<^bsub>G\<^esub>
[PROOF STEP]
using invG gG
[PROOF STATE]
proof (prove)
using this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep (inv\<^bsub>G\<^esub> g \<otimes>\<^bsub>G\<^esub> g)
inv\<^bsub>G\<^esub> g \<in> carrier G
g \<in> carrier G

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep \<one>\<^bsub>G\<^esub>
[PROOF STEP]
by (metis group group.l_inv)
[PROOF STATE]
proof (state)
this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep \<one>\<^bsub>G\<^esub>

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
hence "rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>"
[PROOF STATE]
proof (prove)
using this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = rep \<one>\<^bsub>G\<^esub>

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
using this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> x = rep \<one>\<^bsub>G\<^esub>

goal (1 subgoal):
 1. rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = rep ` carrier G, monoid.mult = \<lambda>x y. rep (the_inv_into (carrier G) rep x \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep y), one = rep \<one>\<^bsub>G\<^esub>\<rparr>\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>

goal (1 subgoal):
 1. \<And>x. x \<in> carrier (flatten G rep) \<Longrightarrow> \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rep (inv\<^bsub>G\<^esub> g) \<in> carrier (flatten G rep)
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
show "\<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>"
[PROOF STATE]
proof (prove)
using this:
rep (inv\<^bsub>G\<^esub> g) \<in> carrier (flatten G rep)
rep (inv\<^bsub>G\<^esub> g) \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>

goal (1 subgoal):
 1. \<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in normal) flatten_set_group_mod_inj:
  shows "inj_on (\<lambda>U. SOME g. g \<in> U) (carrier (G Mod H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>U. SOME g. g \<in> U) (carrier (G Mod H))
[PROOF STEP]
proof (rule inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (G Mod H); y \<in> carrier (G Mod H); (SOME g. g \<in> x) = (SOME g. g \<in> y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix U V
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (G Mod H); y \<in> carrier (G Mod H); (SOME g. g \<in> x) = (SOME g. g \<in> y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume U:"U \<in> carrier (G Mod H)" and V:"V \<in> carrier (G Mod H)"
[PROOF STATE]
proof (state)
this:
U \<in> carrier (G Mod H)
V \<in> carrier (G Mod H)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (G Mod H); y \<in> carrier (G Mod H); (SOME g. g \<in> x) = (SOME g. g \<in> y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U \<in> carrier (G Mod H)
V \<in> carrier (G Mod H)
[PROOF STEP]
obtain g h where g:"U = H #> g" "g \<in> carrier G" and h:"V = H #> h" "h \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier (G Mod H)
V \<in> carrier (G Mod H)

goal (1 subgoal):
 1. (\<And>g h. \<lbrakk>U = H #> g; g \<in> carrier G; V = H #> h; h \<in> carrier G\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding FactGroup_def RCOSETS_def
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier \<lparr>carrier = \<Union>a\<in>carrier G. {H #> a}, monoid.mult = (<#>), one = H\<rparr>
V \<in> carrier \<lparr>carrier = \<Union>a\<in>carrier G. {H #> a}, monoid.mult = (<#>), one = H\<rparr>

goal (1 subgoal):
 1. (\<And>g h. \<lbrakk>U = H #> g; g \<in> carrier G; V = H #> h; h \<in> carrier G\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U = H #> g
g \<in> carrier G
V = H #> h
h \<in> carrier G

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (G Mod H); y \<in> carrier (G Mod H); (SOME g. g \<in> x) = (SOME g. g \<in> y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence notempty:"U \<noteq> {}" "V \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
U = H #> g
g \<in> carrier G
V = H #> h
h \<in> carrier G

goal (1 subgoal):
 1. U \<noteq> {} &&& V \<noteq> {}
[PROOF STEP]
by (metis empty_iff is_subgroup rcos_self)+
[PROOF STATE]
proof (state)
this:
U \<noteq> {}
V \<noteq> {}

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (G Mod H); y \<in> carrier (G Mod H); (SOME g. g \<in> x) = (SOME g. g \<in> y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "(SOME g. g \<in> U) = (SOME g. g \<in> V)"
[PROOF STATE]
proof (state)
this:
(SOME g. g \<in> U) = (SOME g. g \<in> V)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (G Mod H); y \<in> carrier (G Mod H); (SOME g. g \<in> x) = (SOME g. g \<in> y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with notempty
[PROOF STATE]
proof (chain)
picking this:
U \<noteq> {}
V \<noteq> {}
(SOME g. g \<in> U) = (SOME g. g \<in> V)
[PROOF STEP]
have "(SOME g. g \<in> U) \<in> U \<inter> V"
[PROOF STATE]
proof (prove)
using this:
U \<noteq> {}
V \<noteq> {}
(SOME g. g \<in> U) = (SOME g. g \<in> V)

goal (1 subgoal):
 1. (SOME g. g \<in> U) \<in> U \<inter> V
[PROOF STEP]
by (metis IntI ex_in_conv someI)
[PROOF STATE]
proof (state)
this:
(SOME g. g \<in> U) \<in> U \<inter> V

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (G Mod H); y \<in> carrier (G Mod H); (SOME g. g \<in> x) = (SOME g. g \<in> y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
thus "U = V"
[PROOF STATE]
proof (prove)
using this:
(SOME g. g \<in> U) \<in> U \<inter> V

goal (1 subgoal):
 1. U = V
[PROOF STEP]
by (metis Int_iff g h is_subgroup repr_independence)
[PROOF STATE]
proof (state)
this:
U = V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in normal) flatten_set_group_mod:
  shows "group (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group.group (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))
[PROOF STEP]
using factorgroup_is_group flatten_set_group_mod_inj
[PROOF STATE]
proof (prove)
using this:
Group.group (G Mod H)
inj_on (\<lambda>U. SOME g. g \<in> U) (carrier (G Mod H))

goal (1 subgoal):
 1. Group.group (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))
[PROOF STEP]
by (rule flatten_set_group)


[STATEMENT]
lemma (in normal) flatten_set_group_mod_iso:
  shows "(\<lambda>U. SOME g. g \<in> U) \<in> iso (G Mod H) (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>U. SOME g. g \<in> U) \<in> Group.iso (G Mod H) (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))
[PROOF STEP]
unfolding iso_def bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>U. SOME g. g \<in> U) \<in> {h \<in> hom (G Mod H) (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U)). inj_on h (carrier (G Mod H)) \<and> h ` carrier (G Mod H) = carrier (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))}
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<lambda>U. SOME g. g \<in> U) \<in> hom (G Mod H) (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))
 2. inj_on (\<lambda>U. SOME g. g \<in> U) (carrier (G Mod H))
 3. \<And>U. U \<in> carrier (G Mod H) \<Longrightarrow> (SOME g. g \<in> U) \<in> carrier (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))
 4. \<And>x. x \<in> carrier (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U)) \<Longrightarrow> x \<in> (\<lambda>U. SOME g. g \<in> U) ` carrier (G Mod H)
[PROOF STEP]
apply (metis flatten_set_group_mod_inj factorgroup_is_group flatten_set_group_hom)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. inj_on (\<lambda>U. SOME g. g \<in> U) (carrier (G Mod H))
 2. \<And>U. U \<in> carrier (G Mod H) \<Longrightarrow> (SOME g. g \<in> U) \<in> carrier (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))
 3. \<And>x. x \<in> carrier (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U)) \<Longrightarrow> x \<in> (\<lambda>U. SOME g. g \<in> U) ` carrier (G Mod H)
[PROOF STEP]
apply (rule flatten_set_group_mod_inj)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>U. U \<in> carrier (G Mod H) \<Longrightarrow> (SOME g. g \<in> U) \<in> carrier (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))
 2. \<And>x. x \<in> carrier (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U)) \<Longrightarrow> x \<in> (\<lambda>U. SOME g. g \<in> U) ` carrier (G Mod H)
[PROOF STEP]
unfolding flatten_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>U. U \<in> carrier (G Mod H) \<Longrightarrow> (SOME g. g \<in> U) \<in> carrier \<lparr>carrier = (\<lambda>U. SOME g. g \<in> U) ` carrier (G Mod H), monoid.mult = \<lambda>x y. SOME g. g \<in> the_inv_into (carrier (G Mod H)) (\<lambda>U. SOME g. g \<in> U) x \<otimes>\<^bsub>G Mod H\<^esub> the_inv_into (carrier (G Mod H)) (\<lambda>U. SOME g. g \<in> U) y, one = SOME g. g \<in> \<one>\<^bsub>G Mod H\<^esub>\<rparr>
 2. \<And>x. x \<in> carrier \<lparr>carrier = (\<lambda>U. SOME g. g \<in> U) ` carrier (G Mod H), monoid.mult = \<lambda>x y. SOME g. g \<in> the_inv_into (carrier (G Mod H)) (\<lambda>U. SOME g. g \<in> U) x \<otimes>\<^bsub>G Mod H\<^esub> the_inv_into (carrier (G Mod H)) (\<lambda>U. SOME g. g \<in> U) y, one = SOME g. g \<in> \<one>\<^bsub>G Mod H\<^esub>\<rparr> \<Longrightarrow> x \<in> (\<lambda>U. SOME g. g \<in> U) ` carrier (G Mod H)
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rel_nabla_d_closed [simp]:  "rdom (rel_nabla x) = rel_nabla x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom (rel_nabla x) = rel_nabla x
[PROOF STEP]
by (auto simp: rel_nabla_def rel_antidomain_kleene_algebra.fdia_def rel_antidomain_kleene_algebra.ads_d_def rel_ad_def)


[STATEMENT]
lemma rel_nabla_bin_d_closed [simp]:  "rdom (rel_nabla_bin x q) = rel_nabla_bin x q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom (rel_nabla_bin x q) = rel_nabla_bin x q
[PROOF STEP]
by (auto simp: rel_nabla_bin_def rel_antidomain_kleene_algebra.fdia_def rel_antidomain_kleene_algebra.ads_d_def rel_ad_def)


[STATEMENT]
lemma rel_nabla_bin_unfold: "rel_nabla_bin X Q \<subseteq> relfdia X (rel_nabla_bin X Q) \<union> rdom Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> relfdia X (rel_nabla_bin X Q) \<union> rdom Q
[PROOF STEP]
by (simp add: rel_nabla_bin_def rel_ad_def rel_antidomain_kleene_algebra.fdia_def, blast)


[STATEMENT]
lemma rel_nabla_coinduct_var: "P \<subseteq> relfdia X P \<Longrightarrow> P \<subseteq> rel_nabla X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> relfdia X P \<Longrightarrow> P \<subseteq> rel_nabla X
[PROOF STEP]
by (simp add: rel_nabla_def rel_antidomain_kleene_algebra.fdia_def rel_ad_def, blast)


[STATEMENT]
lemma rel_nabla_bin_coinduct: "P \<subseteq> relfdia X P \<union> rdom Q \<Longrightarrow> P \<subseteq> rel_nabla_bin X Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> relfdia X P \<union> rdom Q \<Longrightarrow> P \<subseteq> rel_nabla_bin X Q
[PROOF STEP]
by (simp add: rel_nabla_bin_def rel_antidomain_kleene_algebra.fdia_def rel_ad_def, blast)


[STATEMENT]
lemma nabla_fusion1: "rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> rel_nabla_bin X Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> rel_nabla_bin X Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> rel_nabla_bin X Q
[PROOF STEP]
have "rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> relfdia X (rel_nabla X) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> relfdia X (rel_nabla X) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q
[PROOF STEP]
by (metis (no_types, lifting) Un_mono inf_sup_aci(6) order_refl rel_antidomain_kleene_algebra.dka.fdia_star_unfold_var rel_nabla_unfold sup.commute)
[PROOF STATE]
proof (state)
this:
rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> relfdia X (rel_nabla X) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q

goal (1 subgoal):
 1. rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> rel_nabla_bin X Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> relfdia X (rel_nabla X) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q

goal (1 subgoal):
 1. rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> rel_nabla_bin X Q
[PROOF STEP]
have "... = relfdia X (rel_nabla X \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relfdia X (rel_nabla X) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q = relfdia X (rel_nabla X \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q
[PROOF STEP]
by (simp add: rel_antidomain_kleene_algebra.dka.fdia_add1)
[PROOF STATE]
proof (state)
this:
relfdia X (rel_nabla X) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q = relfdia X (rel_nabla X \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q

goal (1 subgoal):
 1. rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> rel_nabla_bin X Q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> relfdia X (rel_nabla X \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> relfdia X (rel_nabla X \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q

goal (1 subgoal):
 1. rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> rel_nabla_bin X Q
[PROOF STEP]
using rel_nabla_bin_coinduct
[PROOF STATE]
proof (prove)
using this:
rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> relfdia X (rel_nabla X \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q
?P \<subseteq> relfdia ?X ?P \<union> rdom ?Q \<Longrightarrow> ?P \<subseteq> rel_nabla_bin ?X ?Q

goal (1 subgoal):
 1. rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> rel_nabla_bin X Q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_nabla X \<union> relfdia (X\<^sup>*) Q \<subseteq> rel_nabla_bin X Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_ad_inter_seq: "rel_ad X \<inter> rel_ad Y = rel_ad X ; rel_ad Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_ad X \<inter> rel_ad Y = rel_ad X ; rel_ad Y
[PROOF STEP]
by (auto simp: rel_ad_def)


[STATEMENT]
lemma fusion2_aux2: "rdom (rel_nabla_bin X Q) \<subseteq> rdom (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom (rel_nabla_bin X Q) \<subseteq> rdom (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q)
[PROOF STEP]
apply (auto simp: rel_antidomain_kleene_algebra.ads_d_def rel_ad_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> rel_nabla_bin X Q \<Longrightarrow> \<exists>y. y = x \<and> (x, x) \<in> rel_nabla_bin X Q \<and> (\<forall>y. (x, y) \<notin> relfdia (X\<^sup>*) Q) \<or> (x, y) \<in> relfdia (X\<^sup>*) Q
[PROOF STEP]
by (metis pair_in_Id_conv r_into_rtrancl rel_antidomain_kleene_algebra.a_one rel_antidomain_kleene_algebra.a_star rel_antidomain_kleene_algebra.addual.ars_r_def rel_antidomain_kleene_algebra.dka.dns1'' rel_antidomain_kleene_algebra.dpdz.dom_one rel_antidomain_kleene_algebra.ds.ddual.rsr5 rel_antidomain_kleene_algebra.dual.conway.dagger_unfoldr_eq rel_antidomain_kleene_algebra.dual.tc_eq rel_nabla_bin_d_closed)


[STATEMENT]
lemma nabla_fusion2: "rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
have "rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)  \<subseteq> (relfdia X (rel_nabla_bin X Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> (relfdia X (rel_nabla_bin X Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)
[PROOF STEP]
by (meson Int_mono equalityD1 rel_nabla_bin_unfold)
[PROOF STATE]
proof (state)
this:
rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> (relfdia X (rel_nabla_bin X Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> (relfdia X (rel_nabla_bin X Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
have "... \<subseteq> (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (relfdia X (rel_nabla_bin X Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)
[PROOF STEP]
using fusion2_aux2 rel_antidomain_kleene_algebra.dka.fd_iso1
[PROOF STATE]
proof (prove)
using this:
rdom (rel_nabla_bin ?X ?Q) \<subseteq> rdom (rel_nabla_bin ?X ?Q \<inter> rel_ad (relfdia (?X\<^sup>*) ?Q) \<union> relfdia (?X\<^sup>*) ?Q)
rdom ?x \<subseteq> rdom ?y \<Longrightarrow> relfdia ?z ?x \<subseteq> relfdia ?z ?y

goal (1 subgoal):
 1. (relfdia X (rel_nabla_bin X Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(relfdia X (rel_nabla_bin X Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(relfdia X (rel_nabla_bin X Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
have "... = (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) = (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)
[PROOF STEP]
by (simp add: rel_antidomain_kleene_algebra.dka.fdia_add1)
[PROOF STATE]
proof (state)
this:
(relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) = (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<union> relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) = (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
have "... = (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia (X\<^sup>*) Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) = (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia (X\<^sup>*) Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)
[PROOF STEP]
using rel_antidomain_kleene_algebra.dka.fdia_star_unfold_var
[PROOF STATE]
proof (prove)
using this:
rdom ?y \<union> relfdia ?x (relfdia (?x\<^sup>*) ?y) = relfdia (?x\<^sup>*) ?y

goal (1 subgoal):
 1. (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) = (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia (X\<^sup>*) Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia X (relfdia (X\<^sup>*) Q) \<union> rdom Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q) = (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia (X\<^sup>*) Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia (X\<^sup>*) Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)
[PROOF STEP]
have "rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> relfdia X ((rel_nabla_bin X Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q))"
[PROOF STATE]
proof (prove)
using this:
rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> (relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q)) \<union> relfdia (X\<^sup>*) Q) \<inter> rel_ad (relfdia (X\<^sup>*) Q)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q))
[PROOF STEP]
by (metis (no_types, lifting) inf_commute order_trans_rules(23) rel_ad_inter_seq rel_antidomain_kleene_algebra.a_mult_add rel_antidomain_kleene_algebra.a_subid_aux1' rel_antidomain_kleene_algebra.addual.bdia_def rel_antidomain_kleene_algebra.ds.ddual.rsr5)
[PROOF STATE]
proof (state)
this:
rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q))

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
hence "rdom (rel_nabla_bin X Q) ; rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> rdom (rel_nabla X)"
[PROOF STATE]
proof (prove)
using this:
rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> relfdia X (rel_nabla_bin X Q \<inter> rel_ad (relfdia (X\<^sup>*) Q))

goal (1 subgoal):
 1. rdom (rel_nabla_bin X Q) ; rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> rdom (rel_nabla X)
[PROOF STEP]
by (metis rel_ad_inter_seq rel_antidomain_kleene_algebra.addual.ars_r_def rel_nabla_bin_d_closed rel_nabla_coinduct_var rel_nabla_d_closed)
[PROOF STATE]
proof (state)
this:
rdom (rel_nabla_bin X Q) ; rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> rdom (rel_nabla X)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
rdom (rel_nabla_bin X Q) ; rel_ad (relfdia (X\<^sup>*) Q) \<subseteq> rdom (rel_nabla X)

goal (1 subgoal):
 1. rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
by (metis rel_antidomain_kleene_algebra.addual.ars_r_def rel_antidomain_kleene_algebra.addual.bdia_def rel_antidomain_kleene_algebra.d_a_galois1 rel_antidomain_kleene_algebra.dpdz.domain_invol rel_nabla_bin_d_closed rel_nabla_d_closed)
[PROOF STATE]
proof (state)
this:
rel_nabla_bin X Q \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_nabla_coinduct: "P \<subseteq> relfdia X P \<union> rdom Q \<Longrightarrow> P \<subseteq> rel_nabla X \<union> relfdia (rtrancl X) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> relfdia X P \<union> rdom Q \<Longrightarrow> P \<subseteq> rel_nabla X \<union> relfdia (X\<^sup>*) Q
[PROOF STEP]
by (meson nabla_fusion2 order_trans rel_nabla_bin_coinduct)


[STATEMENT]
lemma fdia_arden: "\<nabla>x = 0 \<Longrightarrow> d p \<le> d q + |x\<rangle> p \<Longrightarrow> d p \<le> |x\<^sup>\<star>\<rangle> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d p \<le> d q +  |x\<rangle> p\<rbrakk> \<Longrightarrow> d p \<le>  |x\<^sup>\<star>\<rangle> q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d p \<le> d q +  |x\<rangle> p\<rbrakk> \<Longrightarrow> d p \<le>  |x\<^sup>\<star>\<rangle> q
[PROOF STEP]
assume a1: "\<nabla>x = zero_class.zero"
[PROOF STATE]
proof (state)
this:
\<nabla>x = (zero_class.zero::'a)

goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d p \<le> d q +  |x\<rangle> p\<rbrakk> \<Longrightarrow> d p \<le>  |x\<^sup>\<star>\<rangle> q
[PROOF STEP]
assume "d p \<le> d q + |x\<rangle> p"
[PROOF STATE]
proof (state)
this:
d p \<le> d q +  |x\<rangle> p

goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d p \<le> d q +  |x\<rangle> p\<rbrakk> \<Longrightarrow> d p \<le>  |x\<^sup>\<star>\<rangle> q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d p \<le> d q +  |x\<rangle> p
[PROOF STEP]
have "ad (ad p) \<le> zero_class.zero + ad (ad (x\<^sup>\<star> \<cdot> q))"
[PROOF STATE]
proof (prove)
using this:
d p \<le> d q +  |x\<rangle> p

goal (1 subgoal):
 1. ad (ad p) \<le> (zero_class.zero::'a) + ad (ad (x\<^sup>\<star> \<cdot> q))
[PROOF STEP]
using a1 add_commute ads_d_def dka.fd_def nabla_coinduction
[PROOF STATE]
proof (prove)
using this:
d p \<le> d q +  |x\<rangle> p
\<nabla>x = (zero_class.zero::'a)
?a + ?b = ?b + ?a
d ?x = ad (ad ?x)
 |?x\<rangle> ?y = d (?x \<cdot> ?y)
d ?y \<le>  |?x\<rangle> ?y + d ?z \<Longrightarrow> d ?y \<le> \<nabla>?x +  |?x\<^sup>\<star>\<rangle> ?z

goal (1 subgoal):
 1. ad (ad p) \<le> (zero_class.zero::'a) + ad (ad (x\<^sup>\<star> \<cdot> q))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ad (ad p) \<le> (zero_class.zero::'a) + ad (ad (x\<^sup>\<star> \<cdot> q))

goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d p \<le> d q +  |x\<rangle> p\<rbrakk> \<Longrightarrow> d p \<le>  |x\<^sup>\<star>\<rangle> q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ad (ad p) \<le> (zero_class.zero::'a) + ad (ad (x\<^sup>\<star> \<cdot> q))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ad (ad p) \<le> (zero_class.zero::'a) + ad (ad (x\<^sup>\<star> \<cdot> q))

goal (1 subgoal):
 1. d p \<le>  |x\<^sup>\<star>\<rangle> q
[PROOF STEP]
by (simp add: ads_d_def dka.fd_def)
[PROOF STATE]
proof (state)
this:
d p \<le>  |x\<^sup>\<star>\<rangle> q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fdia_arden_eq: "\<nabla>x = 0 \<Longrightarrow> d p = d q + |x\<rangle> p \<Longrightarrow> d p = |x\<^sup>\<star>\<rangle> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d p = d q +  |x\<rangle> p\<rbrakk> \<Longrightarrow> d p =  |x\<^sup>\<star>\<rangle> q
[PROOF STEP]
by (simp add: fdia_arden dka.fdia_star_induct_eq order.eq_iff)


[STATEMENT]
lemma "|x\<^sup>\<star>] p \<le> |x] p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |x\<^sup>\<star>] p \<le>  |x] p
[PROOF STEP]
by (simp add: fbox_antitone_var)


[STATEMENT]
lemma fbox_arden: "\<nabla>x = 0 \<Longrightarrow> d q \<cdot> |x] p \<le> d p \<Longrightarrow> |x\<^sup>\<star>] q \<le> d p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d q \<cdot>  |x] p \<le> d p\<rbrakk> \<Longrightarrow>  |x\<^sup>\<star>] q \<le> d p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d q \<cdot>  |x] p \<le> d p\<rbrakk> \<Longrightarrow>  |x\<^sup>\<star>] q \<le> d p
[PROOF STEP]
assume h1: "\<nabla>x = 0" and "d q \<cdot> |x] p \<le> d p"
[PROOF STATE]
proof (state)
this:
\<nabla>x = (zero_class.zero::'a)
d q \<cdot>  |x] p \<le> d p

goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d q \<cdot>  |x] p \<le> d p\<rbrakk> \<Longrightarrow>  |x\<^sup>\<star>] q \<le> d p
[PROOF STEP]
hence "ad p \<le> ad (d q \<cdot> |x] p)"
[PROOF STATE]
proof (prove)
using this:
\<nabla>x = (zero_class.zero::'a)
d q \<cdot>  |x] p \<le> d p

goal (1 subgoal):
 1. ad p \<le> ad (d q \<cdot>  |x] p)
[PROOF STEP]
by (metis a_antitone' a_subid addual.ars_r_def dpdz.domain_subid dual_order.trans)
[PROOF STATE]
proof (state)
this:
ad p \<le> ad (d q \<cdot>  |x] p)

goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d q \<cdot>  |x] p \<le> d p\<rbrakk> \<Longrightarrow>  |x\<^sup>\<star>] q \<le> d p
[PROOF STEP]
hence "ad p \<le> ad q + |x\<rangle> ad p"
[PROOF STATE]
proof (prove)
using this:
ad p \<le> ad (d q \<cdot>  |x] p)

goal (1 subgoal):
 1. ad p \<le> ad q +  |x\<rangle> ad p
[PROOF STEP]
by (simp add: a_6 addual.bbox_def ds.fd_def)
[PROOF STATE]
proof (state)
this:
ad p \<le> ad q +  |x\<rangle> ad p

goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d q \<cdot>  |x] p \<le> d p\<rbrakk> \<Longrightarrow>  |x\<^sup>\<star>] q \<le> d p
[PROOF STEP]
hence "ad p \<le> |x\<^sup>\<star>\<rangle> ad q"
[PROOF STATE]
proof (prove)
using this:
ad p \<le> ad q +  |x\<rangle> ad p

goal (1 subgoal):
 1. ad p \<le>  |x\<^sup>\<star>\<rangle> ad q
[PROOF STEP]
by (metis fdia_arden h1 a_4 ads_d_def dpdz.dsg1  fdia_def meet_ord_def)
[PROOF STATE]
proof (state)
this:
ad p \<le>  |x\<^sup>\<star>\<rangle> ad q

goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d q \<cdot>  |x] p \<le> d p\<rbrakk> \<Longrightarrow>  |x\<^sup>\<star>] q \<le> d p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ad p \<le>  |x\<^sup>\<star>\<rangle> ad q

goal (1 subgoal):
 1.  |x\<^sup>\<star>] q \<le> d p
[PROOF STEP]
by (metis a_antitone' ads_d_def fbox_simp fdia_fbox_de_morgan_2)
[PROOF STATE]
proof (state)
this:
 |x\<^sup>\<star>] q \<le> d p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fbox_arden_eq: "\<nabla>x = 0 \<Longrightarrow> d q \<cdot> |x] p = d p \<Longrightarrow> |x\<^sup>\<star>] q = d p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nabla>x = (zero_class.zero::'a); d q \<cdot>  |x] p = d p\<rbrakk> \<Longrightarrow>  |x\<^sup>\<star>] q = d p
[PROOF STEP]
by (simp add: fbox_arden order.antisym fbox_star_induct_eq)