[STATEMENT]
lemma Erdos_Rado_sunflower_same_card:
  assumes "\<forall> A \<in> F. finite A \<and> card A = k"
    and "card F > (r - 1)^k * fact k"
  shows "\<exists> S. S \<subseteq> F \<and> sunflower S \<and> card S = r \<and> {} \<notin> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. finite A \<and> card A = k
(r - 1) ^ k * fact k < card F

goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
proof (induct k arbitrary: F)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = 0; (r - 1) ^ 0 * fact 0 < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
 2. \<And>k F. \<lbrakk>\<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = k; (r - 1) ^ k * fact k < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S; \<forall>A\<in>F. finite A \<and> card A = Suc k; (r - 1) ^ Suc k * fact (Suc k) < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>F. finite A \<and> card A = 0
(r - 1) ^ 0 * fact 0 < card F

goal (2 subgoals):
 1. \<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = 0; (r - 1) ^ 0 * fact 0 < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
 2. \<And>k F. \<lbrakk>\<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = k; (r - 1) ^ k * fact k < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S; \<forall>A\<in>F. finite A \<and> card A = Suc k; (r - 1) ^ Suc k * fact (Suc k) < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
hence "F = {{}} \<or> F = {}" "card F \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. finite A \<and> card A = 0
(r - 1) ^ 0 * fact 0 < card F

goal (1 subgoal):
 1. F = {{}} \<or> F = {} &&& 2 \<le> card F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F = {{}} \<or> F = {}
2 \<le> card F

goal (2 subgoals):
 1. \<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = 0; (r - 1) ^ 0 * fact 0 < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
 2. \<And>k F. \<lbrakk>\<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = k; (r - 1) ^ k * fact k < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S; \<forall>A\<in>F. finite A \<and> card A = Suc k; (r - 1) ^ Suc k * fact (Suc k) < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
F = {{}} \<or> F = {}
2 \<le> card F

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

goal (2 subgoals):
 1. \<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = 0; (r - 1) ^ 0 * fact 0 < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
 2. \<And>k F. \<lbrakk>\<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = k; (r - 1) ^ k * fact k < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S; \<forall>A\<in>F. finite A \<and> card A = Suc k; (r - 1) ^ Suc k * fact (Suc k) < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S

goal (1 subgoal):
 1. \<And>k F. \<lbrakk>\<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = k; (r - 1) ^ k * fact k < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S; \<forall>A\<in>F. finite A \<and> card A = Suc k; (r - 1) ^ Suc k * fact (Suc k) < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k F. \<lbrakk>\<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = k; (r - 1) ^ k * fact k < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S; \<forall>A\<in>F. finite A \<and> card A = Suc k; (r - 1) ^ Suc k * fact (Suc k) < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
