[STATEMENT]
lemma sumset_inter_ineq:
  assumes "B \<inter> sumset {a} (stabilizer C) = {}" and "stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C" and
  "a \<in> A" and "a \<in> G" and "finite A" and "finite B" and "A \<noteq> {}" and "B \<noteq> {}" and "finite (stabilizer C)"
  shows "int (card (sumset (A \<union> B) (stabilizer C))) - card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) \<ge>
    int (card (stabilizer C)) - card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))"
  (is "int (card (sumset (A \<union> B) (stabilizer C))) - card (sumset (A \<union> B) ?H1) \<ge>
                int (card (stabilizer C)) - card (sumset ?A1 ?H1)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (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. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
have hfinsumH1:"finite (sumset (A \<union> B) ?H1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))
[PROOF STEP]
using finite_sumset assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
have hsubsumH1: "sumset (A \<union> B) ?H1 \<subseteq> sumset (A \<union> B) (stabilizer C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset (A \<union> B) (stabilizer C)
[PROOF STEP]
using sumset.cases assms
[PROOF STATE]
proof (prove)
using this:
\<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
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
have hsumH1card_le: "card (sumset (A \<union> B) ?H1) \<le> card (sumset (A \<union> B) (stabilizer C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) \<le> card (sumset (A \<union> B) (stabilizer C))
[PROOF STEP]
using card_mono finite_sumset stabilizer_finite assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
\<lbrakk>?S \<subseteq> G; ?S \<noteq> {}; finite ?S\<rbrakk> \<Longrightarrow> finite (stabilizer ?S)
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
have hsub: "sumset ?A1 ?H1 \<subseteq> sumset {a} (stabilizer C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset {a} (stabilizer C)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset {a} (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)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset {a} (stabilizer C)
[PROOF STEP]
assume "x \<in> sumset ?A1 ?H1"
[PROOF STATE]
proof (state)
this:
x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (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)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset {a} (stabilizer C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))
[PROOF STEP]
obtain h1 f where "h1 \<in> ?A1" and hf: "f \<in> ?H1" and
      hx: "x = h1 \<oplus> f"
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))

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

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> stabilizer C; h1 = a \<oplus> c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Int_iff empty_iff insert_iff sumset.cases)
[PROOF STATE]
proof (state)
this:
c \<in> stabilizer C
h1 = a \<oplus> c

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

goal (1 subgoal):
 1. c \<oplus> f \<in> stabilizer C
[PROOF STEP]
using hf assms(2) stabilizer_is_subgroup
      subgroup_def monoid_axioms Group_Theory.group.axioms(1)
      Group_Theory.monoid_def subset_iff psubset_imp_subset
[PROOF STATE]
proof (prove)
using this:
c \<in> stabilizer C
h1 = a \<oplus> c
f \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
subgroup (stabilizer ?S) G (\<oplus>) \<zero>
subgroup ?G ?M ?composition ?unit \<equiv> submonoid ?G ?M ?composition ?unit \<and> Group_Theory.group ?G ?composition ?unit
Group_Theory.monoid G (\<oplus>) \<zero>
Group_Theory.group ?G ?composition ?unit \<Longrightarrow> Group_Theory.monoid ?G ?composition ?unit
Group_Theory.monoid ?M ?composition ?unit \<equiv> ((\<forall>a b. a \<in> ?M \<longrightarrow> b \<in> ?M \<longrightarrow> ?composition a b \<in> ?M) \<and> ?unit \<in> ?M) \<and> (\<forall>a b c. a \<in> ?M \<longrightarrow> b \<in> ?M \<longrightarrow> c \<in> ?M \<longrightarrow> ?composition (?composition a b) c = ?composition a (?composition b c)) \<and> (\<forall>a. a \<in> ?M \<longrightarrow> ?composition ?unit a = a) \<and> (\<forall>a. a \<in> ?M \<longrightarrow> ?composition a ?unit = a)
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)
?A \<subset> ?B \<Longrightarrow> ?A \<subseteq> ?B

goal (1 subgoal):
 1. c \<oplus> f \<in> stabilizer C
[PROOF STEP]
by (smt (verit) stabilizer_subset_group sumset.sumsetI sumset_stabilizer_eq)
[PROOF STATE]
proof (state)
this:
c \<oplus> f \<in> stabilizer C

goal (1 subgoal):
 1. \<And>x. x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset {a} (stabilizer C)
[PROOF STEP]
have hcG: "c \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<in> G
[PROOF STEP]
using hc stabilizer_subset_group
[PROOF STATE]
proof (prove)
using this:
c \<in> stabilizer C
stabilizer ?S \<subseteq> G

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

goal (1 subgoal):
 1. \<And>x. x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset {a} (stabilizer C)
[PROOF STEP]
have hfG: "f \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> G
[PROOF STEP]
using hf stabilizer_subset_group
[PROOF STATE]
proof (prove)
using this:
f \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
stabilizer ?S \<subseteq> G

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

goal (1 subgoal):
 1. \<And>x. x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset {a} (stabilizer C)
[PROOF STEP]
show "x \<in> sumset {a} (stabilizer C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> sumset {a} (stabilizer C)
[PROOF STEP]
using hx hac assms stabilizer_subset_group hcf
[PROOF STATE]
proof (prove)
using this:
x = h1 \<oplus> f
h1 = a \<oplus> c
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)
stabilizer ?S \<subseteq> G
c \<oplus> f \<in> stabilizer C

goal (1 subgoal):
 1. x \<in> sumset {a} (stabilizer C)
[PROOF STEP]
using Left_Coset_eq_sumset_stabilizer Left_Coset_memI associative hcG hfG
[PROOF STATE]
proof (prove)
using this:
x = h1 \<oplus> f
h1 = a \<oplus> c
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)
stabilizer ?S \<subseteq> G
c \<oplus> f \<in> stabilizer C
?x \<in> G \<Longrightarrow> sumset {?x} (stabilizer ?B) = ?x \<cdot>| stabilizer ?B
?h \<in> ?H \<Longrightarrow> ?x \<oplus> ?h \<in> ?x \<cdot>| ?H
\<lbrakk>?a \<in> G; ?b \<in> G; ?c \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<oplus> ?c = ?a \<oplus> (?b \<oplus> ?c)
c \<in> G
f \<in> G

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

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

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
have "finite (sumset ?A1 ?H1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))
[PROOF STEP]
using finite_sumset assms stabilizer_finite finite_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)
\<lbrakk>?S \<subseteq> G; ?S \<noteq> {}; finite ?S\<rbrakk> \<Longrightarrow> finite (stabilizer ?S)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset {a} (stabilizer C)
finite (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))
[PROOF STEP]
have "card (sumset {a} (stabilizer C)) - card (sumset ?A1 ?H1) =
    card (sumset {a} (stabilizer C) - sumset ?A1 ?H1)"
