[STATEMENT]
lemma subset_stabilizer_of_subset_sumset:
  assumes "A \<subseteq> sumset {x} (stabilizer B)" and "x \<in> G" and "A \<noteq> {}" and "A \<subseteq> G"
  shows "stabilizer A \<subseteq> stabilizer B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
obtain a where ha: "a \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> sumset {x} (stabilizer B)
x \<in> G
A \<noteq> {}
A \<subseteq> G

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

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

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
[PROOF STEP]
obtain b where hb: "b \<in> stabilizer B" and haxb: "a = x \<oplus> b"
[PROOF STATE]
proof (prove)
using this:
a \<in> A

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

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

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
b \<in> stabilizer B
a = x \<oplus> b
[PROOF STEP]
have "stabilizer A \<subseteq> differenceset A {a}"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
b \<in> stabilizer B
a = x \<oplus> b

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

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

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

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
have "... = sumset {inverse a} A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. differenceset A {a} = sumset {local.inverse a} A
[PROOF STEP]
using sumset_commute ha assms(4) inverse_closed
    subsetD minusset_eq
[PROOF STATE]
proof (prove)
using this:
sumset ?A ?B = sumset ?B ?A
a \<in> A
A \<subseteq> G
?x \<in> G \<Longrightarrow> local.inverse ?x \<in> G
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B
minusset ?A = local.inverse ` (?A \<inter> G)

goal (1 subgoal):
 1. differenceset A {a} = sumset {local.inverse a} A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
differenceset A {a} = sumset {local.inverse a} A

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
differenceset A {a} = sumset {local.inverse a} A

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
have "... \<subseteq> sumset {inverse x \<oplus> inverse b} (sumset {x} (stabilizer B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {local.inverse a} A \<subseteq> sumset {local.inverse x \<ominus> b} (sumset {x} (stabilizer B))
[PROOF STEP]
using assms sumset_mono haxb inverse_closed hb stabilizer_subset_group subsetD
    commutative inverse_composition_commute
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> sumset {x} (stabilizer B)
x \<in> G
A \<noteq> {}
A \<subseteq> G
\<lbrakk>?A' \<subseteq> ?A; ?B' \<subseteq> ?B\<rbrakk> \<Longrightarrow> sumset ?A' ?B' \<subseteq> sumset ?A ?B
a = x \<oplus> b
?x \<in> G \<Longrightarrow> local.inverse ?x \<in> G
b \<in> stabilizer B
stabilizer ?S \<subseteq> G
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B
\<lbrakk>?x \<in> G; ?y \<in> G\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y = ?y \<oplus> ?x
\<lbrakk>invertible ?x; invertible ?y; ?x \<in> G; ?y \<in> G\<rbrakk> \<Longrightarrow> local.inverse (?x \<oplus> ?y) = local.inverse ?y \<ominus> ?x

goal (1 subgoal):
 1. sumset {local.inverse a} A \<subseteq> sumset {local.inverse x \<ominus> b} (sumset {x} (stabilizer B))
[PROOF STEP]
by (metis invertible subset_singleton_iff)
[PROOF STATE]
proof (state)
this:
sumset {local.inverse a} A \<subseteq> sumset {local.inverse x \<ominus> b} (sumset {x} (stabilizer B))

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sumset {local.inverse a} A \<subseteq> sumset {local.inverse x \<ominus> b} (sumset {x} (stabilizer B))

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
have "... = sumset {inverse b} (stabilizer B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {local.inverse x \<ominus> b} (sumset {x} (stabilizer B)) = sumset {local.inverse b} (stabilizer B)
[PROOF STEP]
using sumset_singletons_eq commutative
      assms sumset_assoc hb stabilizer_subset_group inverse_closed invertible
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> sumset {?a} {?b} = {?a \<oplus> ?b}
\<lbrakk>?x \<in> G; ?y \<in> G\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y = ?y \<oplus> ?x
A \<subseteq> sumset {x} (stabilizer B)
x \<in> G
A \<noteq> {}
A \<subseteq> G
sumset (sumset ?A ?B) ?C = sumset ?A (sumset ?B ?C)
b \<in> stabilizer B
stabilizer ?S \<subseteq> G
?x \<in> G \<Longrightarrow> local.inverse ?x \<in> G
?u \<in> G \<Longrightarrow> invertible ?u

goal (1 subgoal):
 1. sumset {local.inverse x \<ominus> b} (sumset {x} (stabilizer B)) = sumset {local.inverse b} (stabilizer B)
[PROOF STEP]
by (metis composition_closed invertible_right_inverse2 sub)
[PROOF STATE]
proof (state)
this:
sumset {local.inverse x \<ominus> b} (sumset {x} (stabilizer B)) = sumset {local.inverse b} (stabilizer B)

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sumset {local.inverse x \<ominus> b} (sumset {x} (stabilizer B)) = sumset {local.inverse b} (stabilizer B)

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
have "... = stabilizer B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {local.inverse b} (stabilizer B) = stabilizer B
[PROOF STEP]
using hb Left_Coset_eq_sumset sub_unit_closed sub subset_iff
    additive_abelian_group_axioms calculation disjoint_iff_not_equal factor_unit inverse_closed
    sumset_subgroup_eq_iff
[PROOF STATE]
proof (prove)
using this:
b \<in> stabilizer B
?x \<in> G \<Longrightarrow> sumset {?x} (stabilizer ?A) = ?x \<cdot>| stabilizer ?A
\<zero> \<in> stabilizer ?A
?a \<in> stabilizer ?A \<Longrightarrow> ?a \<in> G
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)
additive_abelian_group G (\<oplus>) \<zero>
stabilizer A \<subseteq> sumset {local.inverse b} (stabilizer B)
(?A \<inter> ?B = {}) = (\<forall>x\<in>?A. \<forall>y\<in>?B. x \<noteq> y)
stabilizer ?A = \<zero> \<cdot>| stabilizer ?A
?x \<in> G \<Longrightarrow> local.inverse ?x \<in> G
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> (sumset {?a} (stabilizer ?A) = sumset {?b} (stabilizer ?A)) = (sumset {?a} (stabilizer ?A) \<inter> sumset {?b} (stabilizer ?A) \<noteq> {})

goal (1 subgoal):
 1. sumset {local.inverse b} (stabilizer B) = stabilizer B
[PROOF STEP]
by (smt (verit, del_insts))
[PROOF STATE]
proof (state)
this:
sumset {local.inverse b} (stabilizer B) = stabilizer B

goal (1 subgoal):
 1. stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
stabilizer A \<subseteq> stabilizer B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stabilizer A \<subseteq> stabilizer B

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumset_stabilizer_eq_self:
  assumes "A \<subseteq> G"
  shows "sumset (stabilizer A) A = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (stabilizer A) A = A
[PROOF STEP]
using assms sumset_eq_Union_left[OF "stabilizer_subset_group"]
    Int_absorb2 stabilizer_coset_Un sumset_commute sumset_eq_Union_left
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
sumset (stabilizer ?S1) ?B = (\<Union>a\<in>stabilizer ?S1. sumset {a} ?B)
?A \<subseteq> ?B \<Longrightarrow> ?A \<inter> ?B = ?A
?A \<subseteq> G \<Longrightarrow> (\<Union>x\<in>?A. sumset {x} (stabilizer ?A)) = ?A
sumset ?A ?B = sumset ?B ?A
?A \<subseteq> G \<Longrightarrow> sumset ?A ?B = (\<Union>a\<in>?A. sumset {a} ?B)

goal (1 subgoal):
 1. sumset (stabilizer A) A = A
[PROOF STEP]
by presburger


[STATEMENT]
lemma stabilizer_neq_subset_sumset:
  assumes "A \<subseteq> sumset {x} (stabilizer B)" and "x \<in> A" and "\<not> sumset {x} (stabilizer B) \<subseteq> C" and
    "A \<subseteq> C" and "C \<subseteq> G"
  shows "stabilizer A \<noteq> stabilizer B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer A \<noteq> stabilizer B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabilizer A = stabilizer B \<Longrightarrow> False
[PROOF STEP]
assume heq: "stabilizer A = stabilizer B"
[PROOF STATE]
proof (state)
this:
stabilizer A = stabilizer B

goal (1 subgoal):
 1. stabilizer A = stabilizer B \<Longrightarrow> False
[PROOF STEP]
obtain a where "a \<in> sumset {x} (stabilizer B)" and
    "a \<notin> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> sumset {x} (stabilizer B); a \<notin> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> sumset {x} (stabilizer B)
x \<in> A
\<not> sumset {x} (stabilizer B) \<subseteq> C
A \<subseteq> C
C \<subseteq> G

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> sumset {x} (stabilizer B); a \<notin> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> sumset {x} (stabilizer B)
a \<notin> C

goal (1 subgoal):
 1. stabilizer A = stabilizer B \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<in> sumset {x} (stabilizer B)
a \<notin> C

goal (1 subgoal):
 1. stabilizer A = stabilizer B \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> sumset {x} (stabilizer B)
a \<notin> C
[PROOF STEP]
obtain b where "b \<in> stabilizer B" and "a = x \<oplus> b"
[PROOF STATE]
proof (prove)
using this:
a \<in> sumset {x} (stabilizer B)
a \<notin> C

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>b \<in> stabilizer B; a = x \<oplus> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sumset.cases
[PROOF STATE]
proof (prove)
using this:
a \<in> sumset {x} (stabilizer B)
a \<notin> C
\<lbrakk>?a \<in> sumset ?A ?B; \<And>a b. \<lbrakk>?a = a \<oplus> b; a \<in> ?A; a \<in> G; b \<in> ?B; b \<in> G\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. stabilizer A = stabilizer B \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<in> sumset {x} (stabilizer B)
a \<notin> C
b \<in> stabilizer B
a = x \<oplus> b
[PROOF STEP]
have "b \<oplus> x \<notin> A"
[PROOF STATE]
proof (prove)
using this:
a \<in> sumset {x} (stabilizer B)
a \<notin> C
b \<in> stabilizer B
a = x \<oplus> b

goal (1 subgoal):
 1. b \<oplus> x \<notin> A
[PROOF STEP]
using commutative stabilizer_subset_group assms in_mono
[PROOF STATE]
proof (prove)
using this:
a \<in> sumset {x} (stabilizer B)
a \<notin> C
b \<in> stabilizer B
a = x \<oplus> b
\<lbrakk>?x \<in> G; ?y \<in> G\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y = ?y \<oplus> ?x
stabilizer ?S \<subseteq> G
A \<subseteq> sumset {x} (stabilizer B)
x \<in> A
\<not> sumset {x} (stabilizer B) \<subseteq> C
A \<subseteq> C
C \<subseteq> G
?A \<subseteq> ?B \<Longrightarrow> ?x \<in> ?A \<longrightarrow> ?x \<in> ?B

goal (1 subgoal):
 1. b \<oplus> x \<notin> A
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b \<oplus> x \<notin> A

goal (1 subgoal):
 1. stabilizer A = stabilizer B \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
b \<oplus> x \<notin> A

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms heq stabilizer_coset_subset subset_trans
[PROOF STATE]
proof (prove)
using this:
b \<oplus> x \<notin> A
A \<subseteq> sumset {x} (stabilizer B)
x \<in> A
\<not> sumset {x} (stabilizer B) \<subseteq> C
A \<subseteq> C
C \<subseteq> G
stabilizer A = stabilizer B
\<lbrakk>?A \<subseteq> G; ?x \<in> ?A\<rbrakk> \<Longrightarrow> sumset {?x} (stabilizer ?A) \<subseteq> ?A
\<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> ?C\<rbrakk> \<Longrightarrow> ?A \<subseteq> ?C

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer A \<inter> stabilizer B \<Longrightarrow> x \<in> stabilizer (A \<union> B)
[PROOF STEP]
have "sumset {x} (B \<inter> G) = (B \<inter> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} (B \<inter> G) = B \<inter> G
[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 A \<inter> stabilizer B

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

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

goal (1 subgoal):
 1. sumset {x} ((A \<union> B) \<inter> G) = (A \<union> B) \<inter> G
[PROOF STEP]
using sumset_subset_Un2
    boolean_algebra.conj_disj_distrib2
[PROOF STATE]
proof (prove)
using this:
sumset {x} (A \<inter> G) = A \<inter> G
sumset {x} (B \<inter> G) = B \<inter> G
sumset ?A (?B \<union> ?B') = sumset ?A ?B \<union> sumset ?A ?B'
inf (sup ?y ?z) ?x = sup (inf ?y ?x) (inf ?z ?x)

goal (1 subgoal):
 1. sumset {x} ((A \<union> B) \<inter> G) = (A \<union> B) \<inter> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sumset {x} ((A \<union> B) \<inter> G) = (A \<union> B) \<inter> G

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mem_stabilizer_Un_and_left_imp_right:
  assumes "finite B" and "x \<in> stabilizer (A \<union> B)" and "x \<in> stabilizer A" and "disjnt A B"
  shows "x \<in> stabilizer B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> stabilizer B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> stabilizer B
[PROOF STEP]
have "(A \<inter> G) \<union> sumset {x} (B \<inter> G) = (A \<inter> G) \<union> (B \<inter> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> G \<union> sumset {x} (B \<inter> G) = A \<inter> G \<union> B \<inter> G
[PROOF STEP]
using assms(2) sumset_subset_Un2[of "{x}" "A \<inter> G" "B \<inter> G"] stabilizer_def[of "A \<union> B"]
    Int_Un_distrib2[of "A" "B" "G"] assms(3) stabilizer_def
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer (A \<union> B)
sumset {x} (A \<inter> G \<union> B \<inter> G) = sumset {x} (A \<inter> G) \<union> sumset {x} (B \<inter> G)
stabilizer (A \<union> B) \<equiv> {x \<in> G. sumset {x} ((A \<union> B) \<inter> G) = (A \<union> B) \<inter> G}
(A \<union> B) \<inter> G = A \<inter> G \<union> B \<inter> G
x \<in> stabilizer A
stabilizer ?S \<equiv> {x \<in> G. sumset {x} (?S \<inter> G) = ?S \<inter> G}

goal (1 subgoal):
 1. A \<inter> G \<union> sumset {x} (B \<inter> G) = A \<inter> G \<union> B \<inter> G
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
A \<inter> G \<union> sumset {x} (B \<inter> G) = A \<inter> G \<union> B \<inter> G

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

goal (1 subgoal):
 1. B \<inter> G \<subseteq> sumset {x} (B \<inter> G)
[PROOF STEP]
using assms(4) disjnt_def Int_Un_distrib2 Int_commute
    sumset_subset_Un1
[PROOF STATE]
proof (prove)
using this:
A \<inter> G \<union> sumset {x} (B \<inter> G) = A \<inter> G \<union> B \<inter> G
disjnt A B
disjnt ?A ?B = (?A \<inter> ?B = {})
(?B \<union> ?C) \<inter> ?A = ?B \<inter> ?A \<union> ?C \<inter> ?A
?A \<inter> ?B = ?B \<inter> ?A
sumset (?A \<union> ?A') ?B = sumset ?A ?B \<union> sumset ?A' ?B

goal (1 subgoal):
 1. B \<inter> G \<subseteq> sumset {x} (B \<inter> G)
[PROOF STEP]
by (smt (verit, del_insts) Int_assoc Un_Int_eq(2) inf.orderI insert_is_Un
    sumset_empty(2))
[PROOF STATE]
proof (state)
this:
B \<inter> G \<subseteq> sumset {x} (B \<inter> G)

goal (1 subgoal):
 1. x \<in> stabilizer B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<inter> G \<subseteq> sumset {x} (B \<inter> G)
[PROOF STEP]
show "x \<in> stabilizer B"
[PROOF STATE]
proof (prove)
using this:
B \<inter> G \<subseteq> sumset {x} (B \<inter> G)

goal (1 subgoal):
 1. x \<in> stabilizer B
[PROOF STEP]
using stabilizer_def[of "B"] assms(1) assms(3) card_subset_eq
    card_sumset_singleton_subset_eq finite.emptyI finite.insertI finite_Int finite_sumset
    inf.cobounded2 stabilizer_subset_group subsetD
[PROOF STATE]
proof (prove)
using this:
B \<inter> G \<subseteq> sumset {x} (B \<inter> G)
stabilizer B \<equiv> {x \<in> G. sumset {x} (B \<inter> G) = B \<inter> G}
finite B
x \<in> stabilizer A
\<lbrakk>finite ?B; ?A \<subseteq> ?B; card ?A = card ?B\<rbrakk> \<Longrightarrow> ?A = ?B
\<lbrakk>?a \<in> G; ?A \<subseteq> G\<rbrakk> \<Longrightarrow> card (sumset {?a} ?A) = card ?A
finite {}
finite ?A \<Longrightarrow> finite (insert ?a ?A)
finite ?F \<or> finite ?G \<Longrightarrow> finite (?F \<inter> ?G)
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
inf ?a ?b \<le> ?b
stabilizer ?S \<subseteq> G
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B

goal (1 subgoal):
 1. x \<in> stabilizer B
[PROOF STEP]
by (smt (verit) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mem_stabilizer_Un_and_right_imp_left:
  assumes "finite A" and "x \<in> stabilizer (A \<union> B)" and "x \<in> stabilizer B" and "disjnt A B"
  shows "x \<in> stabilizer A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> stabilizer A
[PROOF STEP]
using mem_stabilizer_Un_and_left_imp_right Un_commute assms disjnt_sym
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?x \<in> stabilizer (?A \<union> ?B); ?x \<in> stabilizer ?A; disjnt ?A ?B\<rbrakk> \<Longrightarrow> ?x \<in> stabilizer ?B
?A \<union> ?B = ?B \<union> ?A
finite A
x \<in> stabilizer (A \<union> B)
x \<in> stabilizer B
disjnt A B
disjnt ?A ?B \<Longrightarrow> disjnt ?B ?A

goal (1 subgoal):
 1. x \<in> stabilizer A
[PROOF STEP]
by metis


[STATEMENT]
lemma Union_stabilizer_Class_eq:
  assumes "A \<subseteq> G"
  shows "A = (\<Union> (Class A ` A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = \<Union> (Class A ` A)
[PROOF STEP]
using assms sumset_commute sumset_subgroup_eq_Class_Union
  sumset_stabilizer_eq_self
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
sumset ?A ?B = sumset ?B ?A
?A \<subseteq> G \<Longrightarrow> sumset ?A (stabilizer ?Aa) = \<Union> (Class ?Aa ` ?A)
?A \<subseteq> G \<Longrightarrow> sumset (stabilizer ?A) ?A = ?A