case (Suc k F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>A\<in>?F. finite A \<and> card A = k; (r - 1) ^ k * fact k < card ?F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>?F. sunflower S \<and> card S = r \<and> {} \<notin> S
\<forall>A\<in>F. finite A \<and> card A = Suc k
(r - 1) ^ Suc k * fact (Suc k) < card F

goal (1 subgoal):
 1. \<And>k F. \<lbrakk>\<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = k; (r - 1) ^ k * fact k < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S; \<forall>A\<in>F. finite A \<and> card A = Suc k; (r - 1) ^ Suc k * fact (Suc k) < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
define pd_sub :: "'a set set \<Rightarrow> nat \<Rightarrow> bool" where
    "pd_sub = (\<lambda> G t. G \<subseteq> F \<and> card G = t \<and> pairwise disjnt G \<and> {} \<notin> G)"
[PROOF STATE]
proof (state)
this:
pd_sub = (\<lambda>G t. G \<subseteq> F \<and> card G = t \<and> pairwise disjnt G \<and> {} \<notin> G)

goal (1 subgoal):
 1. \<And>k F. \<lbrakk>\<And>F. \<lbrakk>\<forall>A\<in>F. finite A \<and> card A = k; (r - 1) ^ k * fact k < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S; \<forall>A\<in>F. finite A \<and> card A = Suc k; (r - 1) ^ Suc k * fact (Suc k) < card F\<rbrakk> \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
proof (cases "\<exists> t G. pd_sub G t \<and> t \<ge> r")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
 2. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>t G. pd_sub G t \<and> r \<le> t

goal (2 subgoals):
 1. \<exists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
 2. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t G. pd_sub G t \<and> r \<le> t
[PROOF STEP]
obtain t G where pd_sub: "pd_sub G t" and t: "t \<ge> r"
[PROOF STATE]
proof (prove)
using this:
\<exists>t G. pd_sub G t \<and> r \<le> t

goal (1 subgoal):
 1. (\<And>G t. \<lbrakk>pd_sub G t; r \<le> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pd_sub G t
r \<le> t

goal (2 subgoals):
 1. \<exists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
 2. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from pd_sub[unfolded pd_sub_def] pairwise_disjnt_imp_sunflower
[PROOF STATE]
proof (chain)
picking this:
G \<subseteq> F \<and> card G = t \<and> pairwise disjnt G \<and> {} \<notin> G
pairwise disjnt ?F \<Longrightarrow> sunflower ?F
[PROOF STEP]
have *: "G \<subseteq> F" "card G = t" "sunflower G" "{} \<notin> G"
[PROOF STATE]
proof (prove)
using this:
G \<subseteq> F \<and> card G = t \<and> pairwise disjnt G \<and> {} \<notin> G
pairwise disjnt ?F \<Longrightarrow> sunflower ?F

goal (1 subgoal):
 1. (G \<subseteq> F &&& card G = t) &&& sunflower G &&& {} \<notin> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
G \<subseteq> F
card G = t
sunflower G
{} \<notin> G

goal (2 subgoals):
 1. \<exists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
 2. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from t \<open>card G = t\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<le> t
card G = t
[PROOF STEP]
obtain H where "H \<subseteq> G" "card H = r"
[PROOF STATE]
proof (prove)
using this:
r \<le> t
card G = t

goal (1 subgoal):
 1. (\<And>H. \<lbrakk>H \<subseteq> G; card H = r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_subset_with_card_n)
[PROOF STATE]
proof (state)
this:
H \<subseteq> G
card H = r

goal (2 subgoals):
 1. \<exists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
 2. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
with sunflower_subset[OF \<open>H \<subseteq> G\<close>] *
[PROOF STATE]
proof (chain)
picking this:
sunflower G \<Longrightarrow> sunflower H
G \<subseteq> F
card G = t
sunflower G
{} \<notin> G
H \<subseteq> G
card H = r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sunflower G \<Longrightarrow> sunflower H
G \<subseteq> F
card G = t
sunflower G
{} \<notin> G
H \<subseteq> G
card H = r

goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>t G. pd_sub G t \<and> r \<le> t

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
define P where "P = (\<lambda> t. \<exists> G. pd_sub G t)"
[PROOF STATE]
proof (state)
this:
P = (\<lambda>t. \<exists>G. pd_sub G t)

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have ex: "\<exists> t. P t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. P t
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t G. pd_sub G t
[PROOF STEP]
by (intro exI[of _ 0] exI[of _ "{}"], auto simp: pd_sub_def)
[PROOF STATE]
proof (state)
this:
\<exists>t. P t

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have large': "\<And> t. P t \<Longrightarrow> t < r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. P t \<Longrightarrow> t < r
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<nexists>t G. pd_sub G t \<and> r \<le> t

goal (1 subgoal):
 1. \<And>t. P t \<Longrightarrow> t < r
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>t G. pd_sub G t \<and> r \<le> t

goal (1 subgoal):
 1. \<And>t. \<exists>G. pd_sub G t \<Longrightarrow> t < r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P ?t \<Longrightarrow> ?t < r

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
hence large: "\<And> t. P t \<Longrightarrow> t \<le> r"
[PROOF STATE]
proof (prove)
using this:
P ?t \<Longrightarrow> ?t < r

goal (1 subgoal):
 1. \<And>t. P t \<Longrightarrow> t \<le> r
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
P ?t \<Longrightarrow> ?t \<le> r

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
define t where "t = (GREATEST t. P t)"
[PROOF STATE]
proof (state)
this:
t = (GREATEST t. P t)

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from GreatestI_ex_nat[OF ex large, folded t_def]
[PROOF STATE]
proof (chain)
picking this:
(\<And>y. P y \<Longrightarrow> P y) \<Longrightarrow> P t
[PROOF STEP]
have Pt: "P t"
[PROOF STATE]
proof (prove)
using this:
(\<And>y. P y \<Longrightarrow> P y) \<Longrightarrow> P t

goal (1 subgoal):
 1. P t
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P t

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from Greatest_le_nat[of P, OF _ large]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P ?k; \<And>y. P y \<Longrightarrow> P y\<rbrakk> \<Longrightarrow> ?k \<le> Greatest P
[PROOF STEP]
have greatest: "\<And> s. P s \<Longrightarrow> s \<le> t"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P ?k; \<And>y. P y \<Longrightarrow> P y\<rbrakk> \<Longrightarrow> ?k \<le> Greatest P

goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> s \<le> t
[PROOF STEP]
unfolding t_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P ?k; \<And>y. P y \<Longrightarrow> P y\<rbrakk> \<Longrightarrow> ?k \<le> Greatest P

goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> s \<le> Greatest P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P ?s \<Longrightarrow> ?s \<le> t

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from large'[OF Pt]
[PROOF STATE]
proof (chain)
picking this:
t < r
[PROOF STEP]
have tr: "t \<le> r - 1"
[PROOF STATE]
proof (prove)
using this:
t < r

goal (1 subgoal):
 1. t \<le> r - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<le> r - 1

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from Pt[unfolded P_def pd_sub_def]
[PROOF STATE]
proof (chain)
picking this:
\<exists>G\<subseteq>F. card G = t \<and> pairwise disjnt G \<and> {} \<notin> G
[PROOF STEP]
obtain G where
      cardG: "card G = t" and
      disj: "pairwise disjnt G" and
      GF: "G \<subseteq> F"
[PROOF STATE]
proof (prove)
using this:
\<exists>G\<subseteq>F. card G = t \<and> pairwise disjnt G \<and> {} \<notin> G

goal (1 subgoal):
 1. (\<And>G. \<lbrakk>card G = t; pairwise disjnt G; G \<subseteq> F\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card G = t
pairwise disjnt G
G \<subseteq> F

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
define A where "A = (\<Union> G)"
[PROOF STATE]
proof (state)
this:
A = \<Union> G

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from Suc(3)
[PROOF STATE]
proof (chain)
picking this:
(r - 1) ^ Suc k * fact (Suc k) < card F
[PROOF STEP]
have "card F > 0"
[PROOF STATE]
proof (prove)
using this:
(r - 1) ^ Suc k * fact (Suc k) < card F

goal (1 subgoal):
 1. 0 < card F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < card F

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
hence "finite F"
[PROOF STATE]
proof (prove)
using this:
0 < card F

goal (1 subgoal):
 1. finite F
[PROOF STEP]
by (rule card_ge_0_finite)
[PROOF STATE]
proof (state)
this:
finite F

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from GF \<open>finite F\<close>
[PROOF STATE]
proof (chain)
picking this:
G \<subseteq> F
finite F
[PROOF STEP]
have finG: "finite G"
[PROOF STATE]
proof (prove)
using this:
G \<subseteq> F
finite F

goal (1 subgoal):
 1. finite G
[PROOF STEP]
by (rule finite_subset)
[PROOF STATE]
proof (state)
this:
finite G

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "card (\<Union> G) \<le> sum card G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union> G) \<le> sum card G
[PROOF STEP]
using card_Union_le_sum_card
[PROOF STATE]
proof (prove)
using this:
card (\<Union> ?U) \<le> sum card ?U

goal (1 subgoal):
 1. card (\<Union> G) \<le> sum card G
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (\<Union> G) \<le> sum card G

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (\<Union> G) \<le> sum card G

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "\<dots> \<le> of_nat (card G) * Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum card G \<le> of_nat (card G) * Suc k
[PROOF STEP]
by (metis GF Suc.prems(1) le_Suc_eq subsetD sum_bounded_above)
[PROOF STATE]
proof (state)
this:
sum card G \<le> of_nat (card G) * Suc k

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum card G \<le> of_nat (card G) * Suc k

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "\<dots> \<le> (r - 1) * Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (card G) * Suc k \<le> (r - 1) * Suc k
[PROOF STEP]
using tr[folded cardG]
[PROOF STATE]
proof (prove)
using this:
card G \<le> r - 1

goal (1 subgoal):
 1. of_nat (card G) * Suc k \<le> (r - 1) * Suc k
[PROOF STEP]
by (metis id_apply mult_le_mono1 of_nat_eq_id)
[PROOF STATE]
proof (state)
this:
of_nat (card G) * Suc k \<le> (r - 1) * Suc k

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (\<Union> G) \<le> (r - 1) * Suc k
[PROOF STEP]
have cardA: "card A \<le> (r - 1) * Suc k"
[PROOF STATE]
proof (prove)
using this:
card (\<Union> G) \<le> (r - 1) * Suc k

goal (1 subgoal):
 1. card A \<le> (r - 1) * Suc k
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
card (\<Union> G) \<le> (r - 1) * Suc k

goal (1 subgoal):
 1. card (\<Union> G) \<le> (r - 1) * Suc k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card A \<le> (r - 1) * Suc k

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
card A \<le> (r - 1) * Suc k

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
assume *: "B \<in> F"
[PROOF STATE]
proof (state)
this:
B \<in> F

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
with Suc(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>F. finite A \<and> card A = Suc k
B \<in> F
[PROOF STEP]
have nE: "B \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. finite A \<and> card A = Suc k
B \<in> F

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

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from Suc(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>F. finite A \<and> card A = Suc k
[PROOF STEP]
have eF: "{} \<notin> F"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. finite A \<and> card A = Suc k

goal (1 subgoal):
 1. {} \<notin> F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{} \<notin> F

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "B \<inter> A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<inter> A \<noteq> {}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B \<inter> A = {} \<Longrightarrow> False
[PROOF STEP]
assume dis: "B \<inter> A = {}"
[PROOF STATE]
proof (state)
this:
B \<inter> A = {}

goal (1 subgoal):
 1. B \<inter> A = {} \<Longrightarrow> False
[PROOF STEP]
hence disj: "pairwise disjnt ({B} \<union> G)"
[PROOF STATE]
proof (prove)
using this:
B \<inter> A = {}

goal (1 subgoal):
 1. pairwise disjnt ({B} \<union> G)
[PROOF STEP]
using disj
[PROOF STATE]
proof (prove)
using this:
B \<inter> A = {}
pairwise disjnt G

goal (1 subgoal):
 1. pairwise disjnt ({B} \<union> G)
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
B \<inter> \<Union> G = {}
pairwise disjnt G

goal (1 subgoal):
 1. pairwise disjnt ({B} \<union> G)
[PROOF STEP]
by (smt (verit, ccfv_SIG) Int_commute Un_iff
              Union_disjoint disjnt_def pairwise_def singleton_iff)
[PROOF STATE]
proof (state)
this:
pairwise disjnt ({B} \<union> G)

goal (1 subgoal):
 1. B \<inter> A = {} \<Longrightarrow> False
[PROOF STEP]
from nE dis
[PROOF STATE]
proof (chain)
picking this:
B \<noteq> {}
B \<inter> A = {}
[PROOF STEP]
have "B \<notin> G"
[PROOF STATE]
proof (prove)
using this:
B \<noteq> {}
B \<inter> A = {}

goal (1 subgoal):
 1. B \<notin> G
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
B \<noteq> {}
B \<inter> \<Union> G = {}

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

goal (1 subgoal):
 1. B \<inter> A = {} \<Longrightarrow> False
[PROOF STEP]
with finG
[PROOF STATE]
proof (chain)
picking this:
finite G
B \<notin> G
[PROOF STEP]
have c: "card ({B} \<union> G) = Suc t"
[PROOF STATE]
proof (prove)
using this:
finite G
B \<notin> G

goal (1 subgoal):
 1. card ({B} \<union> G) = Suc t
[PROOF STEP]
by (simp add: cardG)
[PROOF STATE]
proof (state)
this:
card ({B} \<union> G) = Suc t

goal (1 subgoal):
 1. B \<inter> A = {} \<Longrightarrow> False
[PROOF STEP]
have "P (Suc t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (Suc t)
[PROOF STEP]
unfolding P_def pd_sub_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>G\<subseteq>F. card G = Suc t \<and> pairwise disjnt G \<and> {} \<notin> G
[PROOF STEP]
by (intro exI[of _ "{B} \<union> G"], insert eF disj c * GF, auto)
[PROOF STATE]
proof (state)
this:
P (Suc t)

goal (1 subgoal):
 1. B \<inter> A = {} \<Longrightarrow> False
[PROOF STEP]
with greatest
[PROOF STATE]
proof (chain)
picking this:
P ?s \<Longrightarrow> ?s \<le> t
P (Suc t)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
P ?s \<Longrightarrow> ?s \<le> t
P (Suc t)

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

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

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?B2 \<in> F \<Longrightarrow> ?B2 \<inter> A \<noteq> {}

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
note overlap = this
[PROOF STATE]
proof (state)
this:
?B2 \<in> F \<Longrightarrow> ?B2 \<inter> A \<noteq> {}

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "F \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<noteq> {}
[PROOF STEP]
using Suc(2-)
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. finite A \<and> card A = Suc k
(r - 1) ^ Suc k * fact (Suc k) < card F

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

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
with overlap
[PROOF STATE]
proof (chain)
picking this:
?B2 \<in> F \<Longrightarrow> ?B2 \<inter> A \<noteq> {}
F \<noteq> {}
[PROOF STEP]
have Ane: "A \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
?B2 \<in> F \<Longrightarrow> ?B2 \<inter> A \<noteq> {}
F \<noteq> {}

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
?B2 \<in> F \<Longrightarrow> ?B2 \<inter> \<Union> G \<noteq> {}
F \<noteq> {}

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

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union> G)
[PROOF STEP]
using finG Suc(2-) GF
[PROOF STATE]
proof (prove)
using this:
finite G
\<forall>A\<in>F. finite A \<and> card A = Suc k
(r - 1) ^ Suc k * fact (Suc k) < card F
G \<subseteq> F

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

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
let ?g = "\<lambda> B x. x \<in> B \<inter> A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
define f where "f = (\<lambda> B. SOME x. ?g B x)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>B. SOME x. x \<in> B \<inter> A)

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "f \<in> F \<rightarrow> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> F \<rightarrow> A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> f x \<in> A
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> f x \<in> A
[PROOF STEP]
assume "B \<in> F"
[PROOF STATE]
proof (state)
this:
B \<in> F

goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> f x \<in> A
[PROOF STEP]
from overlap[OF this]
[PROOF STATE]
proof (chain)
picking this:
B \<inter> A \<noteq> {}
[PROOF STEP]
have "\<exists> x. ?g B x"
[PROOF STATE]
proof (prove)
using this:
B \<inter> A \<noteq> {}

goal (1 subgoal):
 1. \<exists>x. x \<in> B \<inter> A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
B \<inter> \<Union> G \<noteq> {}

goal (1 subgoal):
 1. \<exists>x. x \<in> B \<inter> \<Union> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> B \<inter> A

goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> f x \<in> A
[PROOF STEP]
from someI_ex[OF this]
[PROOF STATE]
proof (chain)
picking this:
(SOME x. x \<in> B \<inter> A) \<in> B \<inter> A
[PROOF STEP]
show "f B \<in> A"
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> B \<inter> A) \<in> B \<inter> A

goal (1 subgoal):
 1. f B \<in> A
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> B \<inter> A) \<in> B \<inter> A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f \<in> F \<rightarrow> A

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from pigeonhole_card[OF this \<open>finite F\<close> \<open>finite A\<close> Ane]
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>A. card F \<le> card (f -` {y} \<inter> F) * card A
[PROOF STEP]
obtain a where a: "a \<in> A"
      and le: "card F \<le> card (f -` {a} \<inter> F) * card A"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>A. card F \<le> card (f -` {y} \<inter> F) * card A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; card F \<le> card (f -` {a} \<inter> F) * card A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> A
card F \<le> card (f -` {a} \<inter> F) * card A

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a \<in> A
card F \<le> card (f -` {a} \<inter> F) * card A

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
assume "S \<in> F" "f S \<in> {a}"
[PROOF STATE]
proof (state)
this:
S \<in> F
f S \<in> {a}

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
with someI_ex[of "?g S"] a overlap[OF this(1)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> S \<inter> A \<Longrightarrow> (SOME x. x \<in> S \<inter> A) \<in> S \<inter> A
a \<in> A
S \<inter> A \<noteq> {}
S \<in> F
f S \<in> {a}
[PROOF STEP]
have "a \<in> S"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S \<inter> A \<Longrightarrow> (SOME x. x \<in> S \<inter> A) \<in> S \<inter> A
a \<in> A
S \<inter> A \<noteq> {}
S \<in> F
f S \<in> {a}

goal (1 subgoal):
 1. a \<in> S
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S \<inter> A \<Longrightarrow> (SOME x. x \<in> S \<inter> A) \<in> S \<inter> A
a \<in> A
S \<inter> A \<noteq> {}
S \<in> F
(SOME x. x \<in> S \<inter> A) \<in> {a}

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

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?S2 \<in> F; f ?S2 \<in> {a}\<rbrakk> \<Longrightarrow> a \<in> ?S2

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
note FaS = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?S2 \<in> F; f ?S2 \<in> {a}\<rbrakk> \<Longrightarrow> a \<in> ?S2

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
let ?F = "{S - {a} | S . S \<in> F \<and> f S \<in> {a}}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from cardA
[PROOF STATE]
proof (chain)
picking this:
card A \<le> (r - 1) * Suc k
[PROOF STEP]
have "((r - 1) ^ k * fact k) * card A \<le> ((r - 1) ^ k * fact k) * ((r - 1) * Suc k)"
[PROOF STATE]
proof (prove)
using this:
card A \<le> (r - 1) * Suc k

goal (1 subgoal):
 1. (r - 1) ^ k * fact k * card A \<le> (r - 1) ^ k * fact k * ((r - 1) * Suc k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(r - 1) ^ k * fact k * card A \<le> (r - 1) ^ k * fact k * ((r - 1) * Suc k)

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(r - 1) ^ k * fact k * card A \<le> (r - 1) ^ k * fact k * ((r - 1) * Suc k)

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "\<dots> = (r - 1) ^ (Suc k) * fact (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r - 1) ^ k * fact k * ((r - 1) * Suc k) = (r - 1) ^ Suc k * fact (Suc k)
[PROOF STEP]
by (metis (no_types, lifting) fact_Suc mult.assoc mult.commute of_nat_id power_Suc2)
[PROOF STATE]
proof (state)
this:
(r - 1) ^ k * fact k * ((r - 1) * Suc k) = (r - 1) ^ Suc k * fact (Suc k)

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(r - 1) ^ k * fact k * ((r - 1) * Suc k) = (r - 1) ^ Suc k * fact (Suc k)

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "\<dots> < card (f -` {a} \<inter> F) * card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r - 1) ^ Suc k * fact (Suc k) < card (f -` {a} \<inter> F) * card A
[PROOF STEP]
using Suc(3) le
[PROOF STATE]
proof (prove)
using this:
(r - 1) ^ Suc k * fact (Suc k) < card F
card F \<le> card (f -` {a} \<inter> F) * card A

goal (1 subgoal):
 1. (r - 1) ^ Suc k * fact (Suc k) < card (f -` {a} \<inter> F) * card A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(r - 1) ^ Suc k * fact (Suc k) < card (f -` {a} \<inter> F) * card A

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(r - 1) ^ Suc k * fact (Suc k) < card (f -` {a} \<inter> F) * card A

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "f -` {a} \<inter> F = {S \<in> F. f S \<in> {a}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f -` {a} \<inter> F = {S \<in> F. f S \<in> {a}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f -` {a} \<inter> F = {S \<in> F. f S \<in> {a}}

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f -` {a} \<inter> F = {S \<in> F. f S \<in> {a}}

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "card \<dots> = card ((\<lambda> S. S - {a}) ` {S \<in> F. f S \<in> {a}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {S \<in> F. f S \<in> {a}} = card ((\<lambda>S. S - {a}) ` {S \<in> F. f S \<in> {a}})
[PROOF STEP]
by (subst card_image; intro inj_onI refl, insert FaS) auto
[PROOF STATE]
proof (state)
this:
card {S \<in> F. f S \<in> {a}} = card ((\<lambda>S. S - {a}) ` {S \<in> F. f S \<in> {a}})

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {S \<in> F. f S \<in> {a}} = card ((\<lambda>S. S - {a}) ` {S \<in> F. f S \<in> {a}})

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "(\<lambda> S. S - {a}) ` {S \<in> F. f S \<in> {a}} = ?F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>S. S - {a}) ` {S \<in> F. f S \<in> {a}} = {S - {a} |S. S \<in> F \<and> f S \<in> {a}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>S. S - {a}) ` {S \<in> F. f S \<in> {a}} = {S - {a} |S. S \<in> F \<and> f S \<in> {a}}

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(r - 1) ^ k * fact k * card A < card {S - {a} |S. S \<in> F \<and> f S \<in> {a}} * card A
[PROOF STEP]
have lt: "(r - 1) ^ k * fact k < card ?F"
[PROOF STATE]
proof (prove)
using this:
(r - 1) ^ k * fact k * card A < card {S - {a} |S. S \<in> F \<and> f S \<in> {a}} * card A

goal (1 subgoal):
 1. (r - 1) ^ k * fact k < card {S - {a} |S. S \<in> F \<and> f S \<in> {a}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(r - 1) ^ k * fact k < card {S - {a} |S. S \<in> F \<and> f S \<in> {a}}

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
have "\<forall> A \<in> ?F. finite A \<and> card A = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>{S - {a} |S. S \<in> F \<and> f S \<in> {a}}. finite A \<and> card A = k
[PROOF STEP]
using Suc(2) FaS
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. finite A \<and> card A = Suc k
\<lbrakk>?S2 \<in> F; f ?S2 \<in> {a}\<rbrakk> \<Longrightarrow> a \<in> ?S2

goal (1 subgoal):
 1. \<forall>A\<in>{S - {a} |S. S \<in> F \<and> f S \<in> {a}}. finite A \<and> card A = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>{S - {a} |S. S \<in> F \<and> f S \<in> {a}}. finite A \<and> card A = k

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from Suc(1)[OF this lt]
[PROOF STATE]
proof (chain)
picking this:
\<exists>S\<subseteq>{S - {a} |S. S \<in> F \<and> f S \<in> {a}}. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
obtain S
      where "sunflower S" "card S = r" "S \<subseteq> ?F"
[PROOF STATE]
proof (prove)
using this:
\<exists>S\<subseteq>{S - {a} |S. S \<in> F \<and> f S \<in> {a}}. sunflower S \<and> card S = r \<and> {} \<notin> S

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>sunflower S; card S = r; S \<subseteq> {S - {a} |S. S \<in> F \<and> f S \<in> {a}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sunflower S
card S = r
S \<subseteq> {S - {a} |S. S \<in> F \<and> f S \<in> {a}}

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from \<open>S \<subseteq> ?F\<close> FaS
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> {S - {a} |S. S \<in> F \<and> f S \<in> {a}}
\<lbrakk>?S2 \<in> F; f ?S2 \<in> {a}\<rbrakk> \<Longrightarrow> a \<in> ?S2
[PROOF STEP]
have "S \<subseteq> {A - {a} |A. A \<in> F \<and> a \<in> A}"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> {S - {a} |S. S \<in> F \<and> f S \<in> {a}}
\<lbrakk>?S2 \<in> F; f ?S2 \<in> {a}\<rbrakk> \<Longrightarrow> a \<in> ?S2

goal (1 subgoal):
 1. S \<subseteq> {A - {a} |A. A \<in> F \<and> a \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<subseteq> {A - {a} |A. A \<in> F \<and> a \<in> A}

goal (1 subgoal):
 1. \<nexists>t G. pd_sub G t \<and> r \<le> t \<Longrightarrow> \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
from sunflower_remove_element_lift[OF this \<open>sunflower S\<close>] \<open>card S = r\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>Sa. sunflower Sa \<and> Sa \<subseteq> F \<and> card Sa = card S \<and> Sa = insert a ` S
card S = r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>Sa. sunflower Sa \<and> Sa \<subseteq> F \<and> card Sa = card S \<and> Sa = insert a ` S
card S = r

goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> {} \<notin> S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Erdos_Rado_sunflower:
  assumes "\<forall> A \<in> F. finite A \<and> card A \<le> k"
    and "card F > (r - 1)^k * fact k"
  shows "\<exists> S. S \<subseteq> F \<and> sunflower S \<and> card S = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> card S = r
[PROOF STEP]
by (rule sunflower_card_subset_lift[OF _ assms],
      metis Erdos_Rado_sunflower_same_card)


[STATEMENT]
lemma sunflower_lower_bound:
  assumes inf: "infinite (UNIV :: 'a set)"
    and r: "r \<noteq> 0"
    and rk: "r = 1 \<Longrightarrow> k \<noteq> 0"
  shows "\<exists> F.
    card F = (r - 1)^k \<and> finite F \<and>
    (\<forall> A \<in> F. finite (A :: 'a set) \<and> card A = k) \<and>
    (\<nexists> S. S \<subseteq> F \<and> sunflower S \<and> card S \<ge> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
proof (cases "r = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
 2. r \<noteq> 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r \<noteq> 1

goal (2 subgoals):
 1. r = 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
 2. r \<noteq> 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
with r
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> 0
r \<noteq> 1
[PROOF STEP]
have r: "r > 1"
[PROOF STATE]
proof (prove)
using this:
r \<noteq> 0
r \<noteq> 1

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

goal (2 subgoals):
 1. r = 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
 2. r \<noteq> 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>F. card F = (r - 1) ^ 0 \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = 0) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
 2. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<exists>F. card F = (r - 1) ^ 0 \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = 0) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
 2. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
have id: "S \<subseteq> {{}} \<longleftrightarrow> (S = {} \<or> S = {{}})" for S :: "'a set set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S \<subseteq> {{}}) = (S = {} \<or> S = {{}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(?S \<subseteq> {{}}) = (?S = {} \<or> ?S = {{}})

goal (2 subgoals):
 1. \<exists>F. card F = (r - 1) ^ 0 \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = 0) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
 2. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>F. card F = (r - 1) ^ 0 \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = 0) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
1 < r

goal (1 subgoal):
 1. \<exists>F. card F = (r - 1) ^ 0 \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = 0) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
by (intro exI[of _ "{{}}"], auto simp: id)
[PROOF STATE]
proof (state)
this:
\<exists>F. card F = (r - 1) ^ 0 \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = 0) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)

goal (1 subgoal):
 1. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)

goal (1 subgoal):
 1. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
obtain F where
      cardF: "card F = (r - 1) ^ k" and
      fin: "finite F" and
      AF: "\<And> A. (A :: 'a set) \<in> F \<Longrightarrow> finite A \<and> card A = k" and
      sf: "\<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)"
[PROOF STATE]
proof (prove)
using this:
\<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)

goal (1 subgoal):
 1. (\<And>F. \<lbrakk>card F = (r - 1) ^ k; finite F; \<And>A. A \<in> F \<Longrightarrow> finite A \<and> card A = k; \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
card F = (r - 1) ^ k
finite F
?A \<in> F \<Longrightarrow> finite ?A \<and> card ?A = k
\<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)

goal (1 subgoal):
 1. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
text \<open>main idea: get @{term "k-1 :: nat"} fresh elements
      and add one of these to all elements of F\<close>
[PROOF STATE]
proof (state)
this:
card F = (r - 1) ^ k
finite F
?A \<in> F \<Longrightarrow> finite ?A \<and> card ?A = k
\<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)

goal (1 subgoal):
 1. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
have "finite (\<Union> F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union> F)
[PROOF STEP]
using fin AF
[PROOF STATE]
proof (prove)
using this:
finite F
?A \<in> F \<Longrightarrow> finite ?A \<and> card ?A = k

goal (1 subgoal):
 1. finite (\<Union> F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (\<Union> F)

goal (1 subgoal):
 1. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
hence "infinite (UNIV - \<Union> F)"
[PROOF STATE]
proof (prove)
using this:
finite (\<Union> F)

goal (1 subgoal):
 1. infinite (UNIV - \<Union> F)
[PROOF STEP]
using inf
[PROOF STATE]
proof (prove)
using this:
finite (\<Union> F)
infinite UNIV

goal (1 subgoal):
 1. infinite (UNIV - \<Union> F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
infinite (UNIV - \<Union> F)

goal (1 subgoal):
 1. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
from infinite_arbitrarily_large[OF this, of "r - 1"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>B. finite B \<and> card B = r - 1 \<and> B \<subseteq> UNIV - \<Union> F
[PROOF STEP]
obtain New where New: "finite New" "card New = r - 1"
      "New \<inter> \<Union> F = {}"
[PROOF STATE]
proof (prove)
using this:
\<exists>B. finite B \<and> card B = r - 1 \<and> B \<subseteq> UNIV - \<Union> F

goal (1 subgoal):
 1. (\<And>New. \<lbrakk>finite New; card New = r - 1; New \<inter> \<Union> F = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite New
card New = r - 1
New \<inter> \<Union> F = {}

goal (1 subgoal):
 1. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
define G where "G = (\<lambda> (A, a). insert a A) ` (F \<times> New)"
[PROOF STATE]
proof (state)
this:
G = (\<lambda>(A, a). insert a A) ` (F \<times> New)

goal (1 subgoal):
 1. \<And>k. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S) \<Longrightarrow> \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
proof (intro exI[of _ G] conjI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. card G = (r - 1) ^ Suc k
 2. finite G
 3. \<forall>A\<in>G. finite A \<and> card A = Suc k
 4. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
show "finite G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite G
[PROOF STEP]
using New fin
[PROOF STATE]
proof (prove)
using this:
finite New
card New = r - 1
New \<inter> \<Union> F = {}
finite F

goal (1 subgoal):
 1. finite G
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
using this:
finite New
card New = r - 1
New \<inter> \<Union> F = {}
finite F

goal (1 subgoal):
 1. finite ((\<lambda>(A, a). insert a A) ` (F \<times> New))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite G

goal (3 subgoals):
 1. card G = (r - 1) ^ Suc k
 2. \<forall>A\<in>G. finite A \<and> card A = Suc k
 3. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
have "card G = card (F \<times> New)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card G = card (F \<times> New)
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>(A, a). insert a A) ` (F \<times> New)) = card (F \<times> New)
[PROOF STEP]
proof ((subst card_image; (intro refl)?), intro inj_onI, clarsimp, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>insert b a = insert ba aa; a \<in> F; b \<in> New; aa \<in> F; ba \<in> New\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
case (1 A a B b)
[PROOF STATE]
proof (state)
this:
insert a A = insert b B
A \<in> F
a \<in> New
B \<in> F
b \<in> New

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>insert b a = insert ba aa; a \<in> F; b \<in> New; aa \<in> F; ba \<in> New\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
hence ab: "a = b"
[PROOF STATE]
proof (prove)
using this:
insert a A = insert b B
A \<in> F
a \<in> New
B \<in> F
b \<in> New

goal (1 subgoal):
 1. a = b
[PROOF STEP]
using New
[PROOF STATE]
proof (prove)
using this:
insert a A = insert b B
A \<in> F
a \<in> New
B \<in> F
b \<in> New
finite New
card New = r - 1
New \<inter> \<Union> F = {}

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

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>insert b a = insert ba aa; a \<in> F; b \<in> New; aa \<in> F; ba \<in> New\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
from 1(1)
[PROOF STATE]
proof (chain)
picking this:
insert a A = insert b B
[PROOF STEP]
have "insert a A - {a} = insert b B - {a}"
[PROOF STATE]
proof (prove)
using this:
insert a A = insert b B

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

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>insert b a = insert ba aa; a \<in> F; b \<in> New; aa \<in> F; ba \<in> New\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insert a A - {a} = insert b B - {a}

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>insert b a = insert ba aa; a \<in> F; b \<in> New; aa \<in> F; ba \<in> New\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
have "insert a A - {a} = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert a A - {a} = A
[PROOF STEP]
using New 1
[PROOF STATE]
proof (prove)
using this:
finite New
card New = r - 1
New \<inter> \<Union> F = {}
insert a A = insert b B
A \<in> F
a \<in> New
B \<in> F
b \<in> New

goal (1 subgoal):
 1. insert a A - {a} = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert a A - {a} = A

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>insert b a = insert ba aa; a \<in> F; b \<in> New; aa \<in> F; ba \<in> New\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insert a A - {a} = A

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>insert b a = insert ba aa; a \<in> F; b \<in> New; aa \<in> F; ba \<in> New\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
have "insert b B - {a} = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert b B - {a} = B
[PROOF STEP]
using New 1 ab[symmetric]
[PROOF STATE]
proof (prove)
using this:
finite New
card New = r - 1
New \<inter> \<Union> F = {}
insert a A = insert b B
A \<in> F
a \<in> New
B \<in> F
b \<in> New
b = a

goal (1 subgoal):
 1. insert b B - {a} = B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert b B - {a} = B

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>insert b a = insert ba aa; a \<in> F; b \<in> New; aa \<in> F; ba \<in> New\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A = B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
A = B

goal (1 subgoal):
 1. A = B \<and> a = b
[PROOF STEP]
using ab
[PROOF STATE]
proof (prove)
using this:
A = B
a = b

goal (1 subgoal):
 1. A = B \<and> a = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = B \<and> a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card G = card (F \<times> New)

goal (3 subgoals):
 1. card G = (r - 1) ^ Suc k
 2. \<forall>A\<in>G. finite A \<and> card A = Suc k
 3. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card G = card (F \<times> New)

goal (3 subgoals):
 1. card G = (r - 1) ^ Suc k
 2. \<forall>A\<in>G. finite A \<and> card A = Suc k
 3. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
have "\<dots> = card F * card New"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (F \<times> New) = card F * card New
[PROOF STEP]
using New fin
[PROOF STATE]
proof (prove)
using this:
finite New
card New = r - 1
New \<inter> \<Union> F = {}
finite F

goal (1 subgoal):
 1. card (F \<times> New) = card F * card New
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (F \<times> New) = card F * card New

goal (3 subgoals):
 1. card G = (r - 1) ^ Suc k
 2. \<forall>A\<in>G. finite A \<and> card A = Suc k
 3. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card G = card F * card New
[PROOF STEP]
show "card G = (r - 1) ^ Suc k"
[PROOF STATE]
proof (prove)
using this:
card G = card F * card New

goal (1 subgoal):
 1. card G = (r - 1) ^ Suc k
[PROOF STEP]
unfolding cardF New
[PROOF STATE]
proof (prove)
using this:
card G = (r - 1) ^ k * (r - 1)

goal (1 subgoal):
 1. card G = (r - 1) ^ Suc k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card G = (r - 1) ^ Suc k

goal (2 subgoals):
 1. \<forall>A\<in>G. finite A \<and> card A = Suc k
 2. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
card G = (r - 1) ^ Suc k

goal (2 subgoals):
 1. \<forall>A\<in>G. finite A \<and> card A = Suc k
 2. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>A\<in>G. finite A \<and> card A = Suc k
 2. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
assume "B \<in> G"
[PROOF STATE]
proof (state)
this:
B \<in> G

goal (2 subgoals):
 1. \<forall>A\<in>G. finite A \<and> card A = Suc k
 2. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<in> G
[PROOF STEP]
obtain a A where G: "a \<in> New" "A \<in> F" "B = insert a A"
[PROOF STATE]
proof (prove)
using this:
B \<in> G

goal (1 subgoal):
 1. (\<And>a A. \<lbrakk>a \<in> New; A \<in> F; B = insert a A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
using this:
B \<in> (\<lambda>(A, a). insert a A) ` (F \<times> New)

goal (1 subgoal):
 1. (\<And>a A. \<lbrakk>a \<in> New; A \<in> F; B = insert a A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> New
A \<in> F
B = insert a A

goal (2 subgoals):
 1. \<forall>A\<in>G. finite A \<and> card A = Suc k
 2. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
with AF[of A] New
[PROOF STATE]
proof (chain)
picking this:
A \<in> F \<Longrightarrow> finite A \<and> card A = k
finite New
card New = r - 1
New \<inter> \<Union> F = {}
a \<in> New
A \<in> F
B = insert a A
[PROOF STEP]
have "finite B" "card B = Suc k"
[PROOF STATE]
proof (prove)
using this:
A \<in> F \<Longrightarrow> finite A \<and> card A = k
finite New
card New = r - 1
New \<inter> \<Union> F = {}
a \<in> New
A \<in> F
B = insert a A

goal (1 subgoal):
 1. finite B &&& card B = Suc k
[PROOF STEP]
by (auto simp: card_insert_if)
[PROOF STATE]
proof (state)
this:
finite B
card B = Suc k

goal (2 subgoals):
 1. \<forall>A\<in>G. finite A \<and> card A = Suc k
 2. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?B2 \<in> G \<Longrightarrow> finite ?B2
?B2 \<in> G \<Longrightarrow> card ?B2 = Suc k

goal (2 subgoals):
 1. \<forall>A\<in>G. finite A \<and> card A = Suc k
 2. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
thus "\<forall>A\<in>G. finite A \<and> card A = Suc k"
[PROOF STATE]
proof (prove)
using this:
?B2 \<in> G \<Longrightarrow> finite ?B2
?B2 \<in> G \<Longrightarrow> card ?B2 = Suc k

goal (1 subgoal):
 1. \<forall>A\<in>G. finite A \<and> card A = Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>G. finite A \<and> card A = Suc k

goal (1 subgoal):
 1. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
show "\<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)
[PROOF STEP]
proof (intro notI, elim exE conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume *: "S \<subseteq> G" "sunflower S" "r \<le> card S"
[PROOF STATE]
proof (state)
this:
S \<subseteq> G
sunflower S
r \<le> card S

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
define g where "g B = (SOME a. a \<in> New \<and> a \<in> B)" for B
[PROOF STATE]
proof (state)
this:
g ?B = (SOME a. a \<in> New \<and> a \<in> ?B)

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g ?B = (SOME a. a \<in> New \<and> a \<in> ?B)

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "B \<in> S"
[PROOF STATE]
proof (state)
this:
B \<in> S

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>S \<subseteq> G\<close>
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> G
B \<in> S
[PROOF STEP]
have "B \<in> G"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> G
B \<in> S

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

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "\<exists> a. a \<in> New \<and> a \<in> B"
[PROOF STATE]
proof (prove)
using this:
B \<in> G

goal (1 subgoal):
 1. \<exists>a. a \<in> New \<and> a \<in> B
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
using this:
B \<in> (\<lambda>(A, a). insert a A) ` (F \<times> New)

goal (1 subgoal):
 1. \<exists>a. a \<in> New \<and> a \<in> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a. a \<in> New \<and> a \<in> B

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from someI_ex[OF this, folded g_def]
[PROOF STATE]
proof (chain)
picking this:
g B \<in> New \<and> g B \<in> B
[PROOF STEP]
have "g B \<in> New" "g B \<in> B"
[PROOF STATE]
proof (prove)
using this:
g B \<in> New \<and> g B \<in> B

goal (1 subgoal):
 1. g B \<in> New &&& g B \<in> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g B \<in> New
g B \<in> B

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?B2 \<in> S \<Longrightarrow> g ?B2 \<in> New
?B2 \<in> S \<Longrightarrow> g ?B2 \<in> ?B2

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note gB = this
[PROOF STATE]
proof (state)
this:
?B2 \<in> S \<Longrightarrow> g ?B2 \<in> New
?B2 \<in> S \<Longrightarrow> g ?B2 \<in> ?B2

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "card (g ` S) \<le> card New"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (g ` S) \<le> card New
[PROOF STEP]
by (rule card_mono, insert New gB, auto)
[PROOF STATE]
proof (state)
this:
card (g ` S) \<le> card New

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (g ` S) \<le> card New

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> < r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card New < r
[PROOF STEP]
unfolding New
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r - 1 < r
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
1 < r

goal (1 subgoal):
 1. r - 1 < r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card New < r

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card New < r

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<le> card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> card S
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
r \<le> card S

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (g ` S) < card S
[PROOF STEP]
have "card (g ` S) < card S"
[PROOF STATE]
proof (prove)
using this:
card (g ` S) < card S

goal (1 subgoal):
 1. card (g ` S) < card S
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card (g ` S) < card S

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from pigeonhole[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<not> inj_on g S
[PROOF STEP]
have "\<not> inj_on g S"
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on g S

goal (1 subgoal):
 1. \<not> inj_on g S
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> inj_on g S

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> inj_on g S
[PROOF STEP]
obtain B1 B2 where B12: "B1 \<in> S" "B2 \<in> S" "B1 \<noteq> B2" "g B1 = g B2"
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on g S

goal (1 subgoal):
 1. (\<And>B1 B2. \<lbrakk>B1 \<in> S; B2 \<in> S; B1 \<noteq> B2; g B1 = g B2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x\<in>S. \<forall>y\<in>S. g x = g y \<longrightarrow> x = y)

goal (1 subgoal):
 1. (\<And>B1 B2. \<lbrakk>B1 \<in> S; B2 \<in> S; B1 \<noteq> B2; g B1 = g B2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B1 \<in> S
B2 \<in> S
B1 \<noteq> B2
g B1 = g B2

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
define a where "a = g B2"
[PROOF STATE]
proof (state)
this:
a = g B2

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from B12 gB[of B1] gB[of B2]
[PROOF STATE]
proof (chain)
picking this:
B1 \<in> S
B2 \<in> S
B1 \<noteq> B2
g B1 = g B2
B1 \<in> S \<Longrightarrow> g B1 \<in> New
B1 \<in> S \<Longrightarrow> g B1 \<in> B1
B2 \<in> S \<Longrightarrow> g B2 \<in> New
B2 \<in> S \<Longrightarrow> g B2 \<in> B2
[PROOF STEP]
have a: "a \<in> New" "a \<in> B1" "a \<in> B2"
[PROOF STATE]
proof (prove)
using this:
B1 \<in> S
B2 \<in> S
B1 \<noteq> B2
g B1 = g B2
B1 \<in> S \<Longrightarrow> g B1 \<in> New
B1 \<in> S \<Longrightarrow> g B1 \<in> B1
B2 \<in> S \<Longrightarrow> g B2 \<in> New
B2 \<in> S \<Longrightarrow> g B2 \<in> B2

goal (1 subgoal):
 1. a \<in> New &&& a \<in> B1 &&& a \<in> B2
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
using this:
B1 \<in> S
B2 \<in> S
B1 \<noteq> B2
g B1 = g B2
B1 \<in> S \<Longrightarrow> g B1 \<in> New
B1 \<in> S \<Longrightarrow> g B1 \<in> B1
B2 \<in> S \<Longrightarrow> g B2 \<in> New
B2 \<in> S \<Longrightarrow> g B2 \<in> B2

goal (1 subgoal):
 1. g B2 \<in> New &&& g B2 \<in> B1 &&& g B2 \<in> B2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> New
a \<in> B1
a \<in> B2

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with B12
[PROOF STATE]
proof (chain)
picking this:
B1 \<in> S
B2 \<in> S
B1 \<noteq> B2
g B1 = g B2
a \<in> New
a \<in> B1
a \<in> B2
[PROOF STEP]
have "\<exists>B1 B2. B1 \<in> S \<and> B2 \<in> S \<and> B1 \<noteq> B2 \<and> a \<in> B1 \<and> a \<in> B2"
[PROOF STATE]
proof (prove)
using this:
B1 \<in> S
B2 \<in> S
B1 \<noteq> B2
g B1 = g B2
a \<in> New
a \<in> B1
a \<in> B2

goal (1 subgoal):
 1. \<exists>B1 B2. B1 \<in> S \<and> B2 \<in> S \<and> B1 \<noteq> B2 \<and> a \<in> B1 \<and> a \<in> B2
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
using this:
B1 \<in> S
B2 \<in> S
B1 \<noteq> B2
g B1 = g B2
g B2 \<in> New
g B2 \<in> B1
g B2 \<in> B2

goal (1 subgoal):
 1. \<exists>B1 B2a. B1 \<in> S \<and> B2a \<in> S \<and> B1 \<noteq> B2a \<and> g B2 \<in> B1 \<and> g B2 \<in> B2a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>B1 B2. B1 \<in> S \<and> B2 \<in> S \<and> B1 \<noteq> B2 \<and> a \<in> B1 \<and> a \<in> B2

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>sunflower S\<close>[unfolded sunflower_def, rule_format, OF this]
[PROOF STATE]
proof (chain)
picking this:
?A \<in> S \<Longrightarrow> a \<in> ?A
[PROOF STEP]
have aS: "B \<in> S \<Longrightarrow> a \<in> B" for B
[PROOF STATE]
proof (prove)
using this:
?A \<in> S \<Longrightarrow> a \<in> ?A

goal (1 subgoal):
 1. B \<in> S \<Longrightarrow> a \<in> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?B \<in> S \<Longrightarrow> a \<in> ?B

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
define h where "h B = B - {a}" for B
[PROOF STATE]
proof (state)
this:
h ?B = ?B - {a}

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
define T where "T = h ` S"
[PROOF STATE]
proof (state)
this:
T = h ` S

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S
[PROOF STEP]
proof (intro exI[of _ T] conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
assume "B \<in> S"
[PROOF STATE]
proof (state)
this:
B \<in> S

goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
have hB: "h B = B - {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h B = B - {a}
[PROOF STEP]
unfolding h_def T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B - {a} = B - {a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h B = B - {a}

goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
from aS \<open>B \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
?B \<in> S \<Longrightarrow> a \<in> ?B
B \<in> S
[PROOF STEP]
have aB: "a \<in> B"
[PROOF STATE]
proof (prove)
using this:
?B \<in> S \<Longrightarrow> a \<in> ?B
B \<in> S

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

goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
from \<open>B \<in> S\<close> \<open>S \<subseteq> G\<close>
[PROOF STATE]
proof (chain)
picking this:
B \<in> S
S \<subseteq> G
[PROOF STEP]
obtain a' A where AF: "A \<in> F"
              and B: "B = insert a' A"
              and a': "a' \<in> New"
[PROOF STATE]
proof (prove)
using this:
B \<in> S
S \<subseteq> G

goal (1 subgoal):
 1. (\<And>A a'. \<lbrakk>A \<in> F; B = insert a' A; a' \<in> New\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
using this:
B \<in> S
S \<subseteq> (\<lambda>(A, a). insert a A) ` (F \<times> New)

goal (1 subgoal):
 1. (\<And>A a'. \<lbrakk>A \<in> F; B = insert a' A; a' \<in> New\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
A \<in> F
B = insert a' A
a' \<in> New

goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
from aB B a' New AF a(1) hB AF
[PROOF STATE]
proof (chain)
picking this:
a \<in> B
B = insert a' A
a' \<in> New
finite New
card New = r - 1
New \<inter> \<Union> F = {}
A \<in> F
a \<in> New
h B = B - {a}
A \<in> F
[PROOF STEP]
have "insert a (h B) = B" "h B = A"
[PROOF STATE]
proof (prove)
using this:
a \<in> B
B = insert a' A
a' \<in> New
finite New
card New = r - 1
New \<inter> \<Union> F = {}
A \<in> F
a \<in> New
h B = B - {a}
A \<in> F

goal (1 subgoal):
 1. insert a (h B) = B &&& h B = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert a (h B) = B
h B = A

goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
hence "insert a (h B) = B" "h B \<in> F" "insert a (h B) \<in> S"
[PROOF STATE]
proof (prove)
using this:
insert a (h B) = B
h B = A

goal (1 subgoal):
 1. insert a (h B) = B &&& h B \<in> F &&& insert a (h B) \<in> S
[PROOF STEP]
using AF \<open>B \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
insert a (h B) = B
h B = A
A \<in> F
B \<in> S

goal (1 subgoal):
 1. insert a (h B) = B &&& h B \<in> F &&& insert a (h B) \<in> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert a (h B) = B
h B \<in> F
insert a (h B) \<in> S

goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) = ?B2
?B2 \<in> S \<Longrightarrow> h ?B2 \<in> F
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) \<in> S

goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) = ?B2
?B2 \<in> S \<Longrightarrow> h ?B2 \<in> F
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) \<in> S

goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
have CTS: "C \<in> T \<Longrightarrow> insert a C \<in> S" for C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<in> T \<Longrightarrow> insert a C \<in> S
[PROOF STEP]
using main
[PROOF STATE]
proof (prove)
using this:
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) = ?B2
?B2 \<in> S \<Longrightarrow> h ?B2 \<in> F
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) \<in> S

goal (1 subgoal):
 1. C \<in> T \<Longrightarrow> insert a C \<in> S
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
using this:
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) = ?B2
?B2 \<in> S \<Longrightarrow> h ?B2 \<in> F
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) \<in> S