[PROOF STATE]
proof (prove)
using this:
sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset {a} (stabilizer C)
finite (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))

goal (1 subgoal):
 1. card (sumset {a} (stabilizer C)) - card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) = card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))
[PROOF STEP]
using card_Diff_subset
[PROOF STATE]
proof (prove)
using this:
sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset {a} (stabilizer C)
finite (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))
\<lbrakk>finite ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> card (?A - ?B) = card ?A - card ?B

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

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
have "card (sumset ?A1 ?H1) \<le>  card (sumset {a} (stabilizer C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) \<le> card (sumset {a} (stabilizer C))
[PROOF STEP]
using card_mono hsub finite_sumset assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B
sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset {a} (stabilizer C)
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (sumset {a} (stabilizer C)) - card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) = card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))
card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) \<le> card (sumset {a} (stabilizer C))
[PROOF STEP]
have "int (card (sumset {a} (stabilizer C))) - card (sumset ?A1 ?H1) =
    card (sumset {a} (stabilizer C) - sumset ?A1 ?H1)"
[PROOF STATE]
proof (prove)
using this:
card (sumset {a} (stabilizer C)) - card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) = card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))
card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) \<le> card (sumset {a} (stabilizer C))

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

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
have "... \<le> card ((sumset (A \<union> B) (stabilizer C)) - (sumset (A \<union> B) ?H1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (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. int (card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
have "sumset {a} (stabilizer C) - sumset ?A1 ?H1 \<subseteq> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) ?H1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (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> sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (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> sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))
[PROOF STEP]
assume hx: "x \<in> sumset {a} (stabilizer C) - sumset ?A1 ?H1"
[PROOF STATE]
proof (state)
this:
x \<in> sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>x = a \<oplus> c; c \<in> stabilizer C; c \<in> G\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sumset.cases
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer 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>x = a \<oplus> c; c \<in> stabilizer C; c \<in> G\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = a \<oplus> c
c \<in> stabilizer C
c \<in> G

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

goal (1 subgoal):
 1. x \<in> sumset (A \<union> B) (stabilizer C)
[PROOF STEP]
using assms sumset.cases
[PROOF STATE]
proof (prove)
using this:
x = a \<oplus> c
c \<in> stabilizer C
c \<in> G
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer 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. x \<in> sumset (A \<union> B) (stabilizer C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> sumset (A \<union> B) (stabilizer C)

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

goal (1 subgoal):
 1. \<And>x. x \<in> sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))
[PROOF STEP]
have "x \<notin> sumset (A \<union> B) ?H1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> sumset (A \<union> B) (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. x \<in> sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> False
[PROOF STEP]
assume "x \<in> sumset (A \<union> B) ?H1"
[PROOF STATE]
proof (state)
this:
x \<in> sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))

goal (1 subgoal):
 1. x \<in> sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))
[PROOF STEP]
obtain y h1 where hy: "y \<in> A \<union> B" and hyG: "y \<in> G" and hh1G: "h1 \<in> G"
          and hh1: "h1 \<in> ?H1" and hxy: "x = y \<oplus> h1"
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))

goal (1 subgoal):
 1. (\<And>y h1. \<lbrakk>y \<in> A \<union> B; y \<in> G; h1 \<in> G; h1 \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))); x = y \<oplus> h1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson sumset.cases)
[PROOF STATE]
proof (state)
this:
y \<in> A \<union> B
y \<in> G
h1 \<in> G
h1 \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
x = y \<oplus> h1

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

goal (1 subgoal):
 1. y = a \<oplus> c \<ominus> h1
[PROOF STEP]
using hxac hxy assms associative commutative composition_closed
          inverse_closed invertible invertible_left_inverse2
[PROOF STATE]
proof (prove)
using this:
y \<in> A \<union> B
y \<in> G
h1 \<in> G
h1 \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
x = y \<oplus> h1
x = a \<oplus> c
x = y \<oplus> h1
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)
\<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
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> G
?x \<in> G \<Longrightarrow> local.inverse ?x \<in> G
?u \<in> G \<Longrightarrow> invertible ?u
\<lbrakk>invertible ?u; ?u \<in> G; ?v \<in> G\<rbrakk> \<Longrightarrow> local.inverse ?u \<oplus> (?u \<oplus> ?v) = ?v

goal (1 subgoal):
 1. y = a \<oplus> c \<ominus> h1
[PROOF STEP]
by (metis hcG)
[PROOF STATE]
proof (state)
this:
y = a \<oplus> c \<ominus> h1

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

goal (1 subgoal):
 1. x \<in> sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> False
[PROOF STEP]
have "h1 \<in> stabilizer C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h1 \<in> stabilizer C
[PROOF STEP]
using hh1 assms
[PROOF STATE]
proof (prove)
using this:
h1 \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)

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

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

goal (1 subgoal):
 1. x \<in> sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> False
[PROOF STEP]
hence "c \<oplus> inverse h1 \<in> stabilizer C"
[PROOF STATE]
proof (prove)
using this:
h1 \<in> stabilizer C

goal (1 subgoal):
 1. c \<ominus> h1 \<in> stabilizer C
[PROOF STEP]
using hc stabilizer_is_subgroup subgroup_def
          group_axioms invertible subgroup.subgroup_inverse_iff submonoid.sub_composition_closed hh1G