goal (1 subgoal):
 1. A = \<Union> (Class A ` A)
[PROOF STEP]
by presburger


[STATEMENT]
lemma card_stabilizer_sumset_divide_sumset:
  "card (stabilizer (sumset A B)) dvd card (sumset A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (stabilizer (sumset A B)) dvd card (sumset A B)
[PROOF STEP]
using card_divide_sumset
  sumset_commute sumset_stabilizer_eq_self sumset_subset_carrier
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> G \<Longrightarrow> card (stabilizer ?Aa) dvd card (sumset ?A (stabilizer ?Aa))
sumset ?A ?B = sumset ?B ?A
?A \<subseteq> G \<Longrightarrow> sumset (stabilizer ?A) ?A = ?A
sumset ?A ?B \<subseteq> G

goal (1 subgoal):
 1. card (stabilizer (sumset A B)) dvd card (sumset A B)
[PROOF STEP]
by metis


[STATEMENT]
lemma card_stabilizer_le:
  assumes "A \<subseteq> G" and "finite A" and "A \<noteq> {}"
  shows "card (stabilizer A) \<le> card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (stabilizer A) \<le> card A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
finite A
A \<noteq> {}

goal (1 subgoal):
 1. card (stabilizer A) \<le> card A
[PROOF STEP]
by (metis card_le_sumset finite.cases insertCI insert_subset stabilizer_finite
    stabilizer_subset_group sumset_commute sumset_stabilizer_eq_self)


[STATEMENT]
lemma sumset_Inter_subset_sumset:
  assumes "a \<in> G" and "b \<in> G"
  shows "sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<subseteq>
    sumset {a \<oplus> b} (stabilizer C)" (is "sumset ?A ?B \<subseteq> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<subseteq> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<Longrightarrow> x \<in> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<Longrightarrow> x \<in> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
assume "x \<in> sumset ?A ?B"
[PROOF STATE]
proof (state)
this:
x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))

goal (1 subgoal):
 1. \<And>x. x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<Longrightarrow> x \<in> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
[PROOF STEP]
obtain d1 d2 where "d1 \<in> sumset {a} (stabilizer C)" and
    "d2 \<in> sumset {b} (stabilizer C)" and "x = d1 \<oplus> d2"
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))

goal (1 subgoal):
 1. (\<And>d1 d2. \<lbrakk>d1 \<in> sumset {a} (stabilizer C); d2 \<in> sumset {b} (stabilizer C); x = d1 \<oplus> d2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson IntD2 sumset.cases)
[PROOF STATE]
proof (state)
this:
d1 \<in> sumset {a} (stabilizer C)
d2 \<in> sumset {b} (stabilizer C)
x = d1 \<oplus> d2

goal (1 subgoal):
 1. \<And>x. x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<Longrightarrow> x \<in> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d1 \<in> sumset {a} (stabilizer C)
d2 \<in> sumset {b} (stabilizer C)
x = d1 \<oplus> d2
[PROOF STEP]
obtain c1 c2 where hc1: "c1 \<in> stabilizer C" and hc2: "c2 \<in> stabilizer C" and
    "x = (a \<oplus> c1) \<oplus> (b \<oplus> c2)"
[PROOF STATE]
proof (prove)
using this:
d1 \<in> sumset {a} (stabilizer C)
d2 \<in> sumset {b} (stabilizer C)
x = d1 \<oplus> d2

goal (1 subgoal):
 1. (\<And>c1 c2. \<lbrakk>c1 \<in> stabilizer C; c2 \<in> stabilizer C; x = a \<oplus> c1 \<oplus> (b \<oplus> c2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sumset.simps
[PROOF STATE]
proof (prove)
using this:
d1 \<in> sumset {a} (stabilizer C)
d2 \<in> sumset {b} (stabilizer C)
x = d1 \<oplus> d2
(?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)

goal (1 subgoal):
 1. (\<And>c1 c2. \<lbrakk>c1 \<in> stabilizer C; c2 \<in> stabilizer C; x = a \<oplus> c1 \<oplus> (b \<oplus> c2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c1 \<in> stabilizer C
c2 \<in> stabilizer C
x = a \<oplus> c1 \<oplus> (b \<oplus> c2)

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

goal (1 subgoal):
 1. x = a \<oplus> b \<oplus> (c1 \<oplus> c2)
[PROOF STEP]
using hc1 hc2 assms associative commutative
    stabilizer_subset_group
[PROOF STATE]
proof (prove)
using this:
c1 \<in> stabilizer C
c2 \<in> stabilizer C
x = a \<oplus> c1 \<oplus> (b \<oplus> c2)
c1 \<in> stabilizer C
c2 \<in> stabilizer C
a \<in> G
b \<in> G
\<lbrakk>?a \<in> G; ?b \<in> G; ?c \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<oplus> ?c = ?a \<oplus> (?b \<oplus> ?c)
\<lbrakk>?x \<in> G; ?y \<in> G\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y = ?y \<oplus> ?x
stabilizer ?S \<subseteq> G

goal (1 subgoal):
 1. x = a \<oplus> b \<oplus> (c1 \<oplus> c2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = a \<oplus> b \<oplus> (c1 \<oplus> c2)

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

goal (1 subgoal):
 1. x \<in> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
using stabilizer_is_subgroup hc1 hc2
    stabilizer_subset_group sumset.simps sumset_stabilizer_eq assms
[PROOF STATE]
proof (prove)
using this:
x = a \<oplus> b \<oplus> (c1 \<oplus> c2)
subgroup (stabilizer ?S) G (\<oplus>) \<zero>
c1 \<in> stabilizer C
c2 \<in> stabilizer C
stabilizer ?S \<subseteq> G
(?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 (stabilizer ?A) (stabilizer ?A) = stabilizer ?A
a \<in> G
b \<in> G

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convergent_set_sub_powerset:
  "convergent_set A B \<subseteq> Pow (sumset A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent_set A B \<subseteq> Pow (sumset A B)
[PROOF STEP]
using convergent_set_def convergent_def
[PROOF STATE]
proof (prove)
using this:
convergent_set ?A ?B = {C. local.convergent C ?A ?B}
local.convergent ?C ?A ?B \<equiv> ?C \<subseteq> sumset ?A ?B \<and> ?C \<noteq> {} \<and> card (?A \<inter> ?B) + card (sumset (?A \<union> ?B) (stabilizer ?C)) \<le> card ?C + card (stabilizer ?C)

goal (1 subgoal):
 1. convergent_set A B \<subseteq> Pow (sumset A B)
[PROOF STEP]
by blast


[STATEMENT]
lemma finite_convergent_set:
  assumes "finite A" and "finite B"
  shows "finite (convergent_set A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (convergent_set A B)
[PROOF STEP]
using convergent_set_sub_powerset finite_Pow_iff finite_sumset assms finite_subset
[PROOF STATE]
proof (prove)
using this:
convergent_set ?A ?B \<subseteq> Pow (sumset ?A ?B)
finite (Pow ?A) = finite ?A
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
finite A
finite B
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (convergent_set A B)
[PROOF STEP]
by metis


[STATEMENT]
lemma stabilizer_sumset_psubset_stabilizer:
  assumes "a \<in> G" and "b \<in> G" and "A \<inter> sumset {a} (stabilizer C) \<noteq> {}" and
  "B \<inter> sumset {b} (stabilizer C) \<noteq> {}" and hnotsub: "\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B"
  shows "stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset>
    stabilizer C" (is "?H \<subset> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer C
 2. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
have "sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> G
b \<in> G
A \<inter> sumset {a} (stabilizer C) \<noteq> {}
B \<inter> sumset {b} (stabilizer C) \<noteq> {}
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B

goal (1 subgoal):
 1. sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}
[PROOF STEP]
by (simp add: inf_assoc)
[PROOF STATE]
proof (state)
this:
sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}

goal (2 subgoals):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer C
 2. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}
[PROOF STEP]
show "?H \<subseteq> stabilizer C"
[PROOF STATE]
proof (prove)
using this:
sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer C
[PROOF STEP]
by (meson assms(1) assms(2) composition_closed subset_stabilizer_of_subset_sumset sumset_Inter_subset_sumset sumset_subset_carrier)
[PROOF STATE]
proof (state)
this:
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer C

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
obtain c1 c2 where "a \<oplus> c1 \<in> A" and "b \<oplus> c2 \<in> B" and hc1: "c1 \<in> stabilizer C" and hc2: "c2 \<in> stabilizer C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c1 c2. \<lbrakk>a \<oplus> c1 \<in> A; b \<oplus> c2 \<in> B; c1 \<in> stabilizer C; c2 \<in> stabilizer C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1, 2, 3, 4) Left_Coset_eq_sumset_stabilizer
[PROOF STATE]
proof (prove)
using this:
a \<in> G
b \<in> G
A \<inter> sumset {a} (stabilizer C) \<noteq> {}
B \<inter> sumset {b} (stabilizer C) \<noteq> {}
?x \<in> G \<Longrightarrow> sumset {?x} (stabilizer ?B) = ?x \<cdot>| stabilizer ?B

goal (1 subgoal):
 1. (\<And>c1 c2. \<lbrakk>a \<oplus> c1 \<in> A; b \<oplus> c2 \<in> B; c1 \<in> stabilizer C; c2 \<in> stabilizer C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a \<oplus> c1 \<in> A
b \<oplus> c2 \<in> B
c1 \<in> stabilizer C
c2 \<in> stabilizer C

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<oplus> c1 \<in> A
b \<oplus> c2 \<in> B
c1 \<in> stabilizer C
c2 \<in> stabilizer C
[PROOF STEP]
have hac1mem: "(a \<oplus> c1) \<in> A \<inter> sumset {a} (stabilizer C)" and hac1G: "a \<oplus> c1 \<in> G" and
    hbc2mem: "(b \<oplus> c2) \<in> B \<inter> sumset {b} (stabilizer C)" and hbc2G: "b \<oplus> c2 \<in> G"
[PROOF STATE]
proof (prove)
using this:
a \<oplus> c1 \<in> A
b \<oplus> c2 \<in> B
c1 \<in> stabilizer C
c2 \<in> stabilizer C

goal (1 subgoal):
 1. (a \<oplus> c1 \<in> A \<inter> sumset {a} (stabilizer C) &&& a \<oplus> c1 \<in> G) &&& b \<oplus> c2 \<in> B \<inter> sumset {b} (stabilizer C) &&& b \<oplus> c2 \<in> G
[PROOF STEP]
by (auto simp add: assms(1, 2) sumset.sumsetI)
[PROOF STATE]
proof (state)
this:
a \<oplus> c1 \<in> A \<inter> sumset {a} (stabilizer C)
a \<oplus> c1 \<in> G
b \<oplus> c2 \<in> B \<inter> sumset {b} (stabilizer C)
b \<oplus> c2 \<in> G

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
have "(a \<oplus> c1) \<oplus> (b \<oplus> c2) \<in> sumset {a \<oplus> b} (stabilizer C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<oplus> c1 \<oplus> (b \<oplus> c2) \<in> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
using assms hc1 hc2
[PROOF STATE]
proof (prove)
using this:
a \<in> G
b \<in> G
A \<inter> sumset {a} (stabilizer C) \<noteq> {}
B \<inter> sumset {b} (stabilizer C) \<noteq> {}
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B
c1 \<in> stabilizer C
c2 \<in> stabilizer C

goal (1 subgoal):
 1. a \<oplus> c1 \<oplus> (b \<oplus> c2) \<in> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
by (smt (verit) associative commutative composition_closed insertI1 sub sub_composition_closed sumset.sumsetI)
[PROOF STATE]
proof (state)
this:
a \<oplus> c1 \<oplus> (b \<oplus> c2) \<in> sumset {a \<oplus> b} (stabilizer C)

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<oplus> c1 \<oplus> (b \<oplus> c2) \<in> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
have "sumset {a \<oplus> b} (stabilizer C) \<inter>  sumset {(a \<oplus> c1) \<oplus> (b \<oplus> c2)} (stabilizer C) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
a \<oplus> c1 \<oplus> (b \<oplus> c2) \<in> sumset {a \<oplus> b} (stabilizer C)

goal (1 subgoal):
 1. sumset {a \<oplus> b} (stabilizer C) \<inter> sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C) \<noteq> {}
[PROOF STEP]
using zero_mem_stabilizer
[PROOF STATE]
proof (prove)
using this:
a \<oplus> c1 \<oplus> (b \<oplus> c2) \<in> sumset {a \<oplus> b} (stabilizer C)
\<zero> \<in> stabilizer ?A

goal (1 subgoal):
 1. sumset {a \<oplus> b} (stabilizer C) \<inter> sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C) \<noteq> {}
[PROOF STEP]
by (smt (verit, ccfv_threshold) composition_closed
      disjoint_iff_not_equal hac1G hbc2G insertCI right_unit sumset.sumsetI unit_closed)
[PROOF STATE]
proof (state)
this:
sumset {a \<oplus> b} (stabilizer C) \<inter> sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C) \<noteq> {}

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sumset {a \<oplus> b} (stabilizer C) \<inter> sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C) \<noteq> {}
[PROOF STEP]
have hsumeq: "sumset {a \<oplus> b} (stabilizer C) = sumset {(a \<oplus> c1) \<oplus> (b \<oplus> c2)} (stabilizer C)"
[PROOF STATE]
proof (prove)
using this:
sumset {a \<oplus> b} (stabilizer C) \<inter> sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C) \<noteq> {}

goal (1 subgoal):
 1. sumset {a \<oplus> b} (stabilizer C) = sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C)
[PROOF STEP]
using sumset_stabilizer_eq_iff assms hac1G hbc2G composition_closed
[PROOF STATE]
proof (prove)
using this:
sumset {a \<oplus> b} (stabilizer C) \<inter> sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C) \<noteq> {}
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> (sumset {?a} (stabilizer ?A) = sumset {?b} (stabilizer ?A)) = (sumset {?a} (stabilizer ?A) \<inter> sumset {?b} (stabilizer ?A) \<noteq> {})
a \<in> G
b \<in> G
A \<inter> sumset {a} (stabilizer C) \<noteq> {}
B \<inter> sumset {b} (stabilizer C) \<noteq> {}
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B
a \<oplus> c1 \<in> G
b \<oplus> c2 \<in> G
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> G

goal (1 subgoal):
 1. sumset {a \<oplus> b} (stabilizer C) = sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
sumset {a \<oplus> b} (stabilizer C) = sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C)

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
have "(sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> sumset {a \<oplus> b} (stabilizer C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<subseteq> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
by (simp add: assms(1, 2) sumset_Inter_subset_sumset)
[PROOF STATE]
proof (state)
this:
sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<subseteq> sumset {a \<oplus> b} (stabilizer C)

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
have hsummem: "(a \<oplus> c1) \<oplus> (b \<oplus> c2) \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<oplus> c1 \<oplus> (b \<oplus> c2) \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
[PROOF STEP]
using hac1mem hbc2mem hac1G hbc2G sumset.sumsetI
[PROOF STATE]
proof (prove)
using this:
a \<oplus> c1 \<in> A \<inter> sumset {a} (stabilizer C)
b \<oplus> c2 \<in> B \<inter> sumset {b} (stabilizer C)
a \<oplus> c1 \<in> G
b \<oplus> c2 \<in> G
\<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. a \<oplus> c1 \<oplus> (b \<oplus> c2) \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<oplus> c1 \<oplus> (b \<oplus> c2) \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
show "?H \<noteq> stabilizer C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
using stabilizer_neq_subset_sumset[OF _ hsummem] hnotsub hsumeq sumset_Inter_subset_sumset assms
      sumset_subset_carrier composition_closed sumset_mono sumset.sumsetI zero_mem_stabilizer
      inf.cobounded1 right_unit unit_closed
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<subseteq> sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer ?B); \<not> sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer ?B) \<subseteq> ?C; sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<subseteq> ?C; ?C \<subseteq> G\<rbrakk> \<Longrightarrow> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer ?B
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B
sumset {a \<oplus> b} (stabilizer C) = sumset {a \<oplus> c1 \<oplus> (b \<oplus> c2)} (stabilizer C)
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> sumset (?A \<inter> sumset {?a} (stabilizer ?C)) (?B \<inter> sumset {?b} (stabilizer ?C)) \<subseteq> sumset {?a \<oplus> ?b} (stabilizer ?C)
a \<in> G
b \<in> G
A \<inter> sumset {a} (stabilizer C) \<noteq> {}
B \<inter> sumset {b} (stabilizer C) \<noteq> {}
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B
sumset ?A ?B \<subseteq> G
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> G
\<lbrakk>?A' \<subseteq> ?A; ?B' \<subseteq> ?B\<rbrakk> \<Longrightarrow> sumset ?A' ?B' \<subseteq> sumset ?A ?B
\<lbrakk>?a \<in> ?A; ?a \<in> G; ?b \<in> ?B; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> sumset ?A ?B
\<zero> \<in> stabilizer ?A
inf ?a ?b \<le> ?a
?a \<in> G \<Longrightarrow> ?a \<oplus> \<zero> = ?a
\<zero> \<in> G

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<noteq> stabilizer C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stabilizer_eq_stabilizer_union:
  assumes "a \<in> G" and "b \<in> G" and"A \<inter> sumset {a} (stabilizer C) \<noteq> {}" and
  "B \<inter> sumset {b} (stabilizer C) \<noteq> {}" and hnotsub: "\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B" and
  "C \<subseteq> sumset A B" and "finite C" and
  "C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {}" and "C \<noteq> {}" and
  "finite A" and "finite B"
  shows "stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) =
    stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))" (is "stabilizer ?H = stabilizer ?K")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) = stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
 2. stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
show "stabilizer ?H \<subseteq> stabilizer ?K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
using subset_stabilizer_Un Int_absorb1
    stabilizer_sumset_psubset_stabilizer psubset_imp_subset assms
[PROOF STATE]
proof (prove)
using this:
stabilizer ?A \<inter> stabilizer ?B \<subseteq> stabilizer (?A \<union> ?B)
?B \<subseteq> ?A \<Longrightarrow> ?A \<inter> ?B = ?B
\<lbrakk>?a \<in> G; ?b \<in> G; ?A \<inter> sumset {?a} (stabilizer ?C) \<noteq> {}; ?B \<inter> sumset {?b} (stabilizer ?C) \<noteq> {}; \<not> sumset {?a \<oplus> ?b} (stabilizer ?C) \<subseteq> sumset ?A ?B\<rbrakk> \<Longrightarrow> stabilizer (sumset (?A \<inter> sumset {?a} (stabilizer ?C)) (?B \<inter> sumset {?b} (stabilizer ?C))) \<subset> stabilizer ?C
?A \<subset> ?B \<Longrightarrow> ?A \<subseteq> ?B
a \<in> G
b \<in> G
A \<inter> sumset {a} (stabilizer C) \<noteq> {}
B \<inter> sumset {b} (stabilizer C) \<noteq> {}
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B
C \<subseteq> sumset A B
finite C
C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {}
C \<noteq> {}
finite A
finite B

goal (1 subgoal):
 1. stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))

goal (1 subgoal):
 1. stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
have hCG : "C \<subseteq> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<subseteq> G
[PROOF STEP]
using assms(6) sumset_subset_carrier
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> sumset A B
sumset ?A ?B \<subseteq> G

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

goal (1 subgoal):
 1. stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
show "stabilizer ?K \<subseteq> stabilizer ?H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subseteq> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<Longrightarrow> x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<Longrightarrow> x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
assume hxC1: "x \<in> stabilizer ?K"
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<Longrightarrow> x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<Longrightarrow> x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
have "x \<in> stabilizer C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> stabilizer C
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> stabilizer C
[PROOF STEP]
have hC_Un: "C = (\<Union> (Class C ` C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C = \<Union> (Class C ` C)
[PROOF STEP]
using Union_stabilizer_Class_eq hCG
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> G \<Longrightarrow> ?A = \<Union> (Class ?A ` ?A)
C \<subseteq> G

goal (1 subgoal):
 1. C = \<Union> (Class C ` C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C = \<Union> (Class C ` C)

goal (1 subgoal):
 1. x \<in> stabilizer C
[PROOF STEP]
have hCsumx: "sumset {x} C = (\<Union> y \<in> Class C ` C. sumset {x} y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} C = \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sumset {x} C \<subseteq> \<Union> (sumset {x} ` Class C ` C)
 2. \<Union> (sumset {x} ` Class C ` C) \<subseteq> sumset {x} C
[PROOF STEP]
show "sumset {x} C \<subseteq> \<Union> (sumset {x} ` Class C ` C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} C \<subseteq> \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} C \<Longrightarrow> xa \<in> \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} C \<Longrightarrow> xa \<in> \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
assume hy: "y \<in> sumset {x} C"
[PROOF STATE]
proof (state)
this:
y \<in> sumset {x} C

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} C \<Longrightarrow> xa \<in> \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> sumset {x} C
[PROOF STEP]
obtain c where hc: "c \<in> C" and hyxc: "y = x \<oplus> c"
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {x} C

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> C; y = x \<oplus> c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sumset.cases
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {x} C
\<lbrakk>?a \<in> sumset ?A ?B; \<And>a b. \<lbrakk>?a = a \<oplus> b; a \<in> ?A; a \<in> G; b \<in> ?B; b \<in> G\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} C \<Longrightarrow> xa \<in> \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> C
y = x \<oplus> c
[PROOF STEP]
obtain K where hK: "K \<in> Class C ` C" and "c \<in> K"
[PROOF STATE]
proof (prove)
using this:
c \<in> C
y = x \<oplus> c