goal (1 subgoal):
 1. C \<in> h ` S \<Longrightarrow> insert a C \<in> S
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?C \<in> T \<Longrightarrow> insert a ?C \<in> S

goal (3 subgoals):
 1. T \<subseteq> F
 2. sunflower T
 3. r \<le> card T
[PROOF STEP]
show "T \<subseteq> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T \<subseteq> F
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h ` S \<subseteq> F
[PROOF STEP]
using main
[PROOF STATE]
proof (prove)
using this:
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) = ?B2
?B2 \<in> S \<Longrightarrow> h ?B2 \<in> F
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) \<in> S

goal (1 subgoal):
 1. h ` S \<subseteq> F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T \<subseteq> F

goal (2 subgoals):
 1. sunflower T
 2. r \<le> card T
[PROOF STEP]
have "r \<le> card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> card S
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
r \<le> card S

goal (2 subgoals):
 1. sunflower T
 2. r \<le> card T
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r \<le> card S

goal (2 subgoals):
 1. sunflower T
 2. r \<le> card T
[PROOF STEP]
have "\<dots> = card T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card S = card T
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card S = card (h ` S)
[PROOF STEP]
by (subst card_image, intro inj_on_inverseI[of _ "insert a"], insert main, auto)
[PROOF STATE]
proof (state)
this:
card S = card T