[PROOF STATE]
proof (prove)
using this:
h1 \<in> stabilizer C
c \<in> stabilizer C
subgroup (stabilizer ?S) G (\<oplus>) \<zero>
subgroup ?G ?M ?composition ?unit \<equiv> submonoid ?G ?M ?composition ?unit \<and> Group_Theory.group ?G ?composition ?unit
Group_Theory.group G (\<oplus>) \<zero>
?u \<in> G \<Longrightarrow> invertible ?u
\<lbrakk>subgroup ?G ?M ?composition ?unit; monoid.invertible ?M ?composition ?unit ?x; ?x \<in> ?M\<rbrakk> \<Longrightarrow> (monoid.inverse ?M ?composition ?unit ?x \<in> ?G) = (?x \<in> ?G)
\<lbrakk>submonoid ?N ?M ?composition ?unit; ?a \<in> ?N; ?b \<in> ?N\<rbrakk> \<Longrightarrow> ?composition ?a ?b \<in> ?N
h1 \<in> G

goal (1 subgoal):
 1. c \<ominus> h1 \<in> stabilizer C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
c \<ominus> h1 \<in> stabilizer C

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

goal (1 subgoal):
 1. y \<in> sumset {a} (stabilizer C)
[PROOF STEP]
using assms hcG hh1G
[PROOF STATE]
proof (prove)
using this:
y = a \<oplus> c \<ominus> h1
h1 \<in> stabilizer C
c \<ominus> h1 \<in> stabilizer C
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)
c \<in> G
h1 \<in> G

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

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

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

goal (1 subgoal):
 1. y \<in> A
[PROOF STEP]
using assms(1) hy
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {a} (stabilizer C)
B \<inter> sumset {a} (stabilizer C) = {}
y \<in> A \<union> B

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

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

goal (1 subgoal):
 1. x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))
[PROOF STEP]
using hxy hh1
[PROOF STATE]
proof (prove)
using this:
y \<in> sumset {a} (stabilizer C)
y \<in> A
x = y \<oplus> h1
h1 \<in> stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))

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

goal (1 subgoal):
 1. x \<in> sumset (A \<union> B) (stabilizer (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:
x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))

goal (1 subgoal):
 1. False
[PROOF STEP]
using hx
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))
x \<in> sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<Longrightarrow> x \<in> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (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> sumset (A \<union> B) (stabilizer C)
x \<notin> sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))
[PROOF STEP]
show "x \<in> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) ?H1"
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset (A \<union> B) (stabilizer C)
x \<notin> sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))

goal (1 subgoal):
 1. x \<in> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (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:
sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))

goal (1 subgoal):
 1. int (card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))

goal (1 subgoal):
 1. int (card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
using card_mono finite_Diff finite_sumset assms
[PROOF STATE]
proof (prove)
using this:
sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))) \<subseteq> sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B
finite ?A \<Longrightarrow> finite (?A - ?B)
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)

goal (1 subgoal):
 1. int (card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
by (metis finite_UnI nat_int_comparison(3))
[PROOF STATE]
proof (state)
this:
int (card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (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:
int (card (sumset {a} (stabilizer C) - sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
have "... = int (card (sumset (A \<union> B) (stabilizer C))) -
    card (sumset (A \<union> B) ?H1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (card (sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) = int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
using card_Diff_subset[OF hfinsumH1 hsubsumH1] hsumH1card_le
[PROOF STATE]
proof (prove)
using this:
card (sumset (A \<union> B) (stabilizer C) - sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) = card (sumset (A \<union> B) (stabilizer C)) - card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))
card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))) \<le> card (sumset (A \<union> B) (stabilizer C))

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

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (card (sumset {a} (stabilizer C))) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
show "int (card (sumset (A \<union> B) (stabilizer C))) - card (sumset (A \<union> B) ?H1) \<ge>
    int (card (stabilizer C)) - card (sumset ?A1 ?H1)"
[PROOF STATE]
proof (prove)
using this:
int (card (sumset {a} (stabilizer C))) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))

goal (1 subgoal):
 1. int (card (stabilizer C)) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