goal (1 subgoal):
 1. (\<And>K. \<lbrakk>K \<in> Class C ` C; c \<in> K\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using hC_Un
[PROOF STATE]
proof (prove)
using this:
c \<in> C
y = x \<oplus> c
C = \<Union> (Class C ` C)

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

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} C \<Longrightarrow> xa \<in> \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
K \<in> Class C ` C
c \<in> K
[PROOF STEP]
have "y \<in> sumset {x} K"
[PROOF STATE]
proof (prove)
using this:
K \<in> Class C ` C
c \<in> K

goal (1 subgoal):
 1. y \<in> sumset {x} K
[PROOF STEP]
using hyxc hc
[PROOF STATE]
proof (prove)
using this:
K \<in> Class C ` C
c \<in> K
y = x \<oplus> c
c \<in> C

goal (1 subgoal):
 1. y \<in> sumset {x} K
[PROOF STEP]
by (metis sumset.cases
            sumset.sumsetI hCG hy singletonD subset_iff)
[PROOF STATE]
proof (state)
this:
y \<in> sumset {x} K

goal (1 subgoal):
 1. \<And>xa. xa \<in> sumset {x} C \<Longrightarrow> xa \<in> \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> sumset {x} K
[PROOF STEP]
show "y \<in> \<Union> (sumset {x} ` Class C ` C)"
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {x} K

goal (1 subgoal):
 1. y \<in> \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
using hK
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {x} K
K \<in> Class C ` C

goal (1 subgoal):
 1. y \<in> \<Union> (sumset {x} ` Class C ` C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> \<Union> (sumset {x} ` Class C ` C)

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

goal (1 subgoal):
 1. \<Union> (sumset {x} ` Class C ` C) \<subseteq> sumset {x} C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (sumset {x} ` Class C ` C) \<subseteq> sumset {x} C
[PROOF STEP]
show "\<Union> (sumset {x} ` Class C ` C) \<subseteq> sumset {x} C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (sumset {x} ` Class C ` C) \<subseteq> sumset {x} C
[PROOF STEP]
proof(intro Union_least)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. X \<in> sumset {x} ` Class C ` C \<Longrightarrow> X \<subseteq> sumset {x} C
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. X \<in> sumset {x} ` Class C ` C \<Longrightarrow> X \<subseteq> sumset {x} C
[PROOF STEP]
assume "X \<in> sumset {x} ` Class C ` C"
[PROOF STATE]
proof (state)
this:
X \<in> sumset {x} ` Class C ` C

goal (1 subgoal):
 1. \<And>X. X \<in> sumset {x} ` Class C ` C \<Longrightarrow> X \<subseteq> sumset {x} C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<in> sumset {x} ` Class C ` C
[PROOF STEP]
obtain K where "K \<in> Class C ` C" and "X = sumset {x} K"
[PROOF STATE]
proof (prove)
using this:
X \<in> sumset {x} ` Class C ` C

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

goal (1 subgoal):
 1. \<And>X. X \<in> sumset {x} ` Class C ` C \<Longrightarrow> X \<subseteq> sumset {x} C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
K \<in> Class C ` C
X = sumset {x} K
[PROOF STEP]
show "X \<subseteq> sumset {x} C"
[PROOF STATE]
proof (prove)
using this:
K \<in> Class C ` C
X = sumset {x} K

goal (1 subgoal):
 1. X \<subseteq> sumset {x} C
[PROOF STEP]
using sumset_mono[of "{x}" "{x}" "K" "C"]
            hC_Un subset_refl
[PROOF STATE]
proof (prove)
using this:
K \<in> Class C ` C
X = sumset {x} K
\<lbrakk>{x} \<subseteq> {x}; K \<subseteq> C\<rbrakk> \<Longrightarrow> sumset {x} K \<subseteq> sumset {x} C
C = \<Union> (Class C ` C)
?A \<subseteq> ?A

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sumset {x} C = \<Union> (sumset {x} ` Class C ` C)

goal (1 subgoal):
 1. x \<in> stabilizer C
[PROOF STEP]
have "x \<notin> stabilizer C \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
assume hxC: "x \<notin> stabilizer C"
[PROOF STATE]
proof (state)
this:
x \<notin> stabilizer C

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> stabilizer C
[PROOF STEP]
have hxG: "x \<in> G"
[PROOF STATE]
proof (prove)
using this:
x \<notin> stabilizer C

goal (1 subgoal):
 1. x \<in> G
[PROOF STEP]
using hxC1 stabilizer_subset_group
[PROOF STATE]
proof (prove)
using this:
x \<notin> stabilizer C
x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
stabilizer ?S \<subseteq> G

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

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> G
[PROOF STEP]
have hxCne: "sumset {x} C \<noteq> C"
[PROOF STATE]
proof (prove)
using this:
x \<in> G

goal (1 subgoal):
 1. sumset {x} C \<noteq> C
[PROOF STEP]
using stabilizer_def[of "C"] hCG Int_absorb2
        hxC
[PROOF STATE]
proof (prove)
using this:
x \<in> G
stabilizer C \<equiv> {x \<in> G. sumset {x} (C \<inter> G) = C \<inter> G}
C \<subseteq> G
?A \<subseteq> ?B \<Longrightarrow> ?A \<inter> ?B = ?A
x \<notin> stabilizer C

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

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sumset {x} C \<noteq> C

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
have hxsplit: "sumset {x} C \<union> sumset {x} ?H = C \<union> ?H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} C \<union> sumset {x} (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) = C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
[PROOF STEP]
using hxC1 stabilizer_def[of "?K"] sumset_subset_carrier assms(6) sumset_subset_Un2
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<equiv> {x \<in> G. sumset {x} ((C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<inter> G) = (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<inter> G}
sumset ?A ?B \<subseteq> G
C \<subseteq> sumset A B
sumset ?A (?B \<union> ?B') = sumset ?A ?B \<union> sumset ?A ?B'

goal (1 subgoal):
 1. sumset {x} C \<union> sumset {x} (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) = C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sumset {x} C \<union> sumset {x} (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) = C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
have "sumset {x} C \<inter> ?H \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sumset {x} C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {} \<Longrightarrow> False
[PROOF STEP]
assume "sumset {x} C \<inter> ?H = {}"
[PROOF STATE]
proof (state)
this:
sumset {x} C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {}

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

goal (1 subgoal):
 1. sumset {x} C \<subset> C
[PROOF STEP]
using hxsplit hxCne
[PROOF STATE]
proof (prove)
using this:
sumset {x} C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {}
sumset {x} C \<union> sumset {x} (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) = C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
sumset {x} C \<noteq> C

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

goal (1 subgoal):
 1. sumset {x} C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {} \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
sumset {x} C \<subset> C

goal (1 subgoal):
 1. False
[PROOF STEP]
using hCG assms(6) assms(7) hxC1 stabilizer_subset_group psubset_card_mono
[PROOF STATE]
proof (prove)
using this:
sumset {x} C \<subset> C
C \<subseteq> G
C \<subseteq> sumset A B
finite C
x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
stabilizer ?S \<subseteq> G
\<lbrakk>finite ?B; ?A \<subset> ?B\<rbrakk> \<Longrightarrow> card ?A < card ?B

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis card_sumset_singleton_eq sumset_Int_carrier sumset_commute
          sumset_stabilizer_eq_self hxG less_irrefl_nat)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sumset {x} C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sumset {x} C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}
[PROOF STEP]
obtain c where hc: "c \<in> C" and
        hxcne: "sumset {x} (Class C c) \<inter> ?H \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
sumset {x} C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}

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

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

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> C
sumset {x} (Class C c) \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}
[PROOF STEP]
have hxc: "sumset {x} (Class C c) = Class C (x \<oplus> c)"
[PROOF STATE]
proof (prove)
using this:
c \<in> C
sumset {x} (Class C c) \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}

goal (1 subgoal):
 1. sumset {x} (Class C c) = Class C (x \<oplus> c)
[PROOF STEP]
using hxG assms(6) Left_Coset_Class_unit Left_Coset_eq_sumset_stabilizer sumset_assoc
        sumset_singletons_eq composition_closed sumset.cases sumset_stabilizer_eq_self hCG
[PROOF STATE]
proof (prove)
using this:
c \<in> C
sumset {x} (Class C c) \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}
x \<in> G
C \<subseteq> sumset A B
?g \<in> G \<Longrightarrow> ?g \<cdot>| stabilizer ?A = Class ?A ?g
?x \<in> G \<Longrightarrow> sumset {?x} (stabilizer ?B) = ?x \<cdot>| stabilizer ?B
sumset (sumset ?A ?B) ?C = sumset ?A (sumset ?B ?C)
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> sumset {?a} {?b} = {?a \<oplus> ?b}
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> G
\<lbrakk>?a \<in> sumset ?A ?B; \<And>a b. \<lbrakk>?a = a \<oplus> b; a \<in> ?A; a \<in> G; b \<in> ?B; b \<in> G\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
?A \<subseteq> G \<Longrightarrow> sumset (stabilizer ?A) ?A = ?A
C \<subseteq> G

goal (1 subgoal):
 1. sumset {x} (Class C c) = Class C (x \<oplus> c)
