[STATEMENT]
lemma (in normal) factgroup_subgroup_union_normal:
  assumes "A \<lhd> (G Mod H)"
  shows "\<Union>A \<lhd> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> A \<lhd> G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> A \<lhd> G
[PROOF STEP]
have "{x \<in> carrier G. H #> x \<in> A} \<lhd> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier G. H #> x \<in> A} \<lhd> G
[PROOF STEP]
unfolding normal_def normal_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup {x \<in> carrier G. H #> x \<in> A} G \<and> Group.group G \<and> (\<forall>x\<in>carrier G. {x \<in> carrier G. H #> x \<in> A} #> x = x <# {x \<in> carrier G. H #> x \<in> A})
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. subgroup {x \<in> carrier G. H #> x \<in> A} G
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
(*(auto del: equalityI)*)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. subgroup {x \<in> carrier G. H #> x \<in> A} G
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
A \<lhd> G Mod H
[PROOF STEP]
show "subgroup {x \<in> carrier G. H #> x \<in> A} G"
[PROOF STATE]
proof (prove)
using this:
A \<lhd> G Mod H

goal (1 subgoal):
 1. subgroup {x \<in> carrier G. H #> x \<in> A} G
[PROOF STEP]
by (metis (full_types) factgroup_subgroup_union_char factgroup_subgroup_union_subgroup normal_imp_subgroup)
[PROOF STATE]
proof (state)
this:
subgroup {x \<in> carrier G. H #> x \<in> A} G

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
interpret Anormal: normal A "(G Mod H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<lhd> G Mod H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<lhd> G Mod H

goal (1 subgoal):
 1. A \<lhd> G Mod H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
assume x:"x \<in> carrier G" "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
[PROOF STATE]
proof (state)
this:
x \<in> carrier G
y \<in> {x \<in> carrier G. H #> x \<in> A} #> x

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier G
y \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
obtain x' where "x' \<in> {x \<in> carrier G. H #> x \<in> A}" "y = x' \<otimes> x"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
y \<in> {x \<in> carrier G. H #> x \<in> A} #> x

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> {x \<in> carrier G. H #> x \<in> A}; y = x' \<otimes> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding r_coset_def
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
y \<in> (\<Union>h\<in>{x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}. {h \<otimes> x})

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> {x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}; y = x' \<otimes> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> {x \<in> carrier G. H #> x \<in> A}
y = x' \<otimes> x

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence x':"x' \<in> carrier G" "H #> x' \<in> A"
[PROOF STATE]
proof (prove)
using this:
x' \<in> {x \<in> carrier G. H #> x \<in> A}
y = x' \<otimes> x

goal (1 subgoal):
 1. x' \<in> carrier G &&& H #> x' \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> carrier G
H #> x' \<in> A

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
from x(1)
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier G
[PROOF STEP]
have Hx:"H #> x \<in> carrier (G Mod H)"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G

goal (1 subgoal):
 1. H #> x \<in> carrier (G Mod H)
[PROOF STEP]
unfolding FactGroup_def RCOSETS_def
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G

goal (1 subgoal):
 1. H #> x \<in> carrier \<lparr>carrier = \<Union>a\<in>carrier G. {H #> a}, monoid.mult = (<#>), one = H\<rparr>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
H #> x \<in> carrier (G Mod H)

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
with x'
[PROOF STATE]
proof (chain)
picking this:
x' \<in> carrier G
H #> x' \<in> A
H #> x \<in> carrier (G Mod H)
[PROOF STEP]
have "(inv\<^bsub>G Mod H\<^esub> (H #> x)) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
x' \<in> carrier G
H #> x' \<in> A
H #> x \<in> carrier (G Mod H)

goal (1 subgoal):
 1. inv\<^bsub>G Mod H\<^esub> (H #> x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> x) \<in> A
[PROOF STEP]
using Anormal.inv_op_closed1
[PROOF STATE]
proof (prove)
using this:
x' \<in> carrier G
H #> x' \<in> A
H #> x \<in> carrier (G Mod H)
\<lbrakk>?x \<in> carrier (G Mod H); ?h \<in> A\<rbrakk> \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> ?x \<otimes>\<^bsub>G Mod H\<^esub> ?h \<otimes>\<^bsub>G Mod H\<^esub> ?x \<in> A

goal (1 subgoal):
 1. inv\<^bsub>G Mod H\<^esub> (H #> x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> x) \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G Mod H\<^esub> (H #> x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> x) \<in> A

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence "(set_inv (H #> x)) <#> (H #> x') <#> (H #> x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G Mod H\<^esub> (H #> x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> x) \<in> A

goal (1 subgoal):
 1. set_inv (H #> x) <#> (H #> x') <#> (H #> x) \<in> A
[PROOF STEP]
using inv_FactGroup Hx
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G Mod H\<^esub> (H #> x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> x) \<in> A
?X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> ?X = set_inv ?X
H #> x \<in> carrier (G Mod H)

goal (1 subgoal):
 1. set_inv (H #> x) <#> (H #> x') <#> (H #> x) \<in> A
[PROOF STEP]
unfolding FactGroup_def
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub> (H #> x) \<otimes>\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub> (H #> x') \<otimes>\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub> (H #> x) \<in> A
?X \<in> carrier \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr> \<Longrightarrow> inv\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub> ?X = set_inv ?X
H #> x \<in> carrier \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>

goal (1 subgoal):
 1. set_inv (H #> x) <#> (H #> x') <#> (H #> x) \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_inv (H #> x) <#> (H #> x') <#> (H #> x) \<in> A

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence "(H #> (inv x)) <#> (H #> x') <#> (H #> x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
set_inv (H #> x) <#> (H #> x') <#> (H #> x) \<in> A

goal (1 subgoal):
 1. H #> inv x <#> (H #> x') <#> (H #> x) \<in> A
[PROOF STEP]
using x(1)
[PROOF STATE]
proof (prove)
using this:
set_inv (H #> x) <#> (H #> x') <#> (H #> x) \<in> A
x \<in> carrier G

goal (1 subgoal):
 1. H #> inv x <#> (H #> x') <#> (H #> x) \<in> A
[PROOF STEP]
by (metis rcos_inv)
[PROOF STATE]
proof (state)
this:
H #> inv x <#> (H #> x') <#> (H #> x) \<in> A

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence "(H #> (inv x \<otimes> x')) <#> (H #> x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
H #> inv x <#> (H #> x') <#> (H #> x) \<in> A

goal (1 subgoal):
 1. H #> inv x \<otimes> x' <#> (H #> x) \<in> A
[PROOF STEP]
by (metis inv_closed rcos_sum x'(1) x(1))
[PROOF STATE]
proof (state)
this:
H #> inv x \<otimes> x' <#> (H #> x) \<in> A

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence "H #> (inv x \<otimes> x' \<otimes> x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
H #> inv x \<otimes> x' <#> (H #> x) \<in> A

goal (1 subgoal):
 1. H #> inv x \<otimes> x' \<otimes> x \<in> A
[PROOF STEP]
by (metis inv_closed m_closed rcos_sum x'(1) x(1))
[PROOF STATE]
proof (state)
this:
H #> inv x \<otimes> x' \<otimes> x \<in> A

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H #> inv x \<otimes> x' \<otimes> x \<in> A

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
have "inv x \<otimes> x' \<otimes> x \<in> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv x \<otimes> x' \<otimes> x \<in> carrier G
[PROOF STEP]
using x x'
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
y \<in> {x \<in> carrier G. H #> x \<in> A} #> x
x' \<in> carrier G
H #> x' \<in> A

goal (1 subgoal):
 1. inv x \<otimes> x' \<otimes> x \<in> carrier G
[PROOF STEP]
by (metis inv_closed m_closed)
[PROOF STATE]
proof (state)
this:
inv x \<otimes> x' \<otimes> x \<in> carrier G

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
H #> inv x \<otimes> x' \<otimes> x \<in> A
inv x \<otimes> x' \<otimes> x \<in> carrier G
[PROOF STEP]
have "inv x \<otimes> x' \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
using this:
H #> inv x \<otimes> x' \<otimes> x \<in> A
inv x \<otimes> x' \<otimes> x \<in> carrier G

goal (1 subgoal):
 1. inv x \<otimes> x' \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv x \<otimes> x' \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A}

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence xcoset:"x \<otimes> (inv x \<otimes> x' \<otimes> x) \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
using this:
inv x \<otimes> x' \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. x \<otimes> (inv x \<otimes> x' \<otimes> x) \<in> x <# {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
unfolding l_coset_def
[PROOF STATE]
proof (prove)
using this:
inv x \<otimes> x' \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. x \<otimes> (inv x \<otimes> x' \<otimes> x) \<in> (\<Union>h\<in>{x \<in> carrier G. H #> x \<in> A}. {x \<otimes> h})
[PROOF STEP]
using x(1)
[PROOF STATE]
proof (prove)
using this:
inv x \<otimes> x' \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A}
x \<in> carrier G

goal (1 subgoal):
 1. x \<otimes> (inv x \<otimes> x' \<otimes> x) \<in> (\<Union>h\<in>{x \<in> carrier G. H #> x \<in> A}. {x \<otimes> h})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<otimes> (inv x \<otimes> x' \<otimes> x) \<in> x <# {x \<in> carrier G. H #> x \<in> A}

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
have "x \<otimes> (inv x \<otimes> x' \<otimes> x) = (x \<otimes> inv x) \<otimes> x' \<otimes> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes> (inv x \<otimes> x' \<otimes> x) = x \<otimes> inv x \<otimes> x' \<otimes> x
[PROOF STEP]
by (metis Units_eq Units_inv_Units m_assoc m_closed x'(1) x(1))
[PROOF STATE]
proof (state)
this:
x \<otimes> (inv x \<otimes> x' \<otimes> x) = x \<otimes> inv x \<otimes> x' \<otimes> x

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<otimes> (inv x \<otimes> x' \<otimes> x) = x \<otimes> inv x \<otimes> x' \<otimes> x

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
have "\<dots> = x' \<otimes> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes> inv x \<otimes> x' \<otimes> x = x' \<otimes> x
[PROOF STEP]
by (metis l_one r_inv x'(1) x(1))
[PROOF STATE]
proof (state)
this:
x \<otimes> inv x \<otimes> x' \<otimes> x = x' \<otimes> x

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<otimes> inv x \<otimes> x' \<otimes> x = x' \<otimes> x

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
have "\<dots> = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<otimes> x = y
[PROOF STEP]
by (metis \<open>y = x' \<otimes> x\<close>)
[PROOF STATE]
proof (state)
this:
x' \<otimes> x = y

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<otimes> (inv x \<otimes> x' \<otimes> x) = y
[PROOF STEP]
have "x \<otimes> (inv x \<otimes> x' \<otimes> x) = y"
[PROOF STATE]
proof (prove)
using this:
x \<otimes> (inv x \<otimes> x' \<otimes> x) = y

goal (1 subgoal):
 1. x \<otimes> (inv x \<otimes> x' \<otimes> x) = y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<otimes> (inv x \<otimes> x' \<otimes> x) = y

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x\<rbrakk> \<Longrightarrow> xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
with xcoset
[PROOF STATE]
proof (chain)
picking this:
x \<otimes> (inv x \<otimes> x' \<otimes> x) \<in> x <# {x \<in> carrier G. H #> x \<in> A}
x \<otimes> (inv x \<otimes> x' \<otimes> x) = y
[PROOF STEP]
show "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
using this:
x \<otimes> (inv x \<otimes> x' \<otimes> x) \<in> x <# {x \<in> carrier G. H #> x \<in> A}
x \<otimes> (inv x \<otimes> x' \<otimes> x) = y

goal (1 subgoal):
 1. y \<in> x <# {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> x <# {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
interpret Anormal: normal A "(G Mod H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<lhd> G Mod H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<lhd> G Mod H

goal (1 subgoal):
 1. A \<lhd> G Mod H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
assume x:"x \<in> carrier G" "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (state)
this:
x \<in> carrier G
y \<in> x <# {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier G
y \<in> x <# {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
obtain x' where "x' \<in> {x \<in> carrier G. H #> x \<in> A}" "y = x \<otimes> x'"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
y \<in> x <# {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> {x \<in> carrier G. H #> x \<in> A}; y = x \<otimes> x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding l_coset_def
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
y \<in> (\<Union>h\<in>{x \<in> carrier G. H #> x \<in> A}. {x \<otimes> h})

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> {x \<in> carrier G. H #> x \<in> A}; y = x \<otimes> x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> {x \<in> carrier G. H #> x \<in> A}
y = x \<otimes> x'

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence x':"x' \<in> carrier G" "H #> x' \<in> A"
[PROOF STATE]
proof (prove)
using this:
x' \<in> {x \<in> carrier G. H #> x \<in> A}
y = x \<otimes> x'

goal (1 subgoal):
 1. x' \<in> carrier G &&& H #> x' \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> carrier G
H #> x' \<in> A

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
from x(1)
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier G
[PROOF STEP]
have invx:"inv x \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G

goal (1 subgoal):
 1. inv x \<in> carrier G
[PROOF STEP]
by (rule inv_closed)
[PROOF STATE]
proof (state)
this:
inv x \<in> carrier G

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence Hinvx:"H #> (inv x) \<in> carrier (G Mod H)"
[PROOF STATE]
proof (prove)
using this:
inv x \<in> carrier G

goal (1 subgoal):
 1. H #> inv x \<in> carrier (G Mod H)
[PROOF STEP]
unfolding FactGroup_def RCOSETS_def
[PROOF STATE]
proof (prove)
using this:
inv x \<in> carrier G

goal (1 subgoal):
 1. H #> inv x \<in> carrier \<lparr>carrier = \<Union>a\<in>carrier G. {H #> a}, monoid.mult = (<#>), one = H\<rparr>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
H #> inv x \<in> carrier (G Mod H)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
with x'
[PROOF STATE]
proof (chain)
picking this:
x' \<in> carrier G
H #> x' \<in> A
H #> inv x \<in> carrier (G Mod H)
[PROOF STEP]
have "(inv\<^bsub>G Mod H\<^esub> (H #> inv x)) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> inv x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
x' \<in> carrier G
H #> x' \<in> A
H #> inv x \<in> carrier (G Mod H)

goal (1 subgoal):
 1. inv\<^bsub>G Mod H\<^esub> (H #> inv x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> inv x) \<in> A
[PROOF STEP]
using invx Anormal.inv_op_closed1
[PROOF STATE]
proof (prove)
using this:
x' \<in> carrier G
H #> x' \<in> A
H #> inv x \<in> carrier (G Mod H)
inv x \<in> carrier G
\<lbrakk>?x \<in> carrier (G Mod H); ?h \<in> A\<rbrakk> \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> ?x \<otimes>\<^bsub>G Mod H\<^esub> ?h \<otimes>\<^bsub>G Mod H\<^esub> ?x \<in> A

goal (1 subgoal):
 1. inv\<^bsub>G Mod H\<^esub> (H #> inv x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> inv x) \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G Mod H\<^esub> (H #> inv x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> inv x) \<in> A

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence "(set_inv (H #> inv x)) <#> (H #> x') <#> (H #> inv x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G Mod H\<^esub> (H #> inv x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> inv x) \<in> A

goal (1 subgoal):
 1. set_inv (H #> inv x) <#> (H #> x') <#> (H #> inv x) \<in> A
[PROOF STEP]
using inv_FactGroup Hinvx
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G Mod H\<^esub> (H #> inv x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> inv x) \<in> A
?X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> ?X = set_inv ?X
H #> inv x \<in> carrier (G Mod H)

goal (1 subgoal):
 1. set_inv (H #> inv x) <#> (H #> x') <#> (H #> inv x) \<in> A
[PROOF STEP]
unfolding FactGroup_def
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub> (H #> inv x) \<otimes>\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub> (H #> x') \<otimes>\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub> (H #> inv x) \<in> A
?X \<in> carrier \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr> \<Longrightarrow> inv\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub> ?X = set_inv ?X
H #> inv x \<in> carrier \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>

goal (1 subgoal):
 1. set_inv (H #> inv x) <#> (H #> x') <#> (H #> inv x) \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_inv (H #> inv x) <#> (H #> x') <#> (H #> inv x) \<in> A

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence "(H #> inv (inv x)) <#> (H #> x') <#> (H #> inv x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
set_inv (H #> inv x) <#> (H #> x') <#> (H #> inv x) \<in> A

goal (1 subgoal):
 1. H #> inv (inv x) <#> (H #> x') <#> (H #> inv x) \<in> A
[PROOF STEP]
using invx
[PROOF STATE]
proof (prove)
using this:
set_inv (H #> inv x) <#> (H #> x') <#> (H #> inv x) \<in> A
inv x \<in> carrier G

goal (1 subgoal):
 1. H #> inv (inv x) <#> (H #> x') <#> (H #> inv x) \<in> A
[PROOF STEP]
by (metis rcos_inv)
[PROOF STATE]
proof (state)
this:
H #> inv (inv x) <#> (H #> x') <#> (H #> inv x) \<in> A

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence "(H #> x) <#> (H #> x') <#> (H #> inv x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
H #> inv (inv x) <#> (H #> x') <#> (H #> inv x) \<in> A

goal (1 subgoal):
 1. H #> x <#> (H #> x') <#> (H #> inv x) \<in> A
[PROOF STEP]
by (metis inv_inv x(1))
[PROOF STATE]
proof (state)
this:
H #> x <#> (H #> x') <#> (H #> inv x) \<in> A

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence "(H #> (x \<otimes> x')) <#> (H #> inv x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
H #> x <#> (H #> x') <#> (H #> inv x) \<in> A

goal (1 subgoal):
 1. H #> x \<otimes> x' <#> (H #> inv x) \<in> A
[PROOF STEP]
by (metis rcos_sum x'(1) x(1))
[PROOF STATE]
proof (state)
this:
H #> x \<otimes> x' <#> (H #> inv x) \<in> A

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence "H #> (x \<otimes> x' \<otimes> inv x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
H #> x \<otimes> x' <#> (H #> inv x) \<in> A

goal (1 subgoal):
 1. H #> x \<otimes> x' \<otimes> inv x \<in> A
[PROOF STEP]
by (metis inv_closed m_closed rcos_sum x'(1) x(1))
[PROOF STATE]
proof (state)
this:
H #> x \<otimes> x' \<otimes> inv x \<in> A

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H #> x \<otimes> x' \<otimes> inv x \<in> A

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
have "x \<otimes> x' \<otimes> inv x \<in> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes> x' \<otimes> inv x \<in> carrier G
[PROOF STEP]
using x x'
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
y \<in> x <# {x \<in> carrier G. H #> x \<in> A}
x' \<in> carrier G
H #> x' \<in> A

goal (1 subgoal):
 1. x \<otimes> x' \<otimes> inv x \<in> carrier G
[PROOF STEP]
by (metis inv_closed m_closed)
[PROOF STATE]
proof (state)
this:
x \<otimes> x' \<otimes> inv x \<in> carrier G

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
H #> x \<otimes> x' \<otimes> inv x \<in> A
x \<otimes> x' \<otimes> inv x \<in> carrier G
[PROOF STEP]
have "x \<otimes> x' \<otimes> inv x \<in> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
using this:
H #> x \<otimes> x' \<otimes> inv x \<in> A
x \<otimes> x' \<otimes> inv x \<in> carrier G

goal (1 subgoal):
 1. x \<otimes> x' \<otimes> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<otimes> x' \<otimes> inv x \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
hence xcoset:"(x \<otimes> x' \<otimes> inv x) \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
[PROOF STATE]
proof (prove)
using this:
x \<otimes> x' \<otimes> inv x \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. x \<otimes> x' \<otimes> inv x \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
unfolding r_coset_def
[PROOF STATE]
proof (prove)
using this:
x \<otimes> x' \<otimes> inv x \<in> {x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}

goal (1 subgoal):
 1. x \<otimes> x' \<otimes> inv x \<otimes> x \<in> (\<Union>h\<in>{x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}. {h \<otimes> x})
[PROOF STEP]
using invx
[PROOF STATE]
proof (prove)
using this:
x \<otimes> x' \<otimes> inv x \<in> {x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}
inv x \<in> carrier G

goal (1 subgoal):
 1. x \<otimes> x' \<otimes> inv x \<otimes> x \<in> (\<Union>h\<in>{x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}. {h \<otimes> x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<otimes> x' \<otimes> inv x \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A} #> x

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
have "(x \<otimes> x' \<otimes> inv x) \<otimes> x = (x \<otimes> x') \<otimes> (inv x \<otimes> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes> x' \<otimes> inv x \<otimes> x = x \<otimes> x' \<otimes> (inv x \<otimes> x)
[PROOF STEP]
by (metis Units_eq Units_inv_Units m_assoc m_closed x'(1) x(1))
[PROOF STATE]
proof (state)
this:
x \<otimes> x' \<otimes> inv x \<otimes> x = x \<otimes> x' \<otimes> (inv x \<otimes> x)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<otimes> x' \<otimes> inv x \<otimes> x = x \<otimes> x' \<otimes> (inv x \<otimes> x)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
have "\<dots> = x \<otimes> x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes> x' \<otimes> (inv x \<otimes> x) = x \<otimes> x'
[PROOF STEP]
using x(1) l_inv x'(1) m_closed r_one
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
?x \<in> carrier G \<Longrightarrow> inv ?x \<otimes> ?x = \<one>
x' \<in> carrier G
\<lbrakk>?x \<in> carrier G; ?y \<in> carrier G\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<in> carrier G
?x \<in> carrier G \<Longrightarrow> ?x \<otimes> \<one> = ?x

goal (1 subgoal):
 1. x \<otimes> x' \<otimes> (inv x \<otimes> x) = x \<otimes> x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<otimes> x' \<otimes> (inv x \<otimes> x) = x \<otimes> x'

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<otimes> x' \<otimes> (inv x \<otimes> x) = x \<otimes> x'

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
have "\<dots> = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes> x' = y
[PROOF STEP]
by (metis \<open>y = x \<otimes> x'\<close>)
[PROOF STATE]
proof (state)
this:
x \<otimes> x' = y

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<otimes> x' \<otimes> inv x \<otimes> x = y
[PROOF STEP]
have "x \<otimes> x' \<otimes> inv x \<otimes> x = y"
[PROOF STATE]
proof (prove)
using this:
x \<otimes> x' \<otimes> inv x \<otimes> x = y

goal (1 subgoal):
 1. x \<otimes> x' \<otimes> inv x \<otimes> x = y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<otimes> x' \<otimes> inv x \<otimes> x = y

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> carrier G; xa \<in> x <# {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> xa \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
with xcoset
[PROOF STATE]
proof (chain)
picking this:
x \<otimes> x' \<otimes> inv x \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A} #> x
x \<otimes> x' \<otimes> inv x \<otimes> x = y
[PROOF STEP]
show "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
[PROOF STATE]
proof (prove)
using this:
x \<otimes> x' \<otimes> inv x \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A} #> x
x \<otimes> x' \<otimes> inv x \<otimes> x = y

goal (1 subgoal):
 1. y \<in> {x \<in> carrier G. H #> x \<in> A} #> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> {x \<in> carrier G. H #> x \<in> A} #> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{x \<in> carrier G. H #> x \<in> A} \<lhd> G

goal (1 subgoal):
 1. \<Union> A \<lhd> G
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
A \<lhd> G Mod H
{x \<in> carrier G. H #> x \<in> A} \<lhd> G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<lhd> G Mod H
{x \<in> carrier G. H #> x \<in> A} \<lhd> G

goal (1 subgoal):
 1. \<Union> A \<lhd> G
[PROOF STEP]
by (metis (full_types) factgroup_subgroup_union_char normal_imp_subgroup)
[PROOF STATE]
proof (state)
this:
\<Union> A \<lhd> G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in normal) factgroup_subgroup_union_factor:
  assumes "subgroup A (G Mod H)"
  shows "A = rcosets\<^bsub>G\<lparr>carrier := \<Union>A\<rparr>\<^esub> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = rcosets\<^bsub>G\<lparr>carrier := \<Union> A\<rparr>\<^esub> H
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A = rcosets\<^bsub>G\<lparr>carrier := \<Union> A\<rparr>\<^esub> H
[PROOF STEP]
have "A = rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
 2. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
fix U
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
 2. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
assume U:"U \<in> A"
[PROOF STATE]
proof (state)
this:
U \<in> A

goal (2 subgoals):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
 2. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U \<in> A
[PROOF STEP]
obtain x' where x':"x' \<in> carrier G" "U = H #> x'"
[PROOF STATE]
proof (prove)
using this:
U \<in> A

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> carrier G; U = H #> x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms subgroup.subset
[PROOF STATE]
proof (prove)
using this:
U \<in> A
subgroup A (G Mod H)
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

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

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

goal (2 subgoals):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
 2. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
with U
[PROOF STATE]
proof (chain)
picking this:
U \<in> A
x' \<in> carrier G
U = H #> x'
[PROOF STEP]
have "H #> x' \<in> A"
[PROOF STATE]
proof (prove)
using this:
U \<in> A
x' \<in> carrier G
U = H #> x'

goal (1 subgoal):
 1. H #> x' \<in> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
H #> x' \<in> A

goal (2 subgoals):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
 2. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
with x'
[PROOF STATE]
proof (chain)
picking this:
x' \<in> carrier G
U = H #> x'
H #> x' \<in> A
[PROOF STEP]
show "U \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H"
[PROOF STATE]
proof (prove)
using this:
x' \<in> carrier G
U = H #> x'
H #> x' \<in> A

goal (1 subgoal):
 1. U \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
[PROOF STEP]
unfolding RCOSETS_def r_coset_def
[PROOF STATE]
proof (prove)
using this:
x' \<in> carrier G
U = (\<Union>h\<in>H. {h \<otimes> x'})
(\<Union>h\<in>H. {h \<otimes> x'}) \<in> A

goal (1 subgoal):
 1. U \<in> (\<Union>a\<in>carrier (G\<lparr>carrier := {x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}\<rparr>). {\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<lparr>carrier := {x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}\<rparr>\<^esub> a}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H

goal (1 subgoal):
 1. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
fix U
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
assume U:"U \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H"
[PROOF STATE]
proof (state)
this:
U \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H

goal (1 subgoal):
 1. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
[PROOF STEP]
obtain x' where x':"x' \<in> {x \<in> carrier G. H #> x \<in> A}" "U = H #> x'"
[PROOF STATE]
proof (prove)
using this:
U \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> {x \<in> carrier G. H #> x \<in> A}; U = H #> x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding RCOSETS_def r_coset_def
[PROOF STATE]
proof (prove)
using this:
U \<in> (\<Union>a\<in>carrier (G\<lparr>carrier := {x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}\<rparr>). {\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<lparr>carrier := {x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}\<rparr>\<^esub> a}})

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> {x \<in> carrier G. (\<Union>h\<in>H. {h \<otimes> x}) \<in> A}; U = (\<Union>h\<in>H. {h \<otimes> x'})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> {x \<in> carrier G. H #> x \<in> A}
U = H #> x'

goal (1 subgoal):
 1. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
hence "x' \<in> carrier G" "H #> x' \<in> A"
[PROOF STATE]
proof (prove)
using this:
x' \<in> {x \<in> carrier G. H #> x \<in> A}
U = H #> x'

goal (1 subgoal):
 1. x' \<in> carrier G &&& H #> x' \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> carrier G
H #> x' \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H \<Longrightarrow> x \<in> A
[PROOF STEP]
with x'
[PROOF STATE]
proof (chain)
picking this:
x' \<in> {x \<in> carrier G. H #> x \<in> A}
U = H #> x'
x' \<in> carrier G
H #> x' \<in> A
[PROOF STEP]
show "U \<in> A"
[PROOF STATE]
proof (prove)
using this:
x' \<in> {x \<in> carrier G. H #> x \<in> A}
U = H #> x'
x' \<in> carrier G
H #> x' \<in> A

goal (1 subgoal):
 1. U \<in> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
U \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A = rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H

goal (1 subgoal):
 1. A = rcosets\<^bsub>G\<lparr>carrier := \<Union> A\<rparr>\<^esub> H
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
subgroup A (G Mod H)
A = rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
A = rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H

goal (1 subgoal):
 1. A = rcosets\<^bsub>G\<lparr>carrier := \<Union> A\<rparr>\<^esub> H
[PROOF STEP]
using factgroup_subgroup_union_char
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
A = rcosets\<^bsub>G\<lparr>carrier := {x \<in> carrier G. H #> x \<in> A}\<rparr>\<^esub> H
subgroup ?A (G Mod H) \<Longrightarrow> \<Union> ?A = {x \<in> carrier G. H #> x \<in> ?A}

goal (1 subgoal):
 1. A = rcosets\<^bsub>G\<lparr>carrier := \<Union> A\<rparr>\<^esub> H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = rcosets\<^bsub>G\<lparr>carrier := \<Union> A\<rparr>\<^esub> H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma flatten_set_group_hom:
  assumes group:"group G"
  assumes inj:"inj_on rep (carrier G)"
  shows "rep \<in> hom G (flatten G rep)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep \<in> hom G (flatten G rep)
[PROOF STEP]
unfolding hom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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}
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> rep x \<in> carrier (flatten G rep)
 2. \<And>x y. \<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> rep (x \<otimes>\<^bsub>G\<^esub> y) = rep x \<otimes>\<^bsub>flatten G rep\<^esub> rep y
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> rep x \<in> carrier (flatten G rep)
 2. \<And>x y. \<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> rep (x \<otimes>\<^bsub>G\<^esub> y) = rep x \<otimes>\<^bsub>flatten G rep\<^esub> rep y
[PROOF STEP]
assume g:"g \<in> carrier G"
[PROOF STATE]
proof (state)
this:
g \<in> carrier G

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

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

goal (1 subgoal):
 1. rep 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 g \<in> carrier (flatten G rep)

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

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

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

goal (1 subgoal):
 1. rep 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> &&& rep 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 auto
[PROOF STATE]
proof (state)
this:
rep g \<in> carrier (flatten G rep)
rep h \<in> carrier (flatten G rep)

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

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

goal (1 subgoal):
 1. rep 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> rep h = rep (the_inv_into (carrier G) rep (rep g) \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep (rep h))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rep g \<otimes>\<^bsub>flatten G rep\<^esub> rep h = rep (the_inv_into (carrier G) rep (rep g) \<otimes>\<^bsub>G\<^esub> the_inv_into (carrier G) rep (rep h))

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed