[STATEMENT]
lemma Class_cover_imp_subset_or_disj:
  assumes "A = (\<Union> (Class ` C))" and "x \<in> G" and "C \<subseteq> G"
  shows "Class x \<subseteq> A \<or> Class x \<inter> A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Class x \<subseteq> A \<or> Class x \<inter> A = {}
[PROOF STEP]
proof(intro disjCI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Class x \<inter> A \<noteq> {} \<Longrightarrow> Class x \<subseteq> A
[PROOF STEP]
assume "Class x \<inter> A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
Class x \<inter> A \<noteq> {}

goal (1 subgoal):
 1. Class x \<inter> A \<noteq> {} \<Longrightarrow> Class x \<subseteq> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Class x \<inter> A \<noteq> {}
[PROOF STEP]
obtain c where "c \<in> C" and "Class x \<inter> Class c \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
Class x \<inter> A \<noteq> {}

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> C; Class x \<inter> Class c \<noteq> {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Class x \<inter> A \<noteq> {}
A = \<Union> (Class ` C)
x \<in> G
C \<subseteq> G

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> C; Class x \<inter> Class c \<noteq> {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c \<in> C
Class x \<inter> Class c \<noteq> {}

goal (1 subgoal):
 1. Class x \<inter> A \<noteq> {} \<Longrightarrow> Class x \<subseteq> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> C
Class x \<inter> Class c \<noteq> {}
[PROOF STEP]
show "Class x \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
c \<in> C
Class x \<inter> Class c \<noteq> {}

goal (1 subgoal):
 1. Class x \<subseteq> A
[PROOF STEP]
using assms not_disjoint_implies_equal Sup_upper imageI subset_iff
[PROOF STATE]
proof (prove)
using this:
c \<in> C
Class x \<inter> Class c \<noteq> {}
A = \<Union> (Class ` C)
x \<in> G
C \<subseteq> G
\<lbrakk>Class ?a \<inter> Class ?b \<noteq> {}; ?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> Class ?a = Class ?b
?x \<in> ?A \<Longrightarrow> ?x \<le> Sup ?A
?x \<in> ?A \<Longrightarrow> ?f ?x \<in> ?f ` ?A
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)

goal (1 subgoal):
 1. Class x \<subseteq> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Class x \<subseteq> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_is_subgroup: fixes S :: "'a set"
  shows "subgroup (stabilizer S) G (\<oplus>) (\<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (stabilizer S) G (\<oplus>) \<zero>
[PROOF STEP]
proof (intro subgroupI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. stabilizer S \<subseteq> G
 2. \<zero> \<in> stabilizer S
 3. \<And>g h. \<lbrakk>g \<in> stabilizer S; h \<in> stabilizer S\<rbrakk> \<Longrightarrow> g \<oplus> h \<in> stabilizer S
 4. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 5. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
show "stabilizer S \<subseteq> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer S \<subseteq> G
[PROOF STEP]
using stabilizer_def
[PROOF STATE]
proof (prove)
using this:
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. stabilizer S \<subseteq> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stabilizer S \<subseteq> G

goal (4 subgoals):
 1. \<zero> \<in> stabilizer S
 2. \<And>g h. \<lbrakk>g \<in> stabilizer S; h \<in> stabilizer S\<rbrakk> \<Longrightarrow> g \<oplus> h \<in> stabilizer S
 3. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 4. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<zero> \<in> stabilizer S
 2. \<And>g h. \<lbrakk>g \<in> stabilizer S; h \<in> stabilizer S\<rbrakk> \<Longrightarrow> g \<oplus> h \<in> stabilizer S
 3. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 4. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
show "\<zero> \<in> stabilizer S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<in> stabilizer S
[PROOF STEP]
using stabilizer_def
[PROOF STATE]
proof (prove)
using this:
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. \<zero> \<in> stabilizer S
[PROOF STEP]
by (simp add: Int_absorb1 Int_commute)
[PROOF STATE]
proof (state)
this:
\<zero> \<in> stabilizer S

goal (3 subgoals):
 1. \<And>g h. \<lbrakk>g \<in> stabilizer S; h \<in> stabilizer S\<rbrakk> \<Longrightarrow> g \<oplus> h \<in> stabilizer S
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 3. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>g h. \<lbrakk>g \<in> stabilizer S; h \<in> stabilizer S\<rbrakk> \<Longrightarrow> g \<oplus> h \<in> stabilizer S
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 3. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>g h. \<lbrakk>g \<in> stabilizer S; h \<in> stabilizer S\<rbrakk> \<Longrightarrow> g \<oplus> h \<in> stabilizer S
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 3. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
assume haS: "a \<in> stabilizer S" and hbS: "b \<in> stabilizer S"
[PROOF STATE]
proof (state)
this:
a \<in> stabilizer S
b \<in> stabilizer S

goal (3 subgoals):
 1. \<And>g h. \<lbrakk>g \<in> stabilizer S; h \<in> stabilizer S\<rbrakk> \<Longrightarrow> g \<oplus> h \<in> stabilizer S
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 3. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> stabilizer S
b \<in> stabilizer S
[PROOF STEP]
have haG: "a \<in> G" and hbG: "b \<in> G"
[PROOF STATE]
proof (prove)
using this:
a \<in> stabilizer S
b \<in> stabilizer S

goal (1 subgoal):
 1. a \<in> G &&& b \<in> G
[PROOF STEP]
using stabilizer_def
[PROOF STATE]
proof (prove)
using this:
a \<in> stabilizer S
b \<in> stabilizer S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. a \<in> G &&& b \<in> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> G
b \<in> G

goal (3 subgoals):
 1. \<And>g h. \<lbrakk>g \<in> stabilizer S; h \<in> stabilizer S\<rbrakk> \<Longrightarrow> g \<oplus> h \<in> stabilizer S
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 3. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
have "sumset {a \<oplus> b} (S \<inter> G) = sumset {a} (sumset {b} (S \<inter> G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {a \<oplus> b} (S \<inter> G) = sumset {a} (sumset {b} (S \<inter> G))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sumset {a \<oplus> b} (S \<inter> G) \<subseteq> sumset {a} (sumset {b} (S \<inter> G))
 2. sumset {a} (sumset {b} (S \<inter> G)) \<subseteq> sumset {a \<oplus> b} (S \<inter> G)
[PROOF STEP]
show "sumset {a \<oplus> b} (S \<inter> G) \<subseteq> sumset {a} (sumset {b} (S \<inter> G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {a \<oplus> b} (S \<inter> G) \<subseteq> sumset {a} (sumset {b} (S \<inter> G))
[PROOF STEP]
using haG hbG
      empty_subsetI insert_subset subsetI sumset.simps sumset_assoc sumset_mono
[PROOF STATE]
proof (prove)
using this:
a \<in> G
b \<in> G
{} \<subseteq> ?A
(insert ?x ?A \<subseteq> ?B) = (?x \<in> ?B \<and> ?A \<subseteq> ?B)
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B
(?a \<in> sumset ?A ?B) = (\<exists>a b. ?a = a \<oplus> b \<and> a \<in> ?A \<and> a \<in> G \<and> b \<in> ?B \<and> b \<in> G)
sumset (sumset ?A ?B) ?C = sumset ?A (sumset ?B ?C)
\<lbrakk>?A' \<subseteq> ?A; ?B' \<subseteq> ?B\<rbrakk> \<Longrightarrow> sumset ?A' ?B' \<subseteq> sumset ?A ?B

goal (1 subgoal):
 1. sumset {a \<oplus> b} (S \<inter> G) \<subseteq> sumset {a} (sumset {b} (S \<inter> G))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sumset {a \<oplus> b} (S \<inter> G) \<subseteq> sumset {a} (sumset {b} (S \<inter> G))

goal (1 subgoal):
 1. sumset {a} (sumset {b} (S \<inter> G)) \<subseteq> sumset {a \<oplus> b} (S \<inter> G)
[PROOF STEP]
show "sumset {a} (sumset {b} (S \<inter> G)) \<subseteq> sumset {a \<oplus> b} (S \<inter> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {a} (sumset {b} (S \<inter> G)) \<subseteq> sumset {a \<oplus> b} (S \<inter> G)
[PROOF STEP]
using empty_iff insert_iff sumset.simps sumset_assoc
[PROOF STATE]
proof (prove)
using this:
(?c \<in> {}) = False
(?a \<in> insert ?b ?A) = (?a = ?b \<or> ?a \<in> ?A)
(?a \<in> sumset ?A ?B) = (\<exists>a b. ?a = a \<oplus> b \<and> a \<in> ?A \<and> a \<in> G \<and> b \<in> ?B \<and> b \<in> G)
sumset (sumset ?A ?B) ?C = sumset ?A (sumset ?B ?C)

goal (1 subgoal):
 1. sumset {a} (sumset {b} (S \<inter> G)) \<subseteq> sumset {a \<oplus> b} (S \<inter> G)
[PROOF STEP]
by (smt (verit, best) subsetI)
[PROOF STATE]
proof (state)
this:
sumset {a} (sumset {b} (S \<inter> G)) \<subseteq> sumset {a \<oplus> b} (S \<inter> G)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sumset {a \<oplus> b} (S \<inter> G) = sumset {a} (sumset {b} (S \<inter> G))

goal (3 subgoals):
 1. \<And>g h. \<lbrakk>g \<in> stabilizer S; h \<in> stabilizer S\<rbrakk> \<Longrightarrow> g \<oplus> h \<in> stabilizer S
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 3. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sumset {a \<oplus> b} (S \<inter> G) = sumset {a} (sumset {b} (S \<inter> G))
[PROOF STEP]
show "a \<oplus> b \<in> stabilizer S"
[PROOF STATE]
proof (prove)
using this:
sumset {a \<oplus> b} (S \<inter> G) = sumset {a} (sumset {b} (S \<inter> G))

goal (1 subgoal):
 1. a \<oplus> b \<in> stabilizer S
[PROOF STEP]
using haS hbS stabilizer_def
[PROOF STATE]
proof (prove)
using this:
sumset {a \<oplus> b} (S \<inter> G) = sumset {a} (sumset {b} (S \<inter> G))
a \<in> stabilizer S
b \<in> stabilizer S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. a \<oplus> b \<in> stabilizer S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<oplus> b \<in> stabilizer S

goal (2 subgoals):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
assume "g \<in> stabilizer S"
[PROOF STATE]
proof (state)
this:
g \<in> stabilizer S

goal (2 subgoals):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> invertible g
 2. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
thus "invertible g"
[PROOF STATE]
proof (prove)
using this:
g \<in> stabilizer S

goal (1 subgoal):
 1. invertible g
[PROOF STEP]
using stabilizer_def
[PROOF STATE]
proof (prove)
using this:
g \<in> stabilizer S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. invertible g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible g

goal (1 subgoal):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
assume hgS: "g \<in> stabilizer S"
[PROOF STATE]
proof (state)
this:
g \<in> stabilizer S

goal (1 subgoal):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in> stabilizer S
[PROOF STEP]
have hinvsum : "inverse g \<oplus> g = \<zero>"
[PROOF STATE]
proof (prove)
using this:
g \<in> stabilizer S

goal (1 subgoal):
 1. local.inverse g \<oplus> g = \<zero>
[PROOF STEP]
using stabilizer_def
[PROOF STATE]
proof (prove)
using this:
g \<in> stabilizer S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. local.inverse g \<oplus> g = \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.inverse g \<oplus> g = \<zero>

goal (1 subgoal):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
have "sumset {inverse g} (sumset {g}  (S \<inter> G)) =  (S \<inter> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {local.inverse g} (sumset {g} (S \<inter> G)) = S \<inter> G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sumset {local.inverse g} (sumset {g} (S \<inter> G)) \<subseteq> S \<inter> G
 2. S \<inter> G \<subseteq> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
show "sumset {inverse g} (sumset {g} (S \<inter> G)) \<subseteq> (S \<inter> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {local.inverse g} (sumset {g} (S \<inter> G)) \<subseteq> S \<inter> G
[PROOF STEP]
using
      empty_iff insert_iff sumset.simps sumset_assoc subsetI left_unit hinvsum
[PROOF STATE]
proof (prove)
using this:
(?c \<in> {}) = False
(?a \<in> insert ?b ?A) = (?a = ?b \<or> ?a \<in> ?A)
(?a \<in> sumset ?A ?B) = (\<exists>a b. ?a = a \<oplus> b \<and> a \<in> ?A \<and> a \<in> G \<and> b \<in> ?B \<and> b \<in> G)
sumset (sumset ?A ?B) ?C = sumset ?A (sumset ?B ?C)
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B
?a \<in> G \<Longrightarrow> \<zero> \<oplus> ?a = ?a
local.inverse g \<oplus> g = \<zero>

goal (1 subgoal):
 1. sumset {local.inverse g} (sumset {g} (S \<inter> G)) \<subseteq> S \<inter> G
[PROOF STEP]
by (smt (verit, ccfv_threshold))
[PROOF STATE]
proof (state)
this:
sumset {local.inverse g} (sumset {g} (S \<inter> G)) \<subseteq> S \<inter> G

goal (1 subgoal):
 1. S \<inter> G \<subseteq> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
show "(S \<inter> G) \<subseteq> sumset {inverse g} (sumset {g} (S \<inter> G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> G \<subseteq> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<inter> G \<Longrightarrow> x \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<inter> G \<Longrightarrow> x \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
assume hs: "s \<in> (S \<inter> G)"
[PROOF STATE]
proof (state)
this:
s \<in> S \<inter> G

goal (1 subgoal):
 1. \<And>x. x \<in> S \<inter> G \<Longrightarrow> x \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S \<inter> G
[PROOF STEP]
have "inverse g \<oplus> g \<oplus> s \<in> sumset {inverse g} (sumset {g} (S \<inter> G))"
[PROOF STATE]
proof (prove)
using this:
s \<in> S \<inter> G

goal (1 subgoal):
 1. local.inverse g \<oplus> g \<oplus> s \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
using
        hgS stabilizer_def additive_abelian_group.sumset.sumsetI
        additive_abelian_group_axioms associative in_mono inverse_closed mem_Collect_eq singletonI
[PROOF STATE]
proof (prove)
using this:
s \<in> S \<inter> G
g \<in> stabilizer S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}
\<lbrakk>additive_abelian_group ?G ?addition ?zero; ?a \<in> ?A; ?a \<in> ?G; ?b \<in> ?B; ?b \<in> ?G\<rbrakk> \<Longrightarrow> ?addition ?a ?b \<in> additive_abelian_group.sumset ?G ?addition ?A ?B
additive_abelian_group G (\<oplus>) \<zero>
\<lbrakk>?a \<in> G; ?b \<in> G; ?c \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<oplus> ?c = ?a \<oplus> (?b \<oplus> ?c)
?A \<subseteq> ?B \<Longrightarrow> ?x \<in> ?A \<longrightarrow> ?x \<in> ?B
?x \<in> G \<Longrightarrow> local.inverse ?x \<in> G
(?a \<in> Collect ?P) = ?P ?a
?a \<in> {?a}

goal (1 subgoal):
 1. local.inverse g \<oplus> g \<oplus> s \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
by (smt (z3) IntD2)
[PROOF STATE]
proof (state)
this:
local.inverse g \<oplus> g \<oplus> s \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))

goal (1 subgoal):
 1. \<And>x. x \<in> S \<inter> G \<Longrightarrow> x \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
thus "s \<in> sumset {inverse g} (sumset {g} (S \<inter> G))"
[PROOF STATE]
proof (prove)
using this:
local.inverse g \<oplus> g \<oplus> s \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))

goal (1 subgoal):
 1. s \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
using hinvsum hs
[PROOF STATE]
proof (prove)
using this:
local.inverse g \<oplus> g \<oplus> s \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))
local.inverse g \<oplus> g = \<zero>
s \<in> S \<inter> G

goal (1 subgoal):
 1. s \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in> sumset {local.inverse g} (sumset {g} (S \<inter> G))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<inter> G \<subseteq> sumset {local.inverse g} (sumset {g} (S \<inter> G))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sumset {local.inverse g} (sumset {g} (S \<inter> G)) = S \<inter> G

goal (1 subgoal):
 1. \<And>g. g \<in> stabilizer S \<Longrightarrow> local.inverse g \<in> stabilizer S
[PROOF STEP]
thus "inverse g \<in> stabilizer S"
[PROOF STATE]
proof (prove)
using this:
sumset {local.inverse g} (sumset {g} (S \<inter> G)) = S \<inter> G

goal (1 subgoal):
 1. local.inverse g \<in> stabilizer S
[PROOF STEP]
using hgS stabilizer_def
[PROOF STATE]
proof (prove)
using this:
sumset {local.inverse g} (sumset {g} (S \<inter> G)) = S \<inter> G
g \<in> stabilizer S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. local.inverse g \<in> stabilizer S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.inverse g \<in> stabilizer S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zero_mem_stabilizer: "\<zero> \<in> stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<in> stabilizer A
[PROOF STEP]
..


[STATEMENT]
lemma stabilizer_is_nonempty:
  shows "stabilizer S \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer S \<noteq> {}
[PROOF STEP]
using sub_unit_closed
[PROOF STATE]
proof (prove)
using this:
\<zero> \<in> stabilizer ?A

goal (1 subgoal):
 1. stabilizer S \<noteq> {}
[PROOF STEP]
by blast


[STATEMENT]
lemma Left_Coset_eq_sumset_stabilizer:
  assumes "x \<in> G"
  shows "sumset {x} (stabilizer B) = x \<cdot>| (stabilizer B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} (stabilizer B) = x \<cdot>| stabilizer B
[PROOF STEP]
by (simp add: Left_Coset_eq_sumset assms)


[STATEMENT]
lemma stabilizer_subset_difference_singleton:
  assumes "S \<subseteq> G" and "s \<in> S"
  shows "stabilizer S \<subseteq> differenceset S {s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer S \<subseteq> differenceset S {s}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S {s}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S {s}
[PROOF STEP]
assume hx: "x \<in> stabilizer S"
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer S

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S {s}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> stabilizer S
[PROOF STEP]
obtain t where ht: "t \<in> S" and "x \<oplus> s = t"
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer S

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> S; x \<oplus> s = t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms stabilizer_def
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer S
S \<subseteq> G
s \<in> S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> S; x \<oplus> s = t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> S
x \<oplus> s = t

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S {s}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> S
x \<oplus> s = t
[PROOF STEP]
have "x = t \<ominus> s"
[PROOF STATE]
proof (prove)
using this:
t \<in> S
x \<oplus> s = t

goal (1 subgoal):
 1. x = t \<ominus> s
[PROOF STEP]
using hx stabilizer_def assms associative
[PROOF STATE]
proof (prove)
using this:
t \<in> S
x \<oplus> s = t
x \<in> stabilizer S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}
S \<subseteq> G
s \<in> S
\<lbrakk>?a \<in> G; ?b \<in> G; ?c \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<oplus> ?c = ?a \<oplus> (?b \<oplus> ?c)

goal (1 subgoal):
 1. x = t \<ominus> s
[PROOF STEP]
by (metis (no_types, lifting) in_mono inverse_closed invertible invertible_right_inverse sub
      sub.right_unit)
[PROOF STATE]
proof (state)
this:
x = t \<ominus> s

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S {s}
[PROOF STEP]
thus "x \<in> differenceset S {s}"
[PROOF STATE]
proof (prove)
using this:
x = t \<ominus> s

goal (1 subgoal):
 1. x \<in> differenceset S {s}
[PROOF STEP]
using ht assms
[PROOF STATE]
proof (prove)
using this:
x = t \<ominus> s
t \<in> S
S \<subseteq> G
s \<in> S

goal (1 subgoal):
 1. x \<in> differenceset S {s}
[PROOF STEP]
by (simp add: minusset.minussetI subsetD sumset.sumsetI)
[PROOF STATE]
proof (state)
this:
x \<in> differenceset S {s}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_subset_singleton_difference:
  assumes "S \<subseteq> G" and "s \<in> S"
  shows "stabilizer S \<subseteq> differenceset {s} S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer S \<subseteq> differenceset {s} S
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabilizer S \<subseteq> differenceset {s} S
[PROOF STEP]
have "stabilizer S \<subseteq> minusset (stabilizer S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer S \<subseteq> minusset (stabilizer S)
[PROOF STEP]
using assms Int_absorb2 minusset_eq
    subgroup.image_of_inverse submonoid.sub subset_eq
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> G
s \<in> S
?A \<subseteq> ?B \<Longrightarrow> ?A \<inter> ?B = ?A
minusset ?A = local.inverse ` (?A \<inter> G)
\<lbrakk>subgroup ?G ?M ?composition ?unit; ?x \<in> ?G\<rbrakk> \<Longrightarrow> ?x \<in> monoid.inverse ?M ?composition ?unit ` ?G
\<lbrakk>submonoid ?N ?M ?composition ?unit; ?a \<in> ?N\<rbrakk> \<Longrightarrow> ?a \<in> ?M
(?A \<subseteq> ?B) = (\<forall>x\<in>?A. x \<in> ?B)

goal (1 subgoal):
 1. stabilizer S \<subseteq> minusset (stabilizer S)
[PROOF STEP]
by (smt (verit) stabilizer_is_subgroup stabilizer_subset_difference_singleton
      sumset_subset_carrier)
[PROOF STATE]
proof (state)
this:
stabilizer S \<subseteq> minusset (stabilizer S)

goal (1 subgoal):
 1. stabilizer S \<subseteq> differenceset {s} S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stabilizer S \<subseteq> minusset (stabilizer S)

goal (1 subgoal):
 1. stabilizer S \<subseteq> differenceset {s} S
[PROOF STEP]
have "minusset (stabilizer S) \<subseteq> minusset (differenceset S {s})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minusset (stabilizer S) \<subseteq> minusset (differenceset S {s})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> minusset (stabilizer S) \<Longrightarrow> x \<in> minusset (differenceset S {s})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> minusset (stabilizer S) \<Longrightarrow> x \<in> minusset (differenceset S {s})
[PROOF STEP]
assume hx1: "x \<in> minusset (stabilizer S)"
[PROOF STATE]
proof (state)
this:
x \<in> minusset (stabilizer S)

goal (1 subgoal):
 1. \<And>x. x \<in> minusset (stabilizer S) \<Longrightarrow> x \<in> minusset (differenceset S {s})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> minusset (stabilizer S)
[PROOF STEP]
have hx: "inverse x \<in> stabilizer S"
[PROOF STATE]
proof (prove)
using this:
x \<in> minusset (stabilizer S)

goal (1 subgoal):
 1. local.inverse x \<in> stabilizer S
[PROOF STEP]
by (metis invertible invertible_inverse_inverse minusset.cases)
[PROOF STATE]
proof (state)
this:
local.inverse x \<in> stabilizer S

goal (1 subgoal):
 1. \<And>x. x \<in> minusset (stabilizer S) \<Longrightarrow> x \<in> minusset (differenceset S {s})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.inverse x \<in> stabilizer S
[PROOF STEP]
obtain t where ht: "t \<in> S" and "inverse x \<oplus> s = t"
[PROOF STATE]
proof (prove)
using this:
local.inverse x \<in> stabilizer S

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> S; local.inverse x \<oplus> s = t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms stabilizer_def
[PROOF STATE]
proof (prove)
using this:
local.inverse x \<in> stabilizer S
S \<subseteq> G
s \<in> S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> S; local.inverse x \<oplus> s = t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> S
local.inverse x \<oplus> s = t

goal (1 subgoal):
 1. \<And>x. x \<in> minusset (stabilizer S) \<Longrightarrow> x \<in> minusset (differenceset S {s})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> S
local.inverse x \<oplus> s = t
[PROOF STEP]
have hx2: "inverse x = t \<ominus> s"
[PROOF STATE]
proof (prove)
using this:
t \<in> S
local.inverse x \<oplus> s = t

goal (1 subgoal):
 1. local.inverse x = t \<ominus> s
[PROOF STEP]
using hx stabilizer_def assms
[PROOF STATE]
proof (prove)
using this:
t \<in> S
local.inverse x \<oplus> s = t
local.inverse x \<in> stabilizer S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}
S \<subseteq> G
s \<in> S

goal (1 subgoal):
 1. local.inverse x = t \<ominus> s
[PROOF STEP]
by (smt (verit, ccfv_threshold) commutative in_mono inverse_closed invertible
        invertible_left_inverse2 sub)
[PROOF STATE]
proof (state)
this:
local.inverse x = t \<ominus> s

goal (1 subgoal):
 1. \<And>x. x \<in> minusset (stabilizer S) \<Longrightarrow> x \<in> minusset (differenceset S {s})
[PROOF STEP]
thus "x \<in> minusset (differenceset S {s})"
[PROOF STATE]
proof (prove)
using this:
local.inverse x = t \<ominus> s

goal (1 subgoal):
 1. x \<in> minusset (differenceset S {s})
[PROOF STEP]
using ht assms
[PROOF STATE]
proof (prove)
using this:
local.inverse x = t \<ominus> s
t \<in> S
S \<subseteq> G
s \<in> S

goal (1 subgoal):
 1. x \<in> minusset (differenceset S {s})
[PROOF STEP]
by (smt (verit, best) hx1 additive_abelian_group.sumset.sumsetI additive_abelian_group_axioms
        inverse_closed invertible invertible_inverse_inverse minusset.cases minusset.minussetI
        singletonI subset_iff)
[PROOF STATE]
proof (state)
this:
x \<in> minusset (differenceset S {s})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
minusset (stabilizer S) \<subseteq> minusset (differenceset S {s})

goal (1 subgoal):
 1. stabilizer S \<subseteq> differenceset {s} S
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stabilizer S \<subseteq> minusset (stabilizer S)
minusset (stabilizer S) \<subseteq> minusset (differenceset S {s})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stabilizer S \<subseteq> minusset (stabilizer S)
minusset (stabilizer S) \<subseteq> minusset (differenceset S {s})

goal (1 subgoal):
 1. stabilizer S \<subseteq> differenceset {s} S
[PROOF STEP]
using differenceset_commute assms
[PROOF STATE]
proof (prove)
using this:
stabilizer S \<subseteq> minusset (stabilizer S)
minusset (stabilizer S) \<subseteq> minusset (differenceset S {s})
minusset (differenceset ?B ?A) = differenceset ?A ?B
S \<subseteq> G
s \<in> S

goal (1 subgoal):
 1. stabilizer S \<subseteq> differenceset {s} S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
stabilizer S \<subseteq> differenceset {s} S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_subset_nempty:
  assumes "S \<noteq> {}" and "S \<subseteq> G"
  shows "stabilizer S \<subseteq> differenceset S S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer S \<subseteq> differenceset S S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S S
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S S
[PROOF STEP]
assume hx: "x \<in> stabilizer S"
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer S

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> stabilizer S
[PROOF STEP]
obtain s where hs: "s \<in> S \<inter> G"
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer S

goal (1 subgoal):
 1. (\<And>s. s \<in> S \<inter> G \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer S
S \<noteq> {}
S \<subseteq> G

goal (1 subgoal):
 1. (\<And>s. s \<in> S \<inter> G \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s \<in> S \<inter> G

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S \<inter> G
[PROOF STEP]
have "x \<oplus> s \<in> S \<inter> G"
[PROOF STATE]
proof (prove)
using this:
s \<in> S \<inter> G

goal (1 subgoal):
 1. x \<oplus> s \<in> S \<inter> G
[PROOF STEP]
using stabilizer_def assms hx mem_Collect_eq singletonI
    sumset.sumsetI sumset_Int_carrier
[PROOF STATE]
proof (prove)
using this:
s \<in> S \<inter> G
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}
S \<noteq> {}
S \<subseteq> G
x \<in> stabilizer S
(?a \<in> Collect ?P) = ?P ?a
?a \<in> {?a}
\<lbrakk>?a \<in> ?A; ?a \<in> G; ?b \<in> ?B; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> sumset ?A ?B
sumset ?A ?B \<inter> G = sumset ?A ?B

goal (1 subgoal):
 1. x \<oplus> s \<in> S \<inter> G
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<oplus> s \<in> S \<inter> G

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<oplus> s \<in> S \<inter> G
[PROOF STEP]
obtain t where ht: "t \<in> S" and "x \<oplus> s = t"
[PROOF STATE]
proof (prove)
using this:
x \<oplus> s \<in> S \<inter> G

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> S; x \<oplus> s = t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> S
x \<oplus> s = t

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> S
x \<oplus> s = t
[PROOF STEP]
have "x = t \<ominus> s"
[PROOF STATE]
proof (prove)
using this:
t \<in> S
x \<oplus> s = t

goal (1 subgoal):
 1. x = t \<ominus> s
[PROOF STEP]
using hx stabilizer_def assms(2) hs ht associative
[PROOF STATE]
proof (prove)
using this:
t \<in> S
x \<oplus> s = t
x \<in> stabilizer S
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}
S \<subseteq> G
s \<in> S \<inter> G
t \<in> S
\<lbrakk>?a \<in> G; ?b \<in> G; ?c \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<oplus> ?c = ?a \<oplus> (?b \<oplus> ?c)

goal (1 subgoal):
 1. x = t \<ominus> s
[PROOF STEP]
by (metis IntD2 inverse_closed invertible invertible_right_inverse sub sub.right_unit)
[PROOF STATE]
proof (state)
this:
x = t \<ominus> s

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer S \<Longrightarrow> x \<in> differenceset S S
[PROOF STEP]
thus "x \<in> differenceset S S"
[PROOF STATE]
proof (prove)
using this:
x = t \<ominus> s

goal (1 subgoal):
 1. x \<in> differenceset S S
[PROOF STEP]
using ht hs
[PROOF STATE]
proof (prove)
using this:
x = t \<ominus> s
t \<in> S
s \<in> S \<inter> G

goal (1 subgoal):
 1. x \<in> differenceset S S
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
x = t \<ominus> s
t \<in> S
s \<in> S \<inter> G
S \<subseteq> G

goal (1 subgoal):
 1. x \<in> differenceset S S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> differenceset S S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_coset_subset:
  assumes "A \<subseteq> G" and "x \<in> A"
  shows "sumset {x} (stabilizer A) \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} (stabilizer A) \<subseteq> A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (stabilizer A) \<Longrightarrow> xa \<in> A
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (stabilizer A) \<Longrightarrow> xa \<in> A
[PROOF STEP]
assume "y \<in> sumset {x} (stabilizer A)"
[PROOF STATE]
proof (state)
this:
y \<in> sumset {x} (stabilizer A)

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (stabilizer A) \<Longrightarrow> xa \<in> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> sumset {x} (stabilizer A)

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (stabilizer A) \<Longrightarrow> xa \<in> A
[PROOF STEP]
hence "stabilizer A \<subseteq> differenceset A {x}"
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {x} (stabilizer A)

goal (1 subgoal):
 1. stabilizer A \<subseteq> differenceset A {x}
[PROOF STEP]
using assms
      stabilizer_subset_difference_singleton
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {x} (stabilizer A)
A \<subseteq> G
x \<in> A
\<lbrakk>?S \<subseteq> G; ?s \<in> ?S\<rbrakk> \<Longrightarrow> stabilizer ?S \<subseteq> differenceset ?S {?s}

goal (1 subgoal):
 1. stabilizer A \<subseteq> differenceset A {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stabilizer A \<subseteq> differenceset A {x}

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (stabilizer A) \<Longrightarrow> xa \<in> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stabilizer A \<subseteq> differenceset A {x}

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (stabilizer A) \<Longrightarrow> xa \<in> A
[PROOF STEP]
have "sumset {x} (differenceset A {x}) \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} (differenceset A {x}) \<subseteq> A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (differenceset A {x}) \<Longrightarrow> xa \<in> A
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (differenceset A {x}) \<Longrightarrow> xa \<in> A
[PROOF STEP]
assume "z \<in> sumset {x} (differenceset A {x})"
[PROOF STATE]
proof (state)
this:
z \<in> sumset {x} (differenceset A {x})

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (differenceset A {x}) \<Longrightarrow> xa \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> sumset {x} (differenceset A {x})
[PROOF STEP]
obtain a where "a \<in> A" and "z = x \<oplus> (a \<ominus> x)"
[PROOF STATE]
proof (prove)
using this:
z \<in> sumset {x} (differenceset A {x})

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; z = x \<oplus> a \<ominus> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using additive_abelian_group.sumset.cases additive_abelian_group_axioms singletonD
        minusset.cases assms subsetD
[PROOF STATE]
proof (prove)
using this:
z \<in> sumset {x} (differenceset A {x})
\<lbrakk>additive_abelian_group ?G ?addition ?zero; ?a \<in> additive_abelian_group.sumset ?G ?addition ?A ?B; \<And>a b. \<lbrakk>?a = ?addition a b; a \<in> ?A; a \<in> ?G; b \<in> ?B; b \<in> ?G\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
additive_abelian_group G (\<oplus>) \<zero>
?b \<in> {?a} \<Longrightarrow> ?b = ?a
\<lbrakk>?a \<in> minusset ?A; \<And>a. \<lbrakk>?a = local.inverse a; a \<in> ?A; a \<in> G\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
A \<subseteq> G
x \<in> A
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; z = x \<oplus> a \<ominus> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (smt (verit, ccfv_SIG))
[PROOF STATE]
proof (state)
this:
a \<in> A
z = x \<oplus> a \<ominus> x

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (differenceset A {x}) \<Longrightarrow> xa \<in> A
[PROOF STEP]
thus "z \<in> A"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
z = x \<oplus> a \<ominus> x

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> A
z = x \<oplus> a \<ominus> x
A \<subseteq> G
x \<in> A

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
by (metis additive_abelian_group.inverse_closed additive_abelian_group_axioms
          commutative in_mono invertible invertible_right_inverse2)
[PROOF STATE]
proof (state)
this:
z \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sumset {x} (differenceset A {x}) \<subseteq> A

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} (stabilizer A) \<Longrightarrow> xa \<in> A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> sumset {x} (stabilizer A)
stabilizer A \<subseteq> differenceset A {x}
sumset {x} (differenceset A {x}) \<subseteq> A
[PROOF STEP]
show "y \<in> A"
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {x} (stabilizer A)
stabilizer A \<subseteq> differenceset A {x}
sumset {x} (differenceset A {x}) \<subseteq> A

goal (1 subgoal):
 1. y \<in> A
[PROOF STEP]
by (meson in_mono subset_singleton_iff sumset_mono)
[PROOF STATE]
proof (state)
this:
y \<in> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_subset_stabilizer_dvd:
  assumes "stabilizer A \<subseteq> stabilizer B"
  shows "card (stabilizer A) dvd card (stabilizer B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
proof(cases "finite (stabilizer B)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (stabilizer B) \<Longrightarrow> card (stabilizer A) dvd card (stabilizer B)
 2. infinite (stabilizer B) \<Longrightarrow> card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
case hB: True
[PROOF STATE]
proof (state)
this:
finite (stabilizer B)

goal (2 subgoals):
 1. finite (stabilizer B) \<Longrightarrow> card (stabilizer A) dvd card (stabilizer B)
 2. infinite (stabilizer B) \<Longrightarrow> card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
interpret H: subgroup_of_group "stabilizer A" "stabilizer B" "(\<oplus>)" "\<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup_of_group (stabilizer A) (stabilizer B) (\<oplus>) \<zero>
[PROOF STEP]
proof(unfold_locales)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. stabilizer A \<subseteq> stabilizer B
 2. \<And>a b. \<lbrakk>a \<in> stabilizer A; b \<in> stabilizer A\<rbrakk> \<Longrightarrow> a \<oplus> b \<in> stabilizer A
 3. \<zero> \<in> stabilizer A
[PROOF STEP]
show "stabilizer A \<subseteq> stabilizer B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stabilizer A \<subseteq> stabilizer B

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
stabilizer A \<subseteq> stabilizer B

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> stabilizer A; b \<in> stabilizer A\<rbrakk> \<Longrightarrow> a \<oplus> b \<in> stabilizer A
 2. \<zero> \<in> stabilizer A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> stabilizer A; b \<in> stabilizer A\<rbrakk> \<Longrightarrow> a \<oplus> b \<in> stabilizer A
 2. \<zero> \<in> stabilizer A
[PROOF STEP]
show "\<And>a b. a \<in> stabilizer A \<Longrightarrow> b \<in> stabilizer A \<Longrightarrow> a \<oplus> b \<in> stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> stabilizer A; b \<in> stabilizer A\<rbrakk> \<Longrightarrow> a \<oplus> b \<in> stabilizer A
[PROOF STEP]
using stabilizer_is_subgroup group_axioms
[PROOF STATE]
proof (prove)
using this:
subgroup (stabilizer ?S) G (\<oplus>) \<zero>
Group_Theory.group G (\<oplus>) \<zero>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> stabilizer A; b \<in> stabilizer A\<rbrakk> \<Longrightarrow> a \<oplus> b \<in> stabilizer A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in> stabilizer A; ?b \<in> stabilizer A\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> stabilizer A

goal (1 subgoal):
 1. \<zero> \<in> stabilizer A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<zero> \<in> stabilizer A
[PROOF STEP]
show "\<zero> \<in> stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<in> stabilizer A
[PROOF STEP]
using sub_unit_closed
[PROOF STATE]
proof (prove)
using this:
\<zero> \<in> stabilizer ?A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (stabilizer B) \<Longrightarrow> card (stabilizer A) dvd card (stabilizer B)
 2. infinite (stabilizer B) \<Longrightarrow> card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
using H.lagrange hB
[PROOF STATE]
proof (prove)
using this:
finite (stabilizer B) \<Longrightarrow> card (stabilizer B) = card (stabilizer A) * H.index
finite (stabilizer B)

goal (1 subgoal):
 1. card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (stabilizer A) dvd card (stabilizer B)

goal (1 subgoal):
 1. infinite (stabilizer B) \<Longrightarrow> card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (stabilizer B) \<Longrightarrow> card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite (stabilizer B)

goal (1 subgoal):
 1. infinite (stabilizer B) \<Longrightarrow> card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite (stabilizer B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite (stabilizer B)

goal (1 subgoal):
 1. card (stabilizer A) dvd card (stabilizer B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (stabilizer A) dvd card (stabilizer B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_coset_Un:
  assumes "A \<subseteq> G"
  shows "(\<Union> x \<in> A. sumset {x} (stabilizer A)) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>A. sumset {x} (stabilizer A)) = A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Union>x\<in>A. sumset {x} (stabilizer A)) \<subseteq> A
 2. A \<subseteq> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
show "(\<Union>x\<in>A. sumset {x} (stabilizer A)) \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>A. sumset {x} (stabilizer A)) \<subseteq> A
[PROOF STEP]
using stabilizer_coset_subset assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<subseteq> G; ?x \<in> ?A\<rbrakk> \<Longrightarrow> sumset {?x} (stabilizer ?A) \<subseteq> ?A
A \<subseteq> G

goal (1 subgoal):
 1. (\<Union>x\<in>A. sumset {x} (stabilizer A)) \<subseteq> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Union>x\<in>A. sumset {x} (stabilizer A)) \<subseteq> A

goal (1 subgoal):
 1. A \<subseteq> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<subseteq> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
show "A \<subseteq> (\<Union>x\<in>A. sumset {x} (stabilizer A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
assume hx: "x \<in> A"
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have "x \<in> sumset {x} (stabilizer A)"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. x \<in> sumset {x} (stabilizer A)
[PROOF STEP]
using sub_unit_closed assms
[PROOF STATE]
proof (prove)
using this:
x \<in> A
\<zero> \<in> stabilizer ?A
A \<subseteq> G

goal (1 subgoal):
 1. x \<in> sumset {x} (stabilizer A)
[PROOF STEP]
by (metis in_mono right_unit singletonI sumset.sumsetI unit_closed)
[PROOF STATE]
proof (state)
this:
x \<in> sumset {x} (stabilizer A)

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
thus "x \<in> (\<Union>x\<in>A. sumset {x} (stabilizer A))"
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset {x} (stabilizer A)

goal (1 subgoal):
 1. x \<in> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
using hx
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset {x} (stabilizer A)
x \<in> A

goal (1 subgoal):
 1. x \<in> (\<Union>x\<in>A. sumset {x} (stabilizer A))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> (\<Union>x\<in>A. sumset {x} (stabilizer A))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<subseteq> (\<Union>x\<in>A. sumset {x} (stabilizer A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_empty: "stabilizer {} = G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer {} = G
[PROOF STEP]
using sumset_empty Int_empty_left stabilizer_def subset_antisym
[PROOF STATE]
proof (prove)
using this:
sumset ?A {} = {}
sumset {} ?A = {}
{} \<inter> ?B = {}
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}
\<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> ?A = ?B

goal (1 subgoal):
 1. stabilizer {} = G
[PROOF STEP]
by (smt (verit, best) mem_Collect_eq subsetI sumset_Int_carrier_eq(1) sumset_commute)


[STATEMENT]
lemma stabilizer_finite:
  assumes "S \<subseteq> G" and "S \<noteq> {}" and "finite S"
  shows "finite (stabilizer S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (stabilizer S)
[PROOF STEP]
using stabilizer_subset_nempty assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?S \<noteq> {}; ?S \<subseteq> G\<rbrakk> \<Longrightarrow> stabilizer ?S \<subseteq> differenceset ?S ?S
S \<subseteq> G
S \<noteq> {}
finite S

goal (1 subgoal):
 1. finite (stabilizer S)
[PROOF STEP]
by (meson finite_minusset finite_sumset rev_finite_subset)


[STATEMENT]
lemma stabilizer_subset_group:
  shows "stabilizer S \<subseteq> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer S \<subseteq> G
[PROOF STEP]
using stabilizer_def
[PROOF STATE]
proof (prove)
using this:
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. stabilizer S \<subseteq> G
[PROOF STEP]
by blast


[STATEMENT]
lemma sumset_stabilizer_eq_iff:
  assumes "a \<in> G" and "b \<in> G"
  shows "sumset {a} (stabilizer A) = sumset {b} (stabilizer A) \<longleftrightarrow>
    (sumset {a} (stabilizer A)) \<inter> (sumset {b} (stabilizer A)) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sumset {a} (stabilizer A) = sumset {b} (stabilizer A)) = (sumset {a} (stabilizer A) \<inter> sumset {b} (stabilizer A) \<noteq> {})
[PROOF STEP]
by (simp add: assms sumset_subgroup_eq_iff)


[STATEMENT]
lemma sumset_stabilizer_eq_Class_Union:
  assumes "A \<subseteq> G"
  shows "sumset A (stabilizer B) = (\<Union> (Class B ` A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset A (stabilizer B) = \<Union> (Class B ` A)
[PROOF STEP]
by (simp add: assms sumset_subgroup_eq_Class_Union)


[STATEMENT]
lemma card_stabilizer_divide_sumset:
  assumes "A \<subseteq> G"
  shows "card (stabilizer B) dvd card (sumset A (stabilizer B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (stabilizer B) dvd card (sumset A (stabilizer B))
[PROOF STEP]
by (simp add: assms card_divide_sumset)


[STATEMENT]
lemma Class_image_sumset_stabilizer_eq:
  assumes "A \<subseteq> G"
  shows "Class B ` (sumset A (stabilizer B)) = Class B ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Class B ` sumset A (stabilizer B) = Class B ` A
[PROOF STEP]
by (simp add: Class_image_sumset_subgroup_eq assms)


[STATEMENT]
lemma Class_cover_imp_subset_or_disj:
  assumes "A = (\<Union> (Class B ` C))" and "x \<in> G" and "C \<subseteq> G"
  shows "Class B x \<subseteq> A \<or> Class B x \<inter> A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Class B x \<subseteq> A \<or> Class B x \<inter> A = {}
[PROOF STEP]
by (simp add: Class_cover_imp_subset_or_disj assms)


[STATEMENT]
lemma stabilizer_sumset_disjoint:
  fixes S1 S2 :: "'a set"
  assumes "stabilizer S1 \<inter> stabilizer S2 = {\<zero>}" and "S1 \<subseteq> G" and "S2 \<subseteq> G"
    and "finite S1" and "finite S2" and "S1 \<noteq> {}" and "S2 \<noteq> {}"
  shows "card (sumset (stabilizer S1) (stabilizer S2)) =
    card (stabilizer S1) * card (stabilizer S2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (sumset (stabilizer S1) (stabilizer S2)) = card (stabilizer S1) * card (stabilizer S2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (sumset (stabilizer S1) (stabilizer S2)) = card (stabilizer S1) * card (stabilizer S2)
[PROOF STEP]
have inj_on : "inj_on (\<lambda> (a, b). a \<oplus> b) (stabilizer S1 \<times> stabilizer S2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>(a, b). a \<oplus> b) (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
proof(intro inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "x \<in> stabilizer S1 \<times> stabilizer S2" and "y \<in> stabilizer S1 \<times> stabilizer S2" and
      "(case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)"
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer S1 \<times> stabilizer S2
y \<in> stabilizer S1 \<times> stabilizer S2
(case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> stabilizer S1 \<times> stabilizer S2
y \<in> stabilizer S1 \<times> stabilizer S2
(case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)
[PROOF STEP]
obtain a b c d where hx: "x = (a, b)" and hy: "y = (c, d)" and ha: "a \<in> stabilizer S1" and
      hb: "b \<in> stabilizer S2" and hc: "c \<in> stabilizer S1" and hd: "d \<in> stabilizer S2" and
      habcd: "a \<oplus> b = c \<oplus> d"
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer S1 \<times> stabilizer S2
y \<in> stabilizer S1 \<times> stabilizer S2
(case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>x = (a, b); y = (c, d); a \<in> stabilizer S1; b \<in> stabilizer S2; c \<in> stabilizer S1; d \<in> stabilizer S2; a \<oplus> b = c \<oplus> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (a, b)
y = (c, d)
a \<in> stabilizer S1
b \<in> stabilizer S2
c \<in> stabilizer S1
d \<in> stabilizer S2
a \<oplus> b = c \<oplus> d

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (a, b)
y = (c, d)
a \<in> stabilizer S1
b \<in> stabilizer S2
c \<in> stabilizer S1
d \<in> stabilizer S2
a \<oplus> b = c \<oplus> d
[PROOF STEP]
have haG: "a \<in> G"
[PROOF STATE]
proof (prove)
using this:
x = (a, b)
y = (c, d)
a \<in> stabilizer S1
b \<in> stabilizer S2
c \<in> stabilizer S1
d \<in> stabilizer S2
a \<oplus> b = c \<oplus> d

goal (1 subgoal):
 1. a \<in> G
[PROOF STEP]
using stabilizer_def
[PROOF STATE]
proof (prove)
using this:
x = (a, b)
y = (c, d)
a \<in> stabilizer S1
b \<in> stabilizer S2
c \<in> stabilizer S1
d \<in> stabilizer S2
a \<oplus> b = c \<oplus> d
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have hbG: "b \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> G
[PROOF STEP]
using hb stabilizer_def
[PROOF STATE]
proof (prove)
using this:
b \<in> stabilizer S2
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have hcG: "c \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<in> G
[PROOF STEP]
using hc stabilizer_def
[PROOF STATE]
proof (prove)
using this:
c \<in> stabilizer S1
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have hdG: "d \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<in> G
[PROOF STEP]
using hd stabilizer_def
[PROOF STATE]
proof (prove)
using this:
d \<in> stabilizer S2
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d \<in> G
[PROOF STEP]
have "a \<ominus> c = d \<ominus> b"
[PROOF STATE]
proof (prove)
using this:
d \<in> G

goal (1 subgoal):
 1. a \<ominus> c = d \<ominus> b
[PROOF STEP]
using habcd haG hbG hcG hdG
[PROOF STATE]
proof (prove)
using this:
d \<in> G
a \<oplus> b = c \<oplus> d
a \<in> G
b \<in> G
c \<in> G
d \<in> G

goal (1 subgoal):
 1. a \<ominus> c = d \<ominus> b
[PROOF STEP]
by (metis (full_types) associative commutative composition_closed inverse_equality invertible
        invertible_def invertible_left_inverse2)
[PROOF STATE]
proof (state)
this:
a \<ominus> c = d \<ominus> b

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<ominus> c = d \<ominus> b

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "a \<ominus> c \<in> stabilizer S1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<ominus> c \<in> stabilizer S1
[PROOF STEP]
using ha hc stabilizer_is_subgroup
      subgroup.axioms(1) submonoid.sub_composition_closed
[PROOF STATE]
proof (prove)
using this:
a \<in> stabilizer S1
c \<in> stabilizer S1
subgroup (stabilizer ?S) G (\<oplus>) \<zero>
subgroup ?G ?M ?composition ?unit \<Longrightarrow> submonoid ?G ?M ?composition ?unit
\<lbrakk>submonoid ?N ?M ?composition ?unit; ?a \<in> ?N; ?b \<in> ?N\<rbrakk> \<Longrightarrow> ?composition ?a ?b \<in> ?N

goal (1 subgoal):
 1. a \<ominus> c \<in> stabilizer S1
[PROOF STEP]
by (metis group.invertible group_axioms hcG subgroup.subgroup_inverse_iff)
[PROOF STATE]
proof (state)
this:
a \<ominus> c \<in> stabilizer S1

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<ominus> c \<in> stabilizer S1

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "d \<ominus> b \<in> stabilizer S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<ominus> b \<in> stabilizer S2
[PROOF STEP]
using hd hb  stabilizer_is_subgroup
      subgroup.axioms(1) submonoid.sub_composition_closed
[PROOF STATE]
proof (prove)
using this:
d \<in> stabilizer S2
b \<in> stabilizer S2
subgroup (stabilizer ?S) G (\<oplus>) \<zero>
subgroup ?G ?M ?composition ?unit \<Longrightarrow> submonoid ?G ?M ?composition ?unit
\<lbrakk>submonoid ?N ?M ?composition ?unit; ?a \<in> ?N; ?b \<in> ?N\<rbrakk> \<Longrightarrow> ?composition ?a ?b \<in> ?N

goal (1 subgoal):
 1. d \<ominus> b \<in> stabilizer S2
[PROOF STEP]
by (metis group.invertible group_axioms hbG subgroup.subgroup_inverse_iff)
[PROOF STATE]
proof (state)
this:
d \<ominus> b \<in> stabilizer S2

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<ominus> c = d \<ominus> b
a \<ominus> c \<in> stabilizer S1
d \<ominus> b \<in> stabilizer S2
[PROOF STEP]
have "a \<ominus> c = \<zero>" and "d \<ominus> b = \<zero>"
[PROOF STATE]
proof (prove)
using this:
a \<ominus> c = d \<ominus> b
a \<ominus> c \<in> stabilizer S1
d \<ominus> b \<in> stabilizer S2

goal (1 subgoal):
 1. a \<ominus> c = \<zero> &&& d \<ominus> b = \<zero>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
a \<ominus> c = d \<ominus> b
a \<ominus> c \<in> stabilizer S1
d \<ominus> b \<in> stabilizer S2
stabilizer S1 \<inter> stabilizer S2 = {\<zero>}

goal (1 subgoal):
 1. a \<ominus> c = \<zero> &&& d \<ominus> b = \<zero>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<ominus> c = \<zero>
d \<ominus> b = \<zero>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> stabilizer S1 \<times> stabilizer S2; y \<in> stabilizer S1 \<times> stabilizer S2; (case x of (a, b) \<Rightarrow> a \<oplus> b) = (case y of (a, b) \<Rightarrow> a \<oplus> b)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
thus "x = y"
[PROOF STATE]
proof (prove)
using this:
a \<ominus> c = \<zero>
d \<ominus> b = \<zero>

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using hx hy haG hbG hcG hdG
[PROOF STATE]
proof (prove)
using this:
a \<ominus> c = \<zero>
d \<ominus> b = \<zero>
x = (a, b)
y = (c, d)
a \<in> G
b \<in> G
c \<in> G
d \<in> G

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (metis inverse_closed invertible invertible_right_cancel invertible_right_inverse)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>(a, b). a \<oplus> b) (stabilizer S1 \<times> stabilizer S2)

goal (1 subgoal):
 1. card (sumset (stabilizer S1) (stabilizer S2)) = card (stabilizer S1) * card (stabilizer S2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>(a, b). a \<oplus> b) (stabilizer S1 \<times> stabilizer S2)

goal (1 subgoal):
 1. card (sumset (stabilizer S1) (stabilizer S2)) = card (stabilizer S1) * card (stabilizer S2)
[PROOF STEP]
have himage : "(\<lambda> (a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) =
    sumset (stabilizer S1) (stabilizer S2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) = sumset (stabilizer S1) (stabilizer S2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) \<subseteq> sumset (stabilizer S1) (stabilizer S2)
 2. sumset (stabilizer S1) (stabilizer S2) \<subseteq> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
show "(\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) \<subseteq> sumset (stabilizer S1) (stabilizer S2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) \<subseteq> sumset (stabilizer S1) (stabilizer S2)
[PROOF STEP]
using stabilizer_subset_group
[PROOF STATE]
proof (prove)
using this:
stabilizer ?S \<subseteq> G

goal (1 subgoal):
 1. (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) \<subseteq> sumset (stabilizer S1) (stabilizer S2)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) \<subseteq> sumset (stabilizer S1) (stabilizer S2)

goal (1 subgoal):
 1. sumset (stabilizer S1) (stabilizer S2) \<subseteq> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sumset (stabilizer S1) (stabilizer S2) \<subseteq> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
show "sumset (stabilizer S1) (stabilizer S2) \<subseteq> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (stabilizer S1) (stabilizer S2) \<subseteq> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sumset (stabilizer S1) (stabilizer S2) \<Longrightarrow> x \<in> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sumset (stabilizer S1) (stabilizer S2) \<Longrightarrow> x \<in> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
assume "x \<in> sumset (stabilizer S1) (stabilizer S2)"
[PROOF STATE]
proof (state)
this:
x \<in> sumset (stabilizer S1) (stabilizer S2)

goal (1 subgoal):
 1. \<And>x. x \<in> sumset (stabilizer S1) (stabilizer S2) \<Longrightarrow> x \<in> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> sumset (stabilizer S1) (stabilizer S2)
[PROOF STEP]
obtain s1 s2 where hs1: "s1 \<in> stabilizer S1" and hs2: "s2 \<in> stabilizer S2" and
        "x = s1 \<oplus> s2"
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset (stabilizer S1) (stabilizer S2)

goal (1 subgoal):
 1. (\<And>s1 s2. \<lbrakk>s1 \<in> stabilizer S1; s2 \<in> stabilizer S2; x = s1 \<oplus> s2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson sumset.cases)
[PROOF STATE]
proof (state)
this:
s1 \<in> stabilizer S1
s2 \<in> stabilizer S2
x = s1 \<oplus> s2

goal (1 subgoal):
 1. \<And>x. x \<in> sumset (stabilizer S1) (stabilizer S2) \<Longrightarrow> x \<in> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
thus "x \<in> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)"
[PROOF STATE]
proof (prove)
using this:
s1 \<in> stabilizer S1
s2 \<in> stabilizer S2
x = s1 \<oplus> s2

goal (1 subgoal):
 1. x \<in> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
using hs1 hs2
[PROOF STATE]
proof (prove)
using this:
s1 \<in> stabilizer S1
s2 \<in> stabilizer S2
x = s1 \<oplus> s2
s1 \<in> stabilizer S1
s2 \<in> stabilizer S2

goal (1 subgoal):
 1. x \<in> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sumset (stabilizer S1) (stabilizer S2) \<subseteq> (\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) = sumset (stabilizer S1) (stabilizer S2)

goal (1 subgoal):
 1. card (sumset (stabilizer S1) (stabilizer S2)) = card (stabilizer S1) * card (stabilizer S2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inj_on (\<lambda>(a, b). a \<oplus> b) (stabilizer S1 \<times> stabilizer S2)
(\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) = sumset (stabilizer S1) (stabilizer S2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>(a, b). a \<oplus> b) (stabilizer S1 \<times> stabilizer S2)
(\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) = sumset (stabilizer S1) (stabilizer S2)

goal (1 subgoal):
 1. card (sumset (stabilizer S1) (stabilizer S2)) = card (stabilizer S1) * card (stabilizer S2)
[PROOF STEP]
using card_image card_cartesian_product
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>(a, b). a \<oplus> b) (stabilizer S1 \<times> stabilizer S2)
(\<lambda>(a, b). a \<oplus> b) ` (stabilizer S1 \<times> stabilizer S2) = sumset (stabilizer S1) (stabilizer S2)
inj_on ?f ?A \<Longrightarrow> card (?f ` ?A) = card ?A
card (?A \<times> ?B) = card ?A * card ?B

goal (1 subgoal):
 1. card (sumset (stabilizer S1) (stabilizer S2)) = card (stabilizer S1) * card (stabilizer S2)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card (sumset (stabilizer S1) (stabilizer S2)) = card (stabilizer S1) * card (stabilizer S2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_sub_sumset_left:
  "stabilizer A \<subseteq> stabilizer (sumset A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer (sumset A B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer A \<Longrightarrow> x \<in> stabilizer (sumset A B)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer A \<Longrightarrow> x \<in> stabilizer (sumset A B)
[PROOF STEP]
assume hx: "x \<in> stabilizer A"
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer A

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer A \<Longrightarrow> x \<in> stabilizer (sumset A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> stabilizer A
[PROOF STEP]
have "sumset {x} (sumset A B) = sumset A B"
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer A

goal (1 subgoal):
 1. sumset {x} (sumset A B) = sumset A B
[PROOF STEP]
using stabilizer_def sumset_assoc
    mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer A
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}
sumset (sumset ?A ?B) ?C = sumset ?A (sumset ?B ?C)
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. sumset {x} (sumset A B) = sumset A B
[PROOF STEP]
by (smt (verit, del_insts) sumset_Int_carrier_eq(1) sumset_commute)
[PROOF STATE]
proof (state)
this:
sumset {x} (sumset A B) = sumset A B

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer A \<Longrightarrow> x \<in> stabilizer (sumset A B)
[PROOF STEP]
thus "x \<in> stabilizer (sumset A B)"
[PROOF STATE]
proof (prove)
using this:
sumset {x} (sumset A B) = sumset A B

goal (1 subgoal):
 1. x \<in> stabilizer (sumset A B)
[PROOF STEP]
using hx stabilizer_def
[PROOF STATE]
proof (prove)
using this:
sumset {x} (sumset A B) = sumset A B
x \<in> stabilizer A
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. x \<in> stabilizer (sumset A B)
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq sumset_Int_carrier)
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer (sumset A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_sub_sumset_right:
  "stabilizer B \<subseteq> stabilizer (sumset A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer B \<subseteq> stabilizer (sumset A B)
[PROOF STEP]
using stabilizer_sub_sumset_left sumset_commute
[PROOF STATE]
proof (prove)
using this:
stabilizer ?A \<subseteq> stabilizer (sumset ?A ?B)
sumset ?A ?B = sumset ?B ?A

goal (1 subgoal):
 1. stabilizer B \<subseteq> stabilizer (sumset A B)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma not_mem_stabilizer_obtain:
  assumes "A \<noteq> {}" and "x \<notin> stabilizer A" and "x \<in> G" and "A \<subseteq> G" and "finite A"
  obtains a where "a \<in> A" and "x \<oplus> a \<notin> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<oplus> a \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<oplus> a \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "sumset {x} A \<noteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} A \<noteq> A
[PROOF STEP]
using assms stabilizer_def
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
x \<notin> stabilizer A
x \<in> G
A \<subseteq> G
finite A
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. sumset {x} A \<noteq> A
[PROOF STEP]
by (metis (mono_tags, lifting) inf.orderE mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
sumset {x} A \<noteq> A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<oplus> a \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sumset {x} A \<noteq> A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<oplus> a \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "card (sumset {x} A) = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (sumset {x} A) = card A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
x \<notin> stabilizer A
x \<in> G
A \<subseteq> G
finite A

goal (1 subgoal):
 1. card (sumset {x} A) = card A
[PROOF STEP]
by (metis card_sumset_singleton_eq inf.orderE sumset_commute)
[PROOF STATE]
proof (state)
this:
card (sumset {x} A) = card A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<oplus> a \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sumset {x} A \<noteq> A
card (sumset {x} A) = card A
[PROOF STEP]
obtain y where "y \<in> sumset {x} A" and "y \<notin> A"
[PROOF STATE]
proof (prove)
using this:
sumset {x} A \<noteq> A
card (sumset {x} A) = card A

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> sumset {x} A; y \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sumset {x} A \<noteq> A
card (sumset {x} A) = card A
A \<noteq> {}
x \<notin> stabilizer A
x \<in> G
A \<subseteq> G
finite A

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> sumset {x} A; y \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson card_subset_eq subsetI)
[PROOF STATE]
proof (state)
this:
y \<in> sumset {x} A
y \<notin> A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<oplus> a \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> sumset {x} A
y \<notin> A
[PROOF STEP]
obtain a where "a \<in> A" and "x \<oplus> a \<notin> A"
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {x} A
y \<notin> A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<oplus> a \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {x} A
y \<notin> A
A \<noteq> {}
x \<notin> stabilizer A
x \<in> G
A \<subseteq> G
finite A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<oplus> a \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis singletonD sumset.cases)
[PROOF STATE]
proof (state)
this:
a \<in> A
x \<oplus> a \<notin> A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<oplus> a \<notin> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in> A
x \<oplus> a \<notin> A

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> A
x \<oplus> a \<notin> A
\<lbrakk>?a \<in> A; x \<oplus> ?a \<notin> A\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumset_eq_sub_stabilizer:
  assumes "A \<subseteq> G" and "B \<subseteq> G" and "finite B"
  shows "sumset A B = B \<Longrightarrow> A \<subseteq> stabilizer B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset A B = B \<Longrightarrow> A \<subseteq> stabilizer B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sumset A B = B; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> stabilizer B
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sumset A B = B; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> stabilizer B
[PROOF STEP]
assume hsum: "sumset A B = B" and hx: "x \<in> A"
[PROOF STATE]
proof (state)
this:
sumset A B = B
x \<in> A

goal (1 subgoal):
 1. \<And>x. \<lbrakk>sumset A B = B; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> stabilizer B
[PROOF STEP]
have "sumset {x} B = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} B = B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sumset {x} B = B
[PROOF STEP]
have "sumset {x} B \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} B \<subseteq> B
[PROOF STEP]
using hsum hx
[PROOF STATE]
proof (prove)
using this:
sumset A B = B
x \<in> A

goal (1 subgoal):
 1. sumset {x} B \<subseteq> B
[PROOF STEP]
by (metis empty_subsetI equalityE insert_subset sumset_mono)
[PROOF STATE]
proof (state)
this:
sumset {x} B \<subseteq> B

goal (1 subgoal):
 1. sumset {x} B = B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sumset {x} B \<subseteq> B

goal (1 subgoal):
 1. sumset {x} B = B
[PROOF STEP]
have "card (sumset {x} B) = card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (sumset {x} B) = card B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
B \<subseteq> G
finite B

goal (1 subgoal):
 1. card (sumset {x} B) = card B
[PROOF STEP]
by (metis IntD1 Int_absorb1 card_sumset_singleton_eq hx inf_commute sumset_commute)
[PROOF STATE]
proof (state)
this:
card (sumset {x} B) = card B

goal (1 subgoal):
 1. sumset {x} B = B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sumset {x} B \<subseteq> B
card (sumset {x} B) = card B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sumset {x} B \<subseteq> B
card (sumset {x} B) = card B

goal (1 subgoal):
 1. sumset {x} B = B
[PROOF STEP]
using card_subset_eq assms(3)
[PROOF STATE]
proof (prove)
using this:
sumset {x} B \<subseteq> B
card (sumset {x} B) = card B
\<lbrakk>finite ?B; ?A \<subseteq> ?B; card ?A = card ?B\<rbrakk> \<Longrightarrow> ?A = ?B
finite B

goal (1 subgoal):
 1. sumset {x} B = B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sumset {x} B = B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sumset {x} B = B

goal (1 subgoal):
 1. \<And>x. \<lbrakk>sumset A B = B; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> stabilizer B
[PROOF STEP]
thus "x \<in> stabilizer B"
[PROOF STATE]
proof (prove)
using this:
sumset {x} B = B

goal (1 subgoal):
 1. x \<in> stabilizer B
[PROOF STEP]
using hx assms(1) stabilizer_def
[PROOF STATE]
proof (prove)
using this:
sumset {x} B = B
x \<in> A
A \<subseteq> G
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. x \<in> stabilizer B
[PROOF STEP]
by (metis (mono_tags, lifting) assms(2) inf.orderE mem_Collect_eq subsetD)
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumset_stabilizer_eq:
  shows "sumset (stabilizer A) (stabilizer A) = stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (stabilizer A) (stabilizer A) = stabilizer A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sumset (stabilizer A) (stabilizer A) \<subseteq> stabilizer A
 2. stabilizer A \<subseteq> sumset (stabilizer A) (stabilizer A)
[PROOF STEP]
show "sumset (stabilizer A) (stabilizer A) \<subseteq> stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (stabilizer A) (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
using stabilizer_is_subgroup subgroup.axioms(1) subsetI
[PROOF STATE]
proof (prove)
using this:
subgroup (stabilizer ?S) G (\<oplus>) \<zero>
subgroup ?G ?M ?composition ?unit \<Longrightarrow> submonoid ?G ?M ?composition ?unit
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B

goal (1 subgoal):
 1. sumset (stabilizer A) (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
by (metis (mono_tags, lifting) additive_abelian_group.sumset.simps additive_abelian_group_axioms
      submonoid.sub_composition_closed)
[PROOF STATE]
proof (state)
this:
sumset (stabilizer A) (stabilizer A) \<subseteq> stabilizer A

goal (1 subgoal):
 1. stabilizer A \<subseteq> sumset (stabilizer A) (stabilizer A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabilizer A \<subseteq> sumset (stabilizer A) (stabilizer A)
[PROOF STEP]
show "stabilizer A \<subseteq> sumset (stabilizer A) (stabilizer A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer A \<subseteq> sumset (stabilizer A) (stabilizer A)
[PROOF STEP]
using Left_Coset_eq_sumset stabilizer_is_nonempty
      stabilizer_subset_group sub_unit_closed additive_abelian_group_axioms right_unit
      subset_iff sumsetI
[PROOF STATE]
proof (prove)
using this:
?x \<in> G \<Longrightarrow> sumset {?x} (stabilizer ?A) = ?x \<cdot>| stabilizer ?A
stabilizer ?S \<noteq> {}
stabilizer ?S \<subseteq> G
\<zero> \<in> stabilizer ?A
additive_abelian_group G (\<oplus>) \<zero>
?a \<in> G \<Longrightarrow> ?a \<oplus> \<zero> = ?a
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)
\<lbrakk>?a \<in> ?A; ?a \<in> G; ?b \<in> ?B; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> sumset ?A ?B

goal (1 subgoal):
 1. stabilizer A \<subseteq> sumset (stabilizer A) (stabilizer A)
[PROOF STEP]
by (smt (verit, best))
[PROOF STATE]
proof (state)
this:
stabilizer A \<subseteq> sumset (stabilizer A) (stabilizer A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma differenceset_stabilizer_eq:
  shows "differenceset (stabilizer A) (stabilizer A) = stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. differenceset (stabilizer A) (stabilizer A) = stabilizer A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. differenceset (stabilizer A) (stabilizer A) \<subseteq> stabilizer A
 2. stabilizer A \<subseteq> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
show "differenceset (stabilizer A) (stabilizer A) \<subseteq> stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. differenceset (stabilizer A) (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> differenceset (stabilizer A) (stabilizer A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> differenceset (stabilizer A) (stabilizer A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
assume "x \<in> differenceset (stabilizer A) (stabilizer A)"
[PROOF STATE]
proof (state)
this:
x \<in> differenceset (stabilizer A) (stabilizer A)

goal (1 subgoal):
 1. \<And>x. x \<in> differenceset (stabilizer A) (stabilizer A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
obtain a b where "a \<in> stabilizer A" and "b \<in> stabilizer A" and "x = a \<ominus> b"
[PROOF STATE]
proof (prove)
using this:
x \<in> differenceset (stabilizer A) (stabilizer A)

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<in> stabilizer A; b \<in> stabilizer A; x = a \<ominus> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis minusset.cases sumset.cases)
[PROOF STATE]
proof (state)
this:
a \<in> stabilizer A
b \<in> stabilizer A
x = a \<ominus> b

goal (1 subgoal):
 1. \<And>x. x \<in> differenceset (stabilizer A) (stabilizer A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
thus "x \<in> stabilizer A"
[PROOF STATE]
proof (prove)
using this:
a \<in> stabilizer A
b \<in> stabilizer A
x = a \<ominus> b

goal (1 subgoal):
 1. x \<in> stabilizer A
[PROOF STEP]
using stabilizer_is_subgroup subgroup.axioms(1)
[PROOF STATE]
proof (prove)
using this:
a \<in> stabilizer A
b \<in> stabilizer A
x = a \<ominus> b
subgroup (stabilizer ?S) G (\<oplus>) \<zero>
subgroup ?G ?M ?composition ?unit \<Longrightarrow> submonoid ?G ?M ?composition ?unit

goal (1 subgoal):
 1. x \<in> stabilizer A
[PROOF STEP]
by (smt (verit, ccfv_threshold) in_mono invertible stabilizer_subset_group
        subgroup_inverse_iff sub_composition_closed)
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
differenceset (stabilizer A) (stabilizer A) \<subseteq> stabilizer A

goal (1 subgoal):
 1. stabilizer A \<subseteq> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabilizer A \<subseteq> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
show "stabilizer A \<subseteq> differenceset (stabilizer A) (stabilizer A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer A \<subseteq> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer A \<Longrightarrow> x \<in> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer A \<Longrightarrow> x \<in> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
assume hx: "x \<in> stabilizer A"
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer A

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer A \<Longrightarrow> x \<in> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> stabilizer A
[PROOF STEP]
have "x \<ominus> \<zero> \<in> differenceset (stabilizer A) (stabilizer A)"
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer A

goal (1 subgoal):
 1. x \<ominus> \<zero> \<in> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<ominus> \<zero> \<in> differenceset (stabilizer A) (stabilizer A)

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer A \<Longrightarrow> x \<in> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<ominus> \<zero> \<in> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
show "x \<in> differenceset (stabilizer A) (stabilizer A)"
[PROOF STATE]
proof (prove)
using this:
x \<ominus> \<zero> \<in> differenceset (stabilizer A) (stabilizer A)

goal (1 subgoal):
 1. x \<in> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
using hx
[PROOF STATE]
proof (prove)
using this:
x \<ominus> \<zero> \<in> differenceset (stabilizer A) (stabilizer A)
x \<in> stabilizer A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stabilizer A \<subseteq> differenceset (stabilizer A) (stabilizer A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer2_sub_stabilizer:
  shows "stabilizer(stabilizer A) \<subseteq> stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
proof(cases "A \<noteq> {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<noteq> {} \<Longrightarrow> stabilizer (stabilizer A) \<subseteq> stabilizer A
 2. \<not> A \<noteq> {} \<Longrightarrow> stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (2 subgoals):
 1. A \<noteq> {} \<Longrightarrow> stabilizer (stabilizer A) \<subseteq> stabilizer A
 2. \<not> A \<noteq> {} \<Longrightarrow> stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> {}
[PROOF STEP]
have "stabilizer(stabilizer A) \<subseteq> differenceset (stabilizer A) (stabilizer A)"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. stabilizer (stabilizer A) \<subseteq> differenceset (stabilizer A) (stabilizer A)
[PROOF STEP]
by (simp add: stabilizer_is_nonempty stabilizer_subset_group stabilizer_subset_nempty)
[PROOF STATE]
proof (state)
this:
stabilizer (stabilizer A) \<subseteq> differenceset (stabilizer A) (stabilizer A)

goal (2 subgoals):
 1. A \<noteq> {} \<Longrightarrow> stabilizer (stabilizer A) \<subseteq> stabilizer A
 2. \<not> A \<noteq> {} \<Longrightarrow> stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
stabilizer (stabilizer A) \<subseteq> differenceset (stabilizer A) (stabilizer A)

goal (1 subgoal):
 1. stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
using differenceset_stabilizer_eq
[PROOF STATE]
proof (prove)
using this:
stabilizer (stabilizer A) \<subseteq> differenceset (stabilizer A) (stabilizer A)
differenceset (stabilizer ?A) (stabilizer ?A) = stabilizer ?A

goal (1 subgoal):
 1. stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
stabilizer (stabilizer A) \<subseteq> stabilizer A

goal (1 subgoal):
 1. \<not> A \<noteq> {} \<Longrightarrow> stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A \<noteq> {} \<Longrightarrow> stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> A \<noteq> {}

goal (1 subgoal):
 1. \<not> A \<noteq> {} \<Longrightarrow> stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> A \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> A \<noteq> {}

goal (1 subgoal):
 1. stabilizer (stabilizer A) \<subseteq> stabilizer A
[PROOF STEP]
by (simp add: stabilizer_empty stabilizer_subset_group)
[PROOF STATE]
proof (state)
this:
stabilizer (stabilizer A) \<subseteq> stabilizer A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_left_sumset_invariant:
  assumes "a \<in> G" and "A \<subseteq> G"
  shows "stabilizer (sumset {a} A) = stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (sumset {a} A) = stabilizer A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. stabilizer (sumset {a} A) \<subseteq> stabilizer A
 2. stabilizer A \<subseteq> stabilizer (sumset {a} A)
[PROOF STEP]
show "stabilizer (sumset {a} A) \<subseteq> stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (sumset {a} A) \<subseteq> stabilizer A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (sumset {a} A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (sumset {a} A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
assume hx: "x \<in> stabilizer (sumset {a} A)"
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer (sumset {a} A)

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (sumset {a} A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> stabilizer (sumset {a} A)
[PROOF STEP]
have hxG: "x \<in> G"
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer (sumset {a} A)

goal (1 subgoal):
 1. x \<in> G
[PROOF STEP]
using stabilizer_def
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer (sumset {a} A)
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

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

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (sumset {a} A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
have "sumset {x} (sumset {a} A) = sumset {a} A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} (sumset {a} A) = sumset {a} A
[PROOF STEP]
using stabilizer_def hx
[PROOF STATE]
proof (prove)
using this:
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}
x \<in> stabilizer (sumset {a} A)

goal (1 subgoal):
 1. sumset {x} (sumset {a} A) = sumset {a} A
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq sumset_Int_carrier)
[PROOF STATE]
proof (state)
this:
sumset {x} (sumset {a} A) = sumset {a} A

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (sumset {a} A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sumset {x} (sumset {a} A) = sumset {a} A
[PROOF STEP]
have "sumset {x} A = A"
[PROOF STATE]
proof (prove)
using this:
sumset {x} (sumset {a} A) = sumset {a} A

goal (1 subgoal):
 1. sumset {x} A = A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sumset {x} (sumset {a} A) = sumset {a} A
a \<in> G
A \<subseteq> G

goal (1 subgoal):
 1. sumset {x} A = A
[PROOF STEP]
by (metis (full_types) sumset_assoc sumset_commute sumset_subset_carrier
          sumset_translate_eq_right)
[PROOF STATE]
proof (state)
this:
sumset {x} A = A

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (sumset {a} A) \<Longrightarrow> x \<in> stabilizer A
[PROOF STEP]
thus "x \<in> stabilizer A"
[PROOF STATE]
proof (prove)
using this:
sumset {x} A = A

goal (1 subgoal):
 1. x \<in> stabilizer A
[PROOF STEP]
using hxG stabilizer_def
[PROOF STATE]
proof (prove)
using this:
sumset {x} A = A
x \<in> G
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. x \<in> stabilizer A
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq sumset_Int_carrier)
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stabilizer (sumset {a} A) \<subseteq> stabilizer A

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer (sumset {a} A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer (sumset {a} A)
[PROOF STEP]
show "stabilizer A \<subseteq> stabilizer (sumset {a} A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer (sumset {a} A)
[PROOF STEP]
using stabilizer_def
[PROOF STATE]
proof (prove)
using this:
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer (sumset {a} A)
[PROOF STEP]
using stabilizer_sub_sumset_right
[PROOF STATE]
proof (prove)
using this:
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}
stabilizer ?B \<subseteq> stabilizer (sumset ?A ?B)

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer (sumset {a} A)
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
stabilizer A \<subseteq> stabilizer (sumset {a} A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_right_sumset_invariant:
  assumes "a \<in> G" and "A \<subseteq> G"
  shows "stabilizer (sumset A {a}) = stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (sumset A {a}) = stabilizer A
[PROOF STEP]
using sumset_commute stabilizer_left_sumset_invariant assms
[PROOF STATE]
proof (prove)
using this:
sumset ?A ?B = sumset ?B ?A
\<lbrakk>?a \<in> G; ?A \<subseteq> G\<rbrakk> \<Longrightarrow> stabilizer (sumset {?a} ?A) = stabilizer ?A
a \<in> G
A \<subseteq> G

goal (1 subgoal):
 1. stabilizer (sumset A {a}) = stabilizer A
[PROOF STEP]
by simp


[STATEMENT]
lemma stabilizer_right_differenceset_invariant:
  assumes "b \<in> G" and "A \<subseteq> G"
  shows "stabilizer (differenceset A {b}) = stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (differenceset A {b}) = stabilizer A
[PROOF STEP]
using assms minusset_eq stabilizer_right_sumset_invariant
[PROOF STATE]
proof (prove)
using this:
b \<in> G
A \<subseteq> G
minusset ?A = local.inverse ` (?A \<inter> G)
\<lbrakk>?a \<in> G; ?A \<subseteq> G\<rbrakk> \<Longrightarrow> stabilizer (sumset ?A {?a}) = stabilizer ?A

goal (1 subgoal):
 1. stabilizer (differenceset A {b}) = stabilizer A
[PROOF STEP]
by auto


[STATEMENT]
lemma stabilizer_unchanged:
  assumes "a \<in> G" and "b \<in> G"
  shows "stabilizer (sumset A B) = stabilizer (sumset A (sumset (differenceset B {b}) {a}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (sumset A B) = stabilizer (sumset A (sumset (differenceset B {b}) {a}))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabilizer (sumset A B) = stabilizer (sumset A (sumset (differenceset B {b}) {a}))
[PROOF STEP]
have "sumset A (sumset (differenceset B {b}) {a}) = sumset (differenceset (sumset A B) {b}) {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset A (sumset (differenceset B {b}) {a}) = sumset (differenceset (sumset A B) {b}) {a}
[PROOF STEP]
by (simp add: sumset_assoc)
[PROOF STATE]
proof (state)
this:
sumset A (sumset (differenceset B {b}) {a}) = sumset (differenceset (sumset A B) {b}) {a}

goal (1 subgoal):
 1. stabilizer (sumset A B) = stabilizer (sumset A (sumset (differenceset B {b}) {a}))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sumset A (sumset (differenceset B {b}) {a}) = sumset (differenceset (sumset A B) {b}) {a}

goal (1 subgoal):
 1. stabilizer (sumset A B) = stabilizer (sumset A (sumset (differenceset B {b}) {a}))
[PROOF STEP]
using stabilizer_right_sumset_invariant
    stabilizer_right_differenceset_invariant assms sumset_subset_carrier
[PROOF STATE]
proof (prove)
using this:
sumset A (sumset (differenceset B {b}) {a}) = sumset (differenceset (sumset A B) {b}) {a}
\<lbrakk>?a \<in> G; ?A \<subseteq> G\<rbrakk> \<Longrightarrow> stabilizer (sumset ?A {?a}) = stabilizer ?A
\<lbrakk>?b \<in> G; ?A \<subseteq> G\<rbrakk> \<Longrightarrow> stabilizer (differenceset ?A {?b}) = stabilizer ?A
a \<in> G
b \<in> G
sumset ?A ?B \<subseteq> G

goal (1 subgoal):
 1. stabilizer (sumset A B) = stabilizer (sumset A (sumset (differenceset B {b}) {a}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stabilizer (sumset A B) = stabilizer (sumset A (sumset (differenceset B {b}) {a}))

goal:
No subgoals!
[PROOF STEP]
qed