[PROOF STEP]
by (smt (verit))
[PROOF STATE]
proof (state)
this:
sumset {x} (Class C c) = Class C (x \<oplus> c)

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
have hClassCempty: "Class C (x \<oplus> c) \<inter> C = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Class C (x \<oplus> c) \<inter> C = {}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Class C (x \<oplus> c) \<inter> C = {}
[PROOF STEP]
have "\<not> Class C (x \<oplus> c) \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Class C (x \<oplus> c) \<subseteq> C
[PROOF STEP]
using hxc hxcne assms(8)
[PROOF STATE]
proof (prove)
using this:
sumset {x} (Class C c) = Class C (x \<oplus> c)
sumset {x} (Class C c) \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> {}
C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {}

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

goal (1 subgoal):
 1. Class C (x \<oplus> c) \<inter> C = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Class C (x \<oplus> c) \<subseteq> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> Class C (x \<oplus> c) \<subseteq> C

goal (1 subgoal):
 1. Class C (x \<oplus> c) \<inter> C = {}
[PROOF STEP]
using Class_cover_imp_subset_or_disj[OF hC_Un _ hCG]
[PROOF STATE]
proof (prove)
using this:
\<not> Class C (x \<oplus> c) \<subseteq> C
?x \<in> G \<Longrightarrow> Class C ?x \<subseteq> C \<or> Class C ?x \<inter> C = {}

goal (1 subgoal):
 1. Class C (x \<oplus> c) \<inter> C = {}
[PROOF STEP]
by (meson composition_closed hCG hc hxG subsetD)
[PROOF STATE]
proof (state)
this:
Class C (x \<oplus> c) \<inter> C = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Class C (x \<oplus> c) \<inter> C = {}

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
have "Class C (x \<oplus> c) \<subseteq> sumset {x} C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Class C (x \<oplus> c) \<subseteq> sumset {x} C
[PROOF STEP]
using hCsumx hc hxc
[PROOF STATE]
proof (prove)
using this:
sumset {x} C = \<Union> (sumset {x} ` Class C ` C)
c \<in> C
sumset {x} (Class C c) = Class C (x \<oplus> c)

goal (1 subgoal):
 1. Class C (x \<oplus> c) \<subseteq> sumset {x} C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Class C (x \<oplus> c) \<subseteq> sumset {x} C

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Class C (x \<oplus> c) \<subseteq> sumset {x} C
[PROOF STEP]
have "Class C (x \<oplus> c) \<subseteq> ?H"
[PROOF STATE]
proof (prove)
using this:
Class C (x \<oplus> c) \<subseteq> sumset {x} C

goal (1 subgoal):
 1. Class C (x \<oplus> c) \<subseteq> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