goal (2 subgoals):
 1. sunflower T
 2. r \<le> card T
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r \<le> card T
[PROOF STEP]
show "r \<le> card T"
[PROOF STATE]
proof (prove)
using this:
r \<le> card T

goal (1 subgoal):
 1. r \<le> card T
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r \<le> card T

goal (1 subgoal):
 1. sunflower T
[PROOF STEP]
show "sunflower T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sunflower T
[PROOF STEP]
unfolding sunflower_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<exists>A B. A \<in> T \<and> B \<in> T \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B) \<longrightarrow> (\<forall>A. A \<in> T \<longrightarrow> x \<in> A)
[PROOF STEP]
proof (intro allI impI, elim exE conjE, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x A Aa B. \<lbrakk>A \<in> T; Aa \<in> T; B \<in> T; Aa \<noteq> B; x \<in> Aa; x \<in> B\<rbrakk> \<Longrightarrow> x \<in> A
[PROOF STEP]
case (1 x C C1 C2)
[PROOF STATE]
proof (state)
this:
C \<in> T
C1 \<in> T
C2 \<in> T
C1 \<noteq> C2
x \<in> C1
x \<in> C2

goal (1 subgoal):
 1. \<And>x A Aa B. \<lbrakk>A \<in> T; Aa \<in> T; B \<in> T; Aa \<noteq> B; x \<in> Aa; x \<in> B\<rbrakk> \<Longrightarrow> x \<in> A
[PROOF STEP]
from CTS[OF \<open>C1 \<in> T\<close>] CTS[OF \<open>C2 \<in> T\<close>] CTS[OF \<open>C \<in> T\<close>]
[PROOF STATE]
proof (chain)
picking this:
insert a C1 \<in> S
insert a C2 \<in> S
insert a C \<in> S
[PROOF STEP]
have *: "insert a C1 \<in> S" "insert a C2 \<in> S" "insert a C \<in> S"
[PROOF STATE]
proof (prove)
using this:
insert a C1 \<in> S
insert a C2 \<in> S
insert a C \<in> S

goal (1 subgoal):
 1. insert a C1 \<in> S &&& insert a C2 \<in> S &&& insert a C \<in> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert a C1 \<in> S
insert a C2 \<in> S
insert a C \<in> S

goal (1 subgoal):
 1. \<And>x A Aa B. \<lbrakk>A \<in> T; Aa \<in> T; B \<in> T; Aa \<noteq> B; x \<in> Aa; x \<in> B\<rbrakk> \<Longrightarrow> x \<in> A
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
C \<in> T
C1 \<in> T
C2 \<in> T
C1 \<noteq> C2
x \<in> C1
x \<in> C2
[PROOF STEP]
have "insert a C1 \<noteq> insert a C2"
[PROOF STATE]
proof (prove)
using this:
C \<in> T
C1 \<in> T
C2 \<in> T
C1 \<noteq> C2
x \<in> C1
x \<in> C2

goal (1 subgoal):
 1. insert a C1 \<noteq> insert a C2
[PROOF STEP]
using main
[PROOF STATE]
proof (prove)
using this:
C \<in> T
C1 \<in> T
C2 \<in> T
C1 \<noteq> C2
x \<in> C1
x \<in> C2
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) = ?B2
?B2 \<in> S \<Longrightarrow> h ?B2 \<in> F
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) \<in> S

goal (1 subgoal):
 1. insert a C1 \<noteq> insert a C2
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
using this:
C \<in> h ` S
C1 \<in> h ` S
C2 \<in> h ` S
C1 \<noteq> C2
x \<in> C1
x \<in> C2
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) = ?B2
?B2 \<in> S \<Longrightarrow> h ?B2 \<in> F
?B2 \<in> S \<Longrightarrow> insert a (h ?B2) \<in> S

goal (1 subgoal):
 1. insert a C1 \<noteq> insert a C2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert a C1 \<noteq> insert a C2

goal (1 subgoal):
 1. \<And>x A Aa B. \<lbrakk>A \<in> T; Aa \<in> T; B \<in> T; Aa \<noteq> B; x \<in> Aa; x \<in> B\<rbrakk> \<Longrightarrow> x \<in> A
[PROOF STEP]
hence "\<exists>A B. A \<in> S \<and> B \<in> S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B"
[PROOF STATE]
proof (prove)
using this:
insert a C1 \<noteq> insert a C2

goal (1 subgoal):
 1. \<exists>A B. A \<in> S \<and> B \<in> S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B
[PROOF STEP]
using * 1
[PROOF STATE]
proof (prove)
using this:
insert a C1 \<noteq> insert a C2
insert a C1 \<in> S
insert a C2 \<in> S
insert a C \<in> S
C \<in> T
C1 \<in> T
C2 \<in> T
C1 \<noteq> C2
x \<in> C1
x \<in> C2

goal (1 subgoal):
 1. \<exists>A B. A \<in> S \<and> B \<in> S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>A B. A \<in> S \<and> B \<in> S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B

goal (1 subgoal):
 1. \<And>x A Aa B. \<lbrakk>A \<in> T; Aa \<in> T; B \<in> T; Aa \<noteq> B; x \<in> Aa; x \<in> B\<rbrakk> \<Longrightarrow> x \<in> A
[PROOF STEP]
from \<open>sunflower S\<close>[unfolded sunflower_def, rule_format, OF this *(3)]
[PROOF STATE]
proof (chain)
picking this:
x \<in> insert a C
[PROOF STEP]
have "x \<in> insert a C"
[PROOF STATE]
proof (prove)
using this:
x \<in> insert a C

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

goal (1 subgoal):
 1. \<And>x A Aa B. \<lbrakk>A \<in> T; Aa \<in> T; B \<in> T; Aa \<noteq> B; x \<in> Aa; x \<in> B\<rbrakk> \<Longrightarrow> x \<in> A
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
C \<in> T
C1 \<in> T
C2 \<in> T
C1 \<noteq> C2
x \<in> C1
x \<in> C2
x \<in> insert a C
[PROOF STEP]
show "x \<in> C"
[PROOF STATE]
proof (prove)
using this:
C \<in> T
C1 \<in> T
C2 \<in> T
C1 \<noteq> C2
x \<in> C1
x \<in> C2
x \<in> insert a C

goal (1 subgoal):
 1. x \<in> C
[PROOF STEP]
unfolding T_def h_def
[PROOF STATE]
proof (prove)
using this:
C \<in> (\<lambda>B. B - {a}) ` S
C1 \<in> (\<lambda>B. B - {a}) ` S
C2 \<in> (\<lambda>B. B - {a}) ` S
C1 \<noteq> C2
x \<in> C1
x \<in> C2
x \<in> insert a C

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sunflower T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S

goal (1 subgoal):
 1. \<And>S. \<lbrakk>S \<subseteq> G; sunflower S; r \<le> card S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with sf
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>F. card F = (r - 1) ^ Suc k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)

goal (1 subgoal):
 1. r = 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r = 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
case r: True
[PROOF STATE]
proof (state)
this:
r = 1

goal (1 subgoal):
 1. r = 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
with rk
[PROOF STATE]
proof (chain)
picking this:
r = 1 \<Longrightarrow> k \<noteq> 0
r = 1
[PROOF STEP]
have "k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
r = 1 \<Longrightarrow> k \<noteq> 0
r = 1

goal (1 subgoal):
 1. k \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. r = 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
[PROOF STEP]
obtain l where k: "k = Suc l"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0

goal (1 subgoal):
 1. (\<And>l. k = Suc l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases k, auto)
[PROOF STATE]
proof (state)
this:
k = Suc l

goal (1 subgoal):
 1. r = 1 \<Longrightarrow> \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)
[PROOF STEP]
unfolding r k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>F. card F = (1 - 1) ^ Suc l \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = Suc l) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> 1 \<le> card S)
[PROOF STEP]
by (intro exI[of _ "{}"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>F. card F = (r - 1) ^ k \<and> finite F \<and> (\<forall>A\<in>F. finite A \<and> card A = k) \<and> \<not> (\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Erdos_Rado_sunflower_card_core:
  assumes "finite E"
    and "\<forall> A \<in> F. A \<subseteq> E \<and> s \<le> card A \<and> card A \<le> k"
    and "card F > (card E choose s) * (r - 1)^k * fact k"
    and "s \<noteq> 0"
    and "r \<noteq> 0"
  shows "\<exists> S. S \<subseteq> F \<and> sunflower S \<and> card S = r \<and> card (\<Inter> S) \<ge> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> s \<le> card (\<Inter> S)
[PROOF STEP]
by (rule sunflower_card_core_lift[OF assms(1) _ assms(2) _ assms(4-5),
        of "(r - 1)^k * fact k"],
      rule Erdos_Rado_sunflower, insert assms(3), auto simp: ac_simps)


[STATEMENT]
lemma Erdos_Rado_sunflower_nonempty_core:
  assumes "finite E"
    and "\<forall> A \<in> F. A \<subseteq> E \<and> card A \<le> k"
    and "{} \<notin> F"
    and "card F > card E * (r - 1)^k * fact k"
  shows "\<exists> S. S \<subseteq> F \<and> sunflower S \<and> card S = r \<and> \<Inter> S \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S\<subseteq>F. sunflower S \<and> card S = r \<and> \<Inter> S \<noteq> {}
[PROOF STEP]
by (rule sunflower_nonempty_core_lift[OF assms(1)
      _ assms(2-3), of "(r - 1)^k * fact k"],
      rule Erdos_Rado_sunflower, insert assms(4), auto simp: ac_simps)


[STATEMENT]
lemma WT_lassocr\<^sub>C [WT_intro]: "(\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3, \<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3) \<turnstile>\<^sub>C lassocr\<^sub>C \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3, \<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3) \<turnstile>\<^sub>C lassocr\<^sub>C \<surd>
[PROOF STEP]
by(coinduction)(auto simp add: lassocr\<^sub>C_def)


[STATEMENT]
lemma WT_rassocl\<^sub>C [WT_intro]: "\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3), (\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3 \<turnstile>\<^sub>C rassocl\<^sub>C \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3), (\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3 \<turnstile>\<^sub>C rassocl\<^sub>C \<surd>
[PROOF STEP]
by(coinduction)(auto simp add: rassocl\<^sub>C_def)


[STATEMENT]
lemma WT_swap\<^sub>C [WT_intro]: "\<I>1 \<oplus>\<^sub>\<I> \<I>2, \<I>2 \<oplus>\<^sub>\<I> \<I>1 \<turnstile>\<^sub>C swap\<^sub>C \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> \<I>2, \<I>2 \<oplus>\<^sub>\<I> \<I>1 \<turnstile>\<^sub>C swap\<^sub>C \<surd>
[PROOF STEP]
by(coinduction)(auto simp add: swap\<^sub>C_def)


[STATEMENT]
lemma WT_swap_lassocr [WT_intro]: "\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3), \<I>2 \<oplus>\<^sub>\<I> (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<turnstile>\<^sub>C swap_lassocr \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3), \<I>2 \<oplus>\<^sub>\<I> (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<turnstile>\<^sub>C swap_lassocr \<surd>
[PROOF STEP]
unfolding swap_lassocr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3), \<I>2 \<oplus>\<^sub>\<I> (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<turnstile>\<^sub>C rassocl\<^sub>C \<odot> (swap\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> lassocr\<^sub>C \<surd>
[PROOF STEP]
by(rule WT_converter_comp WT_lassocr\<^sub>C WT_rassocl\<^sub>C WT_converter_parallel_converter2 WT_converter_id WT_swap\<^sub>C)+


[STATEMENT]
lemma WT_swap_rassocl [WT_intro]: "(\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3, (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<oplus>\<^sub>\<I> \<I>2 \<turnstile>\<^sub>C swap_rassocl \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3, (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<oplus>\<^sub>\<I> \<I>2 \<turnstile>\<^sub>C swap_rassocl \<surd>
[PROOF STEP]
unfolding swap_rassocl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3, (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<oplus>\<^sub>\<I> \<I>2 \<turnstile>\<^sub>C lassocr\<^sub>C \<odot> (1\<^sub>C |\<^sub>= swap\<^sub>C) \<odot> rassocl\<^sub>C \<surd>
[PROOF STEP]
by(rule WT_converter_comp WT_lassocr\<^sub>C WT_rassocl\<^sub>C WT_converter_parallel_converter2 WT_converter_id WT_swap\<^sub>C)+


[STATEMENT]
lemma WT_parallel_wiring [WT_intro]:
  "(\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> (\<I>3 \<oplus>\<^sub>\<I> \<I>4), (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>4) \<turnstile>\<^sub>C parallel_wiring \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> (\<I>3 \<oplus>\<^sub>\<I> \<I>4), (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>4) \<turnstile>\<^sub>C parallel_wiring \<surd>
[PROOF STEP]
unfolding parallel_wiring_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> (\<I>3 \<oplus>\<^sub>\<I> \<I>4), (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>4) \<turnstile>\<^sub>C lassocr\<^sub>C \<odot> (1\<^sub>C |\<^sub>= swap_lassocr) \<odot> rassocl\<^sub>C \<surd>
[PROOF STEP]
by(rule WT_converter_comp WT_lassocr\<^sub>C WT_rassocl\<^sub>C WT_converter_parallel_converter2 WT_converter_id WT_swap_lassocr)+


[STATEMENT]
lemma map_swap_sum_plus_oracle: includes lifting_syntax shows
  "(id ---> swap_sum ---> map_spmf (map_prod swap_sum id)) (oracle1 \<oplus>\<^sub>O oracle2) =
   (oracle2 \<oplus>\<^sub>O oracle1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (id ---> swap_sum ---> map_spmf (map_prod swap_sum id)) (oracle1 \<oplus>\<^sub>O oracle2) = oracle2 \<oplus>\<^sub>O oracle1
[PROOF STEP]
proof ((rule ext)+; goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. (id ---> swap_sum ---> map_spmf (map_prod swap_sum id)) (oracle1 \<oplus>\<^sub>O oracle2) x xa = (oracle2 \<oplus>\<^sub>O oracle1) x xa
[PROOF STEP]
case (1 s q)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>x xa. (id ---> swap_sum ---> map_spmf (map_prod swap_sum id)) (oracle1 \<oplus>\<^sub>O oracle2) x xa = (oracle2 \<oplus>\<^sub>O oracle1) x xa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (id ---> swap_sum ---> map_spmf (map_prod swap_sum id)) (oracle1 \<oplus>\<^sub>O oracle2) s q = (oracle2 \<oplus>\<^sub>O oracle1) s q
[PROOF STEP]
by (cases q) (simp_all add: spmf.map_comp o_def apfst_def prod.map_comp id_def)
[PROOF STATE]
proof (state)
this:
(id ---> swap_sum ---> map_spmf (map_prod swap_sum id)) (oracle1 \<oplus>\<^sub>O oracle2) s q = (oracle2 \<oplus>\<^sub>O oracle1) s q

goal:
No subgoals!
[PROOF STEP]
qed