int (card (sumset {a} (stabilizer C))) - int (card (sumset (A \<inter> sumset {a} (stabilizer C)) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C)))))) \<le> int (card (sumset (A \<union> B) (stabilizer C))) - int (card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))))))
B \<inter> sumset {a} (stabilizer C) = {}
stabilizer (sumset (A \<inter> sumset {a} (stabilizer C)) (B \<inter> sumset {b} (stabilizer C))) \<subset> stabilizer C
a \<in> A
a \<in> G
finite A
finite B
A \<noteq> {}
B \<noteq> {}
finite (stabilizer C)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exists_convergent_min_stabilizer:
  assumes hind: "\<forall>m<n. \<forall>C D. C \<subseteq> G \<longrightarrow> D \<subseteq> G \<longrightarrow> finite C \<longrightarrow> finite D \<longrightarrow> C \<noteq> {} \<longrightarrow>
    D \<noteq> {} \<longrightarrow> card (sumset C D) + card C = m \<longrightarrow>
    card (sumset C (stabilizer (sumset C D))) + card (sumset D (stabilizer (sumset C D))) -
    card ((stabilizer (sumset C D)))
    \<le> card (sumset C D)" and hAG: "A \<subseteq> G" and hBG: "B \<subseteq> G" and hA: "finite A" and
    hB: "finite B" and hAne: "A \<noteq> {}" and "A \<inter> B \<noteq> {}" and
    hcardsum: "card (sumset A B) + card A = n" and hintercardA: "card (A \<inter> B) < card A"
  obtains X where "convergent X A B" and "\<And> Y. Y \<in> convergent_set A B \<Longrightarrow>
    card (stabilizer Y) \<ge> card (stabilizer X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?C0 = "sumset (A \<inter> B) (A \<union> B)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have hC0ne: "?C0 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (A \<inter> B) (A \<union> B) \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. \<forall>C D. C \<subseteq> G \<longrightarrow> D \<subseteq> G \<longrightarrow> finite C \<longrightarrow> finite D \<longrightarrow> C \<noteq> {} \<longrightarrow> D \<noteq> {} \<longrightarrow> card (sumset C D) + card C = m \<longrightarrow> card (sumset C (stabilizer (sumset C D))) + card (sumset D (stabilizer (sumset C D))) - card (stabilizer (sumset C D)) \<le> card (sumset C D)
A \<subseteq> G
B \<subseteq> G
finite A
finite B
A \<noteq> {}
A \<inter> B \<noteq> {}
card (sumset A B) + card A = n
card (A \<inter> B) < card A

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

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sumset (A \<inter> B) (A \<union> B) \<noteq> {}

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "finite ?C0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (sumset (A \<inter> B) (A \<union> B))
[PROOF STEP]
using sumset_inter_union_subset finite_sumset assms
[PROOF STATE]
proof (prove)
using this:
sumset (?A \<inter> ?B) (?A \<union> ?B) \<subseteq> sumset ?A ?B
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
\<forall>m<n. \<forall>C D. C \<subseteq> G \<longrightarrow> D \<subseteq> G \<longrightarrow> finite C \<longrightarrow> finite D \<longrightarrow> C \<noteq> {} \<longrightarrow> D \<noteq> {} \<longrightarrow> card (sumset C D) + card C = m \<longrightarrow> card (sumset C (stabilizer (sumset C D))) + card (sumset D (stabilizer (sumset C D))) - card (stabilizer (sumset C D)) \<le> card (sumset C D)
A \<subseteq> G
B \<subseteq> G
finite A
finite B
A \<noteq> {}
A \<inter> B \<noteq> {}
card (sumset A B) + card A = n
card (A \<inter> B) < card A

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

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sumset (A \<inter> B) (A \<union> B) \<noteq> {}
finite (sumset (A \<inter> B) (A \<union> B))
[PROOF STEP]
have "finite (stabilizer ?C0)"
[PROOF STATE]
proof (prove)
using this:
sumset (A \<inter> B) (A \<union> B) \<noteq> {}
finite (sumset (A \<inter> B) (A \<union> B))

goal (1 subgoal):
 1. finite (stabilizer (sumset (A \<inter> B) (A \<union> B)))
[PROOF STEP]
using stabilizer_finite
[PROOF STATE]
proof (prove)
using this:
sumset (A \<inter> B) (A \<union> B) \<noteq> {}
finite (sumset (A \<inter> B) (A \<union> B))
\<lbrakk>?S \<subseteq> G; ?S \<noteq> {}; finite ?S\<rbrakk> \<Longrightarrow> finite (stabilizer ?S)

goal (1 subgoal):
 1. finite (stabilizer (sumset (A \<inter> B) (A \<union> B)))
[PROOF STEP]
using sumset_subset_carrier
[PROOF STATE]
proof (prove)
using this:
sumset (A \<inter> B) (A \<union> B) \<noteq> {}
finite (sumset (A \<inter> B) (A \<union> B))
\<lbrakk>?S \<subseteq> G; ?S \<noteq> {}; finite ?S\<rbrakk> \<Longrightarrow> finite (stabilizer ?S)
sumset ?A ?B \<subseteq> G

goal (1 subgoal):
 1. finite (stabilizer (sumset (A \<inter> B) (A \<union> B)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
finite (stabilizer (sumset (A \<inter> B) (A \<union> B)))

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (stabilizer (sumset (A \<inter> B) (A \<union> B)))
[PROOF STEP]
have hcard_sumset_le: "card (A \<inter> B) \<le> card (sumset (A \<inter> B) (stabilizer ?C0))"
[PROOF STATE]
proof (prove)
using this:
finite (stabilizer (sumset (A \<inter> B) (A \<union> B)))

goal (1 subgoal):
 1. card (A \<inter> B) \<le> card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B))))
[PROOF STEP]
using card_le_sumset sumset_commute sub_unit_closed assms
[PROOF STATE]
proof (prove)
using this:
finite (stabilizer (sumset (A \<inter> B) (A \<union> B)))
\<lbrakk>finite ?A; ?a \<in> ?A; ?a \<in> G; finite ?B; ?B \<subseteq> G\<rbrakk> \<Longrightarrow> card ?B \<le> card (sumset ?A ?B)
sumset ?A ?B = sumset ?B ?A
\<zero> \<in> stabilizer ?A
\<forall>m<n. \<forall>C D. C \<subseteq> G \<longrightarrow> D \<subseteq> G \<longrightarrow> finite C \<longrightarrow> finite D \<longrightarrow> C \<noteq> {} \<longrightarrow> D \<noteq> {} \<longrightarrow> card (sumset C D) + card C = m \<longrightarrow> card (sumset C (stabilizer (sumset C D))) + card (sumset D (stabilizer (sumset C D))) - card (stabilizer (sumset C D)) \<le> card (sumset C D)
A \<subseteq> G
B \<subseteq> G
finite A
finite B
A \<noteq> {}
A \<inter> B \<noteq> {}
card (sumset A B) + card A = n
card (A \<inter> B) < card A

goal (1 subgoal):
 1. card (A \<inter> B) \<le> card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B))))
[PROOF STEP]
by (metis Int_Un_eq(3) Un_subset_iff finite_Int unit_closed)
[PROOF STATE]
proof (state)
this:
card (A \<inter> B) \<le> card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B))))

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "card ?C0 \<le> card (sumset A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (sumset (A \<inter> B) (A \<union> B)) \<le> card (sumset A B)
[PROOF STEP]
using card_mono sumset_inter_union_subset finite_sumset assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B
sumset (?A \<inter> ?B) (?A \<union> ?B) \<subseteq> sumset ?A ?B
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)
\<forall>m<n. \<forall>C D. C \<subseteq> G \<longrightarrow> D \<subseteq> G \<longrightarrow> finite C \<longrightarrow> finite D \<longrightarrow> C \<noteq> {} \<longrightarrow> D \<noteq> {} \<longrightarrow> card (sumset C D) + card C = m \<longrightarrow> card (sumset C (stabilizer (sumset C D))) + card (sumset D (stabilizer (sumset C D))) - card (stabilizer (sumset C D)) \<le> card (sumset C D)
A \<subseteq> G
B \<subseteq> G
finite A
finite B
A \<noteq> {}
A \<inter> B \<noteq> {}
card (sumset A B) + card A = n
card (A \<inter> B) < card A

goal (1 subgoal):
 1. card (sumset (A \<inter> B) (A \<union> B)) \<le> card (sumset A B)
[PROOF STEP]
by (simp add: card_mono finite_sumset hA hB sumset_inter_union_subset)
[PROOF STATE]
proof (state)
this:
card (sumset (A \<inter> B) (A \<union> B)) \<le> card (sumset A B)

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (sumset (A \<inter> B) (A \<union> B)) \<le> card (sumset A B)
[PROOF STEP]
have "card ?C0 + card (A \<inter> B) < card (sumset A B) + card A"
[PROOF STATE]
proof (prove)
using this:
card (sumset (A \<inter> B) (A \<union> B)) \<le> card (sumset A B)