[PROOF STEP]
using hClassCempty hxsplit
[PROOF STATE]
proof (prove)
using this:
Class C (x \<oplus> c) \<subseteq> sumset {x} C
Class C (x \<oplus> c) \<inter> C = {}
sumset {x} C \<union> sumset {x} (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) = C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))

goal (1 subgoal):
 1. Class C (x \<oplus> c) \<subseteq> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Class C (x \<oplus> c) \<subseteq> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Class C (x \<oplus> c) \<subseteq> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
have "card (Class C (x \<oplus> c)) = card (stabilizer C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (Class C (x \<oplus> c)) = card (stabilizer C)
[PROOF STEP]
using hxG hc hCG
        composition_closed Right_Coset_Class_unit Right_Coset_cardinality sumset_Int_carrier
        Class_cover_imp_subset_or_disj assms
[PROOF STATE]
proof (prove)
using this:
x \<in> G
c \<in> C
C \<subseteq> G
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> G
?g \<in> G \<Longrightarrow> Right_Coset (stabilizer ?A) ?g = Class ?A ?g
?x \<in> G \<Longrightarrow> card (Right_Coset (stabilizer ?A) ?x) = card (stabilizer ?A)
sumset ?A ?B \<inter> G = sumset ?A ?B
\<lbrakk>?A = \<Union> (Class ?B ` ?C); ?x \<in> G; ?C \<subseteq> G\<rbrakk> \<Longrightarrow> Class ?B ?x \<subseteq> ?A \<or> Class ?B ?x \<inter> ?A = {}
a \<in> G
b \<in> G
A \<inter> sumset {a} (stabilizer C) \<noteq> {}
B \<inter> sumset {b} (stabilizer C) \<noteq> {}
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B
C \<subseteq> sumset A B
finite C
C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {}
C \<noteq> {}
finite A
finite B

goal (1 subgoal):
 1. card (Class C (x \<oplus> c)) = card (stabilizer C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (Class C (x \<oplus> c)) = card (stabilizer C)

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sumset {x} C \<noteq> C
Class C (x \<oplus> c) \<subseteq> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
card (Class C (x \<oplus> c)) = card (stabilizer C)
[PROOF STEP]
have "card (stabilizer C) \<le> card ?H"
[PROOF STATE]
proof (prove)
using this:
sumset {x} C \<noteq> C
Class C (x \<oplus> c) \<subseteq> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
card (Class C (x \<oplus> c)) = card (stabilizer C)

goal (1 subgoal):
 1. card (stabilizer C) \<le> card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
using card_mono finite_sumset assms(10, 11) finite_Int
[PROOF STATE]
proof (prove)
using this:
sumset {x} C \<noteq> C
Class C (x \<oplus> c) \<subseteq> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))
card (Class C (x \<oplus> c)) = card (stabilizer C)
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
finite A
finite B
finite ?F \<or> finite ?G \<Longrightarrow> finite (?F \<inter> ?G)

goal (1 subgoal):
 1. card (stabilizer C) \<le> card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
card (stabilizer C) \<le> card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (stabilizer C) \<le> card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
have "card ?H < card (sumset {a \<oplus> b} (stabilizer C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) < card (sumset {a \<oplus> b} (stabilizer C))
[PROOF STEP]
proof (intro psubset_card_mono psubsetI sumset_Inter_subset_sumset assms(1) assms(2))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (sumset {a \<oplus> b} (stabilizer C))
 2. sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
show "finite (sumset {a \<oplus> b} (stabilizer C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (sumset {a \<oplus> b} (stabilizer C))
[PROOF STEP]
using stabilizer_finite assms finite_sumset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?S \<subseteq> G; ?S \<noteq> {}; finite ?S\<rbrakk> \<Longrightarrow> finite (stabilizer ?S)
a \<in> G
b \<in> G
A \<inter> sumset {a} (stabilizer C) \<noteq> {}
B \<inter> sumset {b} (stabilizer C) \<noteq> {}
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B
C \<subseteq> sumset A B
finite C
C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {}
C \<noteq> {}
finite A
finite B
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)

goal (1 subgoal):
 1. finite (sumset {a \<oplus> b} (stabilizer C))
[PROOF STEP]
by (simp add: hCG)
[PROOF STATE]
proof (state)
this:
finite (sumset {a \<oplus> b} (stabilizer C))

goal (1 subgoal):
 1. sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
show "?H \<noteq> sumset {a \<oplus> b} (stabilizer C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
using hnotsub sumset_mono
[PROOF STATE]
proof (prove)
using this:
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B
\<lbrakk>?A' \<subseteq> ?A; ?B' \<subseteq> ?B\<rbrakk> \<Longrightarrow> sumset ?A' ?B' \<subseteq> sumset ?A ?B

goal (1 subgoal):
 1. sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> sumset {a \<oplus> b} (stabilizer C)
[PROOF STEP]
by (metis Int_lower1)
[PROOF STATE]
proof (state)
this:
sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<noteq> sumset {a \<oplus> b} (stabilizer C)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) < card (sumset {a \<oplus> b} (stabilizer C))

goal (1 subgoal):
 1. x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (stabilizer C) \<le> card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) < card (sumset {a \<oplus> b} (stabilizer C))
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
card (stabilizer C) \<le> card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) < card (sumset {a \<oplus> b} (stabilizer C))

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(1, 2) stabilizer_subset_group
[PROOF STATE]
proof (prove)
using this:
card (stabilizer C) \<le> card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
card (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) < card (sumset {a \<oplus> b} (stabilizer C))
a \<in> G
b \<in> G
stabilizer ?S \<subseteq> G

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: card_sumset_singleton_subset_eq)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<notin> stabilizer C \<Longrightarrow> False

goal (1 subgoal):
 1. x \<in> stabilizer C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> stabilizer C \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> stabilizer C \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer C

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<Longrightarrow> x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer C

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<Longrightarrow> x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
have "finite ?H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
using finite_sumset assms(10, 11) finite_Int
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
finite A
finite B
finite ?F \<or> finite ?G \<Longrightarrow> finite (?F \<inter> ?G)

goal (1 subgoal):
 1. finite (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))

goal (1 subgoal):
 1. \<And>x. x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<Longrightarrow> x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
x \<in> stabilizer C
finite (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
show "x \<in> stabilizer ?H"
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
x \<in> stabilizer C
finite (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))

goal (1 subgoal):
 1. x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
using mem_stabilizer_Un_and_right_imp_left[of "?H" "x" "C"]
      disjnt_def assms Un_commute
[PROOF STATE]
proof (prove)
using this:
x \<in> stabilizer (C \<union> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
x \<in> stabilizer C
finite (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
\<lbrakk>finite (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))); x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) \<union> C); x \<in> stabilizer C; disjnt (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) C\<rbrakk> \<Longrightarrow> x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
disjnt ?A ?B = (?A \<inter> ?B = {})
a \<in> G
b \<in> G
A \<inter> sumset {a} (stabilizer C) \<noteq> {}
B \<inter> sumset {b} (stabilizer C) \<noteq> {}
\<not> sumset {a \<oplus> b} (stabilizer C) \<subseteq> sumset A B
C \<subseteq> sumset A B
finite C
C \<inter> sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)) = {}
C \<noteq> {}
finite A
finite B
?A \<union> ?B = ?B \<union> ?A

goal (1 subgoal):
 1. x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
[PROOF STEP]
by (metis disjoint_iff_not_equal)
[PROOF STATE]
proof (state)
this:
x \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))

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

goal:
No subgoals!
[PROOF STEP]
qed