goal (1 subgoal):
 1. card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) < card (sumset A B) + card A
[PROOF STEP]
using hintercardA
[PROOF STATE]
proof (prove)
using this:
card (sumset (A \<inter> B) (A \<union> B)) \<le> card (sumset A B)
card (A \<inter> B) < card A

goal (1 subgoal):
 1. card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) < card (sumset A B) + card A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) < card (sumset A B) + card A

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) < card (sumset A B) + card A
[PROOF STEP]
obtain m where "m < n" and "card ?C0 + card (A \<inter> B) = m"
[PROOF STATE]
proof (prove)
using this:
card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) < card (sumset A B) + card A

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m < n; card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) = m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using hcardsum
[PROOF STATE]
proof (prove)
using this:
card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) < card (sumset A B) + card A
card (sumset A B) + card A = n

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m < n; card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) = m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m < n
card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) = m

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m < n
card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) = m
[PROOF STEP]
have "card (sumset (A \<inter> B) (stabilizer ?C0)) +
    card (sumset (A \<union> B) (stabilizer ?C0)) - card (stabilizer ?C0) \<le> card ?C0"
[PROOF STATE]
proof (prove)
using this:
m < n
card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) = m

goal (1 subgoal):
 1. card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) - card (stabilizer (sumset (A \<inter> B) (A \<union> B))) \<le> card (sumset (A \<inter> B) (A \<union> B))
[PROOF STEP]
using assms finite_Un finite_Int
[PROOF STATE]
proof (prove)
using this:
m < n
card (sumset (A \<inter> B) (A \<union> B)) + card (A \<inter> B) = m
\<forall>m<n. \<forall>C D. C \<subseteq> G \<longrightarrow> D \<subseteq> G \<longrightarrow> finite C \<longrightarrow> finite D \<longrightarrow> C \<noteq> {} \<longrightarrow> D \<noteq> {} \<longrightarrow> card (sumset C D) + card C = m \<longrightarrow> card (sumset C (stabilizer (sumset C D))) + card (sumset D (stabilizer (sumset C D))) - card (stabilizer (sumset C D)) \<le> card (sumset C D)
A \<subseteq> G
B \<subseteq> G
finite A
finite B
A \<noteq> {}
A \<inter> B \<noteq> {}
card (sumset A B) + card A = n
card (A \<inter> B) < card A
finite (?F \<union> ?G) = (finite ?F \<and> finite ?G)
finite ?F \<or> finite ?G \<Longrightarrow> finite (?F \<inter> ?G)

goal (1 subgoal):
 1. card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) - card (stabilizer (sumset (A \<inter> B) (A \<union> B))) \<le> card (sumset (A \<inter> B) (A \<union> B))
[PROOF STEP]
by (metis Int_Un_eq(4) Un_empty Un_subset_iff)
[PROOF STATE]
proof (state)
this:
card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) - card (stabilizer (sumset (A \<inter> B) (A \<union> B))) \<le> card (sumset (A \<inter> B) (A \<union> B))

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) - card (stabilizer (sumset (A \<inter> B) (A \<union> B))) \<le> card (sumset (A \<inter> B) (A \<union> B))
[PROOF STEP]
have "card ?C0 + card (stabilizer ?C0) \<ge>
    card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer ?C0))"
[PROOF STATE]
proof (prove)
using this:
card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) - card (stabilizer (sumset (A \<inter> B) (A \<union> B))) \<le> card (sumset (A \<inter> B) (A \<union> B))

goal (1 subgoal):
 1. card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) \<le> card (sumset (A \<inter> B) (A \<union> B)) + card (stabilizer (sumset (A \<inter> B) (A \<union> B)))
[PROOF STEP]
using hcard_sumset_le
[PROOF STATE]
proof (prove)
using this:
card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) - card (stabilizer (sumset (A \<inter> B) (A \<union> B))) \<le> card (sumset (A \<inter> B) (A \<union> B))
card (A \<inter> B) \<le> card (sumset (A \<inter> B) (stabilizer (sumset (A \<inter> B) (A \<union> B))))

goal (1 subgoal):
 1. card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) \<le> card (sumset (A \<inter> B) (A \<union> B)) + card (stabilizer (sumset (A \<inter> B) (A \<union> B)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) \<le> card (sumset (A \<inter> B) (A \<union> B)) + card (stabilizer (sumset (A \<inter> B) (A \<union> B)))

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) \<le> card (sumset (A \<inter> B) (A \<union> B)) + card (stabilizer (sumset (A \<inter> B) (A \<union> B)))
[PROOF STEP]
have "?C0 \<in> convergent_set A B"
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) \<le> card (sumset (A \<inter> B) (A \<union> B)) + card (stabilizer (sumset (A \<inter> B) (A \<union> B)))

goal (1 subgoal):
 1. sumset (A \<inter> B) (A \<union> B) \<in> convergent_set A B
[PROOF STEP]
using convergent_set_def convergent_def
   sumset_inter_union_subset hC0ne
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer (sumset (A \<inter> B) (A \<union> B)))) \<le> card (sumset (A \<inter> B) (A \<union> B)) + card (stabilizer (sumset (A \<inter> B) (A \<union> B)))
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)
sumset (?A \<inter> ?B) (?A \<union> ?B) \<subseteq> sumset ?A ?B
sumset (A \<inter> B) (A \<union> B) \<noteq> {}

goal (1 subgoal):
 1. sumset (A \<inter> B) (A \<union> B) \<in> convergent_set A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sumset (A \<inter> B) (A \<union> B) \<in> convergent_set A B

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sumset (A \<inter> B) (A \<union> B) \<in> convergent_set A B
[PROOF STEP]
have hconvergent_ne: "convergent_set A B \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
sumset (A \<inter> B) (A \<union> B) \<in> convergent_set A B

goal (1 subgoal):
 1. convergent_set A B \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
convergent_set A B \<noteq> {}

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define KS where "KS \<equiv> (\<lambda> X. card (stabilizer X)) ` convergent_set A B"
[PROOF STATE]
proof (state)
this:
KS \<equiv> (\<lambda>X. card (stabilizer X)) ` convergent_set A B

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define K where "K \<equiv> Min KS"
[PROOF STATE]
proof (state)
this:
K \<equiv> Min KS

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define C where "C \<equiv> @C. C \<in> convergent_set A B \<and> K = card (stabilizer C)"
[PROOF STATE]
proof (state)
this:
C \<equiv> SOME C. C \<in> convergent_set A B \<and> K = card (stabilizer C)

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain KS: "finite KS" "KS \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>finite KS; KS \<noteq> {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using hconvergent_ne finite_convergent_set assms KS_def
[PROOF STATE]
proof (prove)
using this:
convergent_set A B \<noteq> {}
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (convergent_set ?A ?B)
\<forall>m<n. \<forall>C D. C \<subseteq> G \<longrightarrow> D \<subseteq> G \<longrightarrow> finite C \<longrightarrow> finite D \<longrightarrow> C \<noteq> {} \<longrightarrow> D \<noteq> {} \<longrightarrow> card (sumset C D) + card C = m \<longrightarrow> card (sumset C (stabilizer (sumset C D))) + card (sumset D (stabilizer (sumset C D))) - card (stabilizer (sumset C D)) \<le> card (sumset C D)
A \<subseteq> G
B \<subseteq> G
finite A
finite B
A \<noteq> {}
A \<inter> B \<noteq> {}
card (sumset A B) + card A = n
card (A \<inter> B) < card A
KS \<equiv> (\<lambda>X. card (stabilizer X)) ` convergent_set A B

goal (1 subgoal):
 1. (\<lbrakk>finite KS; KS \<noteq> {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite KS
KS \<noteq> {}

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite KS
KS \<noteq> {}
[PROOF STEP]
have "K \<in> KS"
[PROOF STATE]
proof (prove)
using this:
finite KS
KS \<noteq> {}

goal (1 subgoal):
 1. K \<in> KS
[PROOF STEP]
using K_def Min_in
[PROOF STATE]
proof (prove)
using this:
finite KS
KS \<noteq> {}
K \<equiv> Min KS
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Min ?A \<in> ?A

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

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
K \<in> KS
[PROOF STEP]
have "\<exists> X. X \<in> convergent_set A B \<and> K = card (stabilizer X)"
[PROOF STATE]
proof (prove)
using this:
K \<in> KS

goal (1 subgoal):
 1. \<exists>X. X \<in> convergent_set A B \<and> K = card (stabilizer X)
[PROOF STEP]
using KS_def
[PROOF STATE]
proof (prove)
using this:
K \<in> KS
KS \<equiv> (\<lambda>X. card (stabilizer X)) ` convergent_set A B

goal (1 subgoal):
 1. \<exists>X. X \<in> convergent_set A B \<and> K = card (stabilizer X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>X. X \<in> convergent_set A B \<and> K = card (stabilizer X)

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>X. X \<in> convergent_set A B \<and> K = card (stabilizer X)
[PROOF STEP]
obtain "C \<in> convergent_set A B" and Keq: "K = card (stabilizer C)"
[PROOF STATE]
proof (prove)
using this:
\<exists>X. X \<in> convergent_set A B \<and> K = card (stabilizer X)

goal (1 subgoal):
 1. (\<lbrakk>C \<in> convergent_set A B; K = card (stabilizer C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (mono_tags, lifting) C_def someI_ex)
[PROOF STATE]
proof (state)
this:
C \<in> convergent_set A B
K = card (stabilizer C)

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> convergent_set A B
K = card (stabilizer C)
[PROOF STEP]
have hC: "C \<subseteq> sumset A B" and hCne: "C \<noteq> {}" and
    hCcard: "card C + card (stabilizer C) \<ge>
    card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer C))"
[PROOF STATE]
proof (prove)
using this:
C \<in> convergent_set A B
K = card (stabilizer C)

goal (1 subgoal):
 1. C \<subseteq> sumset A B &&& C \<noteq> {} &&& card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer C)) \<le> card C + card (stabilizer C)
[PROOF STEP]
using convergent_set_def convergent_def
[PROOF STATE]
proof (prove)
using this:
C \<in> convergent_set A B
K = card (stabilizer C)
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. C \<subseteq> sumset A B &&& C \<noteq> {} &&& card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer C)) \<le> card C + card (stabilizer C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<subseteq> sumset A B
C \<noteq> {}
card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer C)) \<le> card C + card (stabilizer C)

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have hCmin: "\<And> Y. Y \<in> convergent_set A B \<Longrightarrow>
    card (stabilizer Y) \<ge> card (stabilizer C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer C) \<le> card (stabilizer Y)
[PROOF STEP]
using K_def KS_def Keq Min_le KS(1)
[PROOF STATE]
proof (prove)
using this:
K \<equiv> Min KS
KS \<equiv> (\<lambda>X. card (stabilizer X)) ` convergent_set A B
K = card (stabilizer C)
\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> Min ?A \<le> ?x
finite KS

goal (1 subgoal):
 1. \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer C) \<le> card (stabilizer Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer C) \<le> card (stabilizer ?Y)

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>local.convergent X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using hCmin hC hCcard hCne local.convergent_def that
[PROOF STATE]
proof (prove)
using this:
?Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer C) \<le> card (stabilizer ?Y)
C \<subseteq> sumset A B
card (A \<inter> B) + card (sumset (A \<union> B) (stabilizer C)) \<le> card C + card (stabilizer C)
C \<noteq> {}
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)
\<lbrakk>local.convergent ?X A B; \<And>Y. Y \<in> convergent_set A B \<Longrightarrow> card (stabilizer ?X) \<le> card (stabilizer Y)\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_eq_coset:
  assumes "\<phi> x = a" and "a \<in> G" and "x \<in> G // K"
  shows "x = a \<cdot>| K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = a \<cdot>| K
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = a \<cdot>| K
[PROOF STEP]
have "(SOME a. a \<in> G \<and> x = a \<cdot>| K) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME a. a \<in> G \<and> x = a \<cdot>| K) = a
[PROOF STEP]
using \<phi>_def assms
[PROOF STATE]
proof (prove)
using this:
\<phi> = (\<lambda>x. if x \<in> Partition then SOME a. a \<in> G \<and> x = a \<cdot>| K else undefined)
\<phi> x = a
a \<in> G
x \<in> Partition

goal (1 subgoal):
 1. (SOME a. a \<in> G \<and> x = a \<cdot>| K) = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(SOME a. a \<in> G \<and> x = a \<cdot>| K) = a

goal (1 subgoal):
 1. x = a \<cdot>| K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(SOME a. a \<in> G \<and> x = a \<cdot>| K) = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(SOME a. a \<in> G \<and> x = a \<cdot>| K) = a

goal (1 subgoal):
 1. x = a \<cdot>| K
[PROOF STEP]
using some_eq_ex representant_exists Left_Coset_Class_unit assms
[PROOF STATE]
proof (prove)
using this:
(SOME a. a \<in> G \<and> x = a \<cdot>| K) = a
?P (SOME x. ?P x) = (\<exists>x. ?P x)
?A \<in> Partition \<Longrightarrow> \<exists>a\<in>G. a \<in> ?A \<and> ?A = Class a
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g
\<phi> x = a
a \<in> G
x \<in> Partition

goal (1 subgoal):
 1. x = a \<cdot>| K
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
x = a \<cdot>| K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_coset_mem:
  assumes "a \<in> G"
  shows "\<phi> (a \<cdot>| K) \<in> a \<cdot>| K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (a \<cdot>| K) \<in> a \<cdot>| K
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (a \<cdot>| K) \<in> a \<cdot>| K
[PROOF STEP]
obtain x where hx: "x = \<phi> (a \<cdot>| K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x = \<phi> (a \<cdot>| K) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = \<phi> (a \<cdot>| K)

goal (1 subgoal):
 1. \<phi> (a \<cdot>| K) \<in> a \<cdot>| K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = \<phi> (a \<cdot>| K)
[PROOF STEP]
have "x = (SOME x. x \<in> G \<and> a \<cdot>| K = x \<cdot>| K)"
[PROOF STATE]
proof (prove)
using this:
x = \<phi> (a \<cdot>| K)

goal (1 subgoal):
 1. x = (SOME x. x \<in> G \<and> a \<cdot>| K = x \<cdot>| K)
[PROOF STEP]
using \<phi>_def assms
    Class_in_Partition Left_Coset_Class_unit
[PROOF STATE]
proof (prove)
using this:
x = \<phi> (a \<cdot>| K)
\<phi> = (\<lambda>x. if x \<in> Partition then SOME a. a \<in> G \<and> x = a \<cdot>| K else undefined)
a \<in> G
?a \<in> G \<Longrightarrow> Class ?a \<in> Partition
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g

goal (1 subgoal):
 1. x = (SOME x. x \<in> G \<and> a \<cdot>| K = x \<cdot>| K)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> G \<and> a \<cdot>| K = x \<cdot>| K)

goal (1 subgoal):
 1. \<phi> (a \<cdot>| K) \<in> a \<cdot>| K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (SOME x. x \<in> G \<and> a \<cdot>| K = x \<cdot>| K)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = (SOME x. x \<in> G \<and> a \<cdot>| K = x \<cdot>| K)

goal (1 subgoal):
 1. \<phi> (a \<cdot>| K) \<in> a \<cdot>| K
[PROOF STEP]
using \<phi>_def Class_self Left_Coset_Class_unit hx assms
[PROOF STATE]
proof (prove)
using this:
x = (SOME x. x \<in> G \<and> a \<cdot>| K = x \<cdot>| K)
\<phi> = (\<lambda>x. if x \<in> Partition then SOME a. a \<in> G \<and> x = a \<cdot>| K else undefined)
?a \<in> G \<Longrightarrow> ?a \<in> Class ?a
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g
x = \<phi> (a \<cdot>| K)
a \<in> G

goal (1 subgoal):
 1. \<phi> (a \<cdot>| K) \<in> a \<cdot>| K
[PROOF STEP]
by (smt (verit, ccfv_SIG) tfl_some)
[PROOF STATE]
proof (state)
this:
\<phi> (a \<cdot>| K) \<in> a \<cdot>| K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_coset_eq:
  assumes "a \<in> G" and "\<phi> x = a" and "x \<in> G // K"
  shows "\<phi> (a \<cdot>| K) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (a \<cdot>| K) = a
[PROOF STEP]
using phi_eq_coset assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<phi> ?x = ?a; ?a \<in> G; ?x \<in> Partition\<rbrakk> \<Longrightarrow> ?x = ?a \<cdot>| K
a \<in> G
\<phi> x = a
x \<in> Partition

goal (1 subgoal):
 1. \<phi> (a \<cdot>| K) = a
[PROOF STEP]
by metis


[STATEMENT]
lemma phi_inverse_right:
  assumes "g \<in> G"
  shows "quot_comp_alt g (\<phi> (inverse g \<cdot>| K)) = \<phi> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
[PROOF STEP]
have "g \<cdot> (\<phi> (inverse g \<cdot>| K)) \<in> (g \<cdot> (inverse g) \<cdot>| K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<in> g \<cdot> local.inverse g \<cdot>| K
[PROOF STEP]
using phi_coset_mem assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> G \<Longrightarrow> \<phi> (?a \<cdot>| K) \<in> ?a \<cdot>| K
g \<in> G

goal (1 subgoal):
 1. g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<in> g \<cdot> local.inverse g \<cdot>| K
[PROOF STEP]
by (smt (z3) Left_Coset_memE factor_unit invertible invertible_right_inverse
    invertible_inverse_closed invertible_inverse_inverse sub invertible_left_inverse2)
[PROOF STATE]
proof (state)
this:
g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<in> g \<cdot> local.inverse g \<cdot>| K

goal (1 subgoal):
 1. quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<in> g \<cdot> local.inverse g \<cdot>| K
[PROOF STEP]
have "g \<cdot> (\<phi> (inverse g \<cdot>| K)) \<cdot>| K = K"
[PROOF STATE]
proof (prove)
using this:
g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<in> g \<cdot> local.inverse g \<cdot>| K

goal (1 subgoal):
 1. g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<cdot>| K = K
[PROOF STEP]
using Block_self Left_Coset_Class_unit Normal_def quotient.unit_closed sub
[PROOF STATE]
proof (prove)
using this:
g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<in> g \<cdot> local.inverse g \<cdot>| K
\<lbrakk>?a \<in> ?A; ?A \<in> Partition\<rbrakk> \<Longrightarrow> Class ?a = ?A
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g
K = Class \<one>
Class \<one> \<in> Partition
?a \<in> K \<Longrightarrow> ?a \<in> G

goal (1 subgoal):
 1. g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<cdot>| K = K
[PROOF STEP]
by (metis assms composition_closed invertible invertible_inverse_closed invertible_right_inverse)
[PROOF STATE]
proof (state)
this:
g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<cdot>| K = K

goal (1 subgoal):
 1. quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<cdot>| K = K
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<cdot>| K = K

goal (1 subgoal):
 1. quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
[PROOF STEP]
using quot_comp_alt_def
[PROOF STATE]
proof (prove)
using this:
g \<cdot> \<phi> (local.inverse g \<cdot>| K) \<cdot>| K = K
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)

goal (1 subgoal):
 1. quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_inverse_left:
  assumes "g \<in> G"
  shows "quot_comp_alt (\<phi> (inverse g \<cdot>| K)) g = \<phi> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
[PROOF STEP]
have "(\<phi> (inverse g \<cdot>| K)) \<cdot> g \<in> ((inverse g) \<cdot> g) \<cdot>| K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (local.inverse g \<cdot>| K) \<cdot> g \<in> local.inverse g \<cdot> g \<cdot>| K
[PROOF STEP]
using phi_coset_mem assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> G \<Longrightarrow> \<phi> (?a \<cdot>| K) \<in> ?a \<cdot>| K
g \<in> G

goal (1 subgoal):
 1. \<phi> (local.inverse g \<cdot>| K) \<cdot> g \<in> local.inverse g \<cdot> g \<cdot>| K
[PROOF STEP]
by (metis Left_Coset_memE factor_unit invertible invertible_inverse_closed invertible_left_inverse normal)
[PROOF STATE]
proof (state)
this:
\<phi> (local.inverse g \<cdot>| K) \<cdot> g \<in> local.inverse g \<cdot> g \<cdot>| K

goal (1 subgoal):
 1. quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (local.inverse g \<cdot>| K) \<cdot> g \<in> local.inverse g \<cdot> g \<cdot>| K
[PROOF STEP]
have "(\<phi> (inverse g \<cdot>| K)) \<cdot> g \<cdot>| K = K"
[PROOF STATE]
proof (prove)
using this:
\<phi> (local.inverse g \<cdot>| K) \<cdot> g \<in> local.inverse g \<cdot> g \<cdot>| K

goal (1 subgoal):
 1. \<phi> (local.inverse g \<cdot>| K) \<cdot> g \<cdot>| K = K
[PROOF STEP]
using Block_self Left_Coset_Class_unit Normal_def
    quotient.unit_closed sub
[PROOF STATE]
proof (prove)
using this:
\<phi> (local.inverse g \<cdot>| K) \<cdot> g \<in> local.inverse g \<cdot> g \<cdot>| K
\<lbrakk>?a \<in> ?A; ?A \<in> Partition\<rbrakk> \<Longrightarrow> Class ?a = ?A
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g
K = Class \<one>
Class \<one> \<in> Partition
?a \<in> K \<Longrightarrow> ?a \<in> G

goal (1 subgoal):
 1. \<phi> (local.inverse g \<cdot>| K) \<cdot> g \<cdot>| K = K
[PROOF STEP]
by (smt (verit, best) assms composition_closed invertible invertible_inverse_closed
    invertible_left_inverse)
[PROOF STATE]
proof (state)
this:
\<phi> (local.inverse g \<cdot>| K) \<cdot> g \<cdot>| K = K

goal (1 subgoal):
 1. quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (local.inverse g \<cdot>| K) \<cdot> g \<cdot>| K = K
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (local.inverse g \<cdot>| K) \<cdot> g \<cdot>| K = K

goal (1 subgoal):
 1. quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
[PROOF STEP]
using quot_comp_alt_def
[PROOF STATE]
proof (prove)
using this:
\<phi> (local.inverse g \<cdot>| K) \<cdot> g \<cdot>| K = K
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)

goal (1 subgoal):
 1. quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_mem_coset_eq:
  assumes "a \<in> G // K" and "b \<in> G"
  shows "\<phi> a \<in> b \<cdot>| K  \<Longrightarrow> a = (b \<cdot>| K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> a \<in> b \<cdot>| K \<Longrightarrow> a = b \<cdot>| K
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> a \<in> b \<cdot>| K \<Longrightarrow> a = b \<cdot>| K
[PROOF STEP]
assume "\<phi> a \<in> b \<cdot>| K"
[PROOF STATE]
proof (state)
this:
\<phi> a \<in> b \<cdot>| K

goal (1 subgoal):
 1. \<phi> a \<in> b \<cdot>| K \<Longrightarrow> a = b \<cdot>| K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> a \<in> b \<cdot>| K
[PROOF STEP]
have "a \<inter> (b \<cdot>| K) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<phi> a \<in> b \<cdot>| K

goal (1 subgoal):
 1. a \<inter> (b \<cdot>| K) \<noteq> {}
[PROOF STEP]
by (metis Class_closed Class_is_Left_Coset Int_iff assms empty_iff phi_coset_mem phi_eq_coset)
[PROOF STATE]
proof (state)
this:
a \<inter> (b \<cdot>| K) \<noteq> {}

goal (1 subgoal):
 1. \<phi> a \<in> b \<cdot>| K \<Longrightarrow> a = b \<cdot>| K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<inter> (b \<cdot>| K) \<noteq> {}
[PROOF STEP]
show "a = b \<cdot>| K"
[PROOF STATE]
proof (prove)
using this:
a \<inter> (b \<cdot>| K) \<noteq> {}

goal (1 subgoal):
 1. a = b \<cdot>| K
[PROOF STEP]
by (metis Class_in_Partition Class_is_Left_Coset assms disjoint)
[PROOF STATE]
proof (state)
this:
a = b \<cdot>| K

goal:
No subgoals!
[PROOF STEP]
qed