diff --git a/thys/Irrationals_From_THEBOOK/Irrationals_From_THEBOOK.thy b/thys/Irrationals_From_THEBOOK/Irrationals_From_THEBOOK.thy
--- a/thys/Irrationals_From_THEBOOK/Irrationals_From_THEBOOK.thy
+++ b/thys/Irrationals_From_THEBOOK/Irrationals_From_THEBOOK.thy
@@ -1,297 +1,290 @@
 section \<open>Some irrational numbers\<close>
 text \<open>From Aigner and Ziegler, \emph{Proofs from THE BOOK} (Springer, 2018), Chapter 8, pp. 50--51.\<close>
 
 theory Irrationals_From_THEBOOK imports "Stirling_Formula.Stirling_Formula"
    
 begin
 
-subsection \<open>Library additions\<close>
-
-lemma field_differentiable_diff_const [simp,derivative_intros]:
-  "(-)c field_differentiable F"
-  unfolding field_differentiable_def
-  by (rule derivative_eq_intros exI | force)+
-
 subsection \<open>Basic definitions and their consequences\<close>
 
 definition hf where "hf \<equiv> \<lambda>n. \<lambda>x::real. (x^n * (1-x)^n) / fact n"
 
 definition cf where "cf \<equiv> \<lambda>n i. if i < n then 0 else (n choose (i-n)) * (-1)^(i-n)"
 
 text \<open>Mere knowledge that the coefficients are integers is not enough later on.\<close>
 lemma hf_int_poly:
   fixes x::real
   shows "hf n = (\<lambda>x. (1 / fact n) * (\<Sum>i=0..2*n. real_of_int (cf n i) * x^i))"
 proof 
   fix x
   have inj: "inj_on ((+)n) {..n}" 
     by (auto simp: inj_on_def)
   have [simp]: "((+)n) ` {..n} = {n..2*n}"
     using nat_le_iff_add by fastforce
   have "(x^n * (-x + 1)^n) = x ^ n * (\<Sum>k\<le>n. real (n choose k) * (- x) ^ k)"
     unfolding binomial_ring by simp
   also have "\<dots> = x ^ n * (\<Sum>k\<le>n. real_of_int ((n choose k) * (-1)^k) * x ^ k)"
     by (simp add: mult.assoc flip: power_minus)
   also have "\<dots> = (\<Sum>k\<le>n. real_of_int ((n choose k) * (-1)^k) * x ^ (n+k))"
     by (simp add: sum_distrib_left mult_ac power_add)
   also have "\<dots> = (\<Sum>i=n..2*n. real_of_int (cf n i) * x^i)"
     by (simp add: sum.reindex [OF inj, simplified] cf_def)
   finally have "hf n x = (1 / fact n) * (\<Sum>i = n..2 * n. real_of_int (cf n i) * x^i)"
     by (simp add: hf_def)
   moreover have "(\<Sum>i = 0..<n. real_of_int (cf n i) * x^i) = 0"
     by (simp add: cf_def)
   ultimately show "hf n x = (1 / fact n) * (\<Sum>i = 0..2 * n. real_of_int (cf n i) * x^i)"
     using sum.union_disjoint [of "{0..<n}" "{n..2*n}" "\<lambda>i. real_of_int (cf n i) * x^i"]
     by (simp add: ivl_disj_int_two(7) ivl_disj_un_two(7) mult_2)
 qed
 
 text \<open>Lemma (ii) in the text has strict inequalities, but that's more work and is less useful.\<close>
 lemma 
   assumes "0 \<le> x" "x \<le> 1" 
   shows hf_nonneg: "0 \<le> hf n x" and hf_le_inverse_fact: "hf n x \<le> 1/fact n"
   using assms by (auto simp: hf_def divide_simps mult_le_one power_le_one)
 
 lemma hf_differt [iff]: "hf n differentiable at x"
   unfolding hf_int_poly differentiable_def
   by (intro derivative_eq_intros exI | simp)+
 
 lemma deriv_sum_int:
   "deriv (\<lambda>x. \<Sum>i=0..n. real_of_int (c i) * x^i) x 
      = (if n=0 then 0 else (\<Sum>i=0..n - Suc 0. real_of_int ((int i + 1) * c (Suc i)) * x^i))"
   (is "deriv ?f x = (if n=0 then 0 else ?g)")
 proof -
   have "(?f has_real_derivative ?g) (at x)" if "n > 0"
   proof -
     have "(\<Sum>i = 0..n. i * x ^ (i - Suc 0) * (c i))
         = (\<Sum>i = Suc 0..n. (real (i - Suc 0) + 1) * real_of_int (c i) * x ^ (i - Suc 0))"
       using that by (auto simp add: sum.atLeast_Suc_atMost intro!: sum.cong)
     also have "\<dots> = sum ((\<lambda>i. (real i + 1) * real_of_int (c (Suc i)) * x^i) \<circ> (\<lambda>n. n - Suc 0)) 
                      {Suc 0..Suc (n - Suc 0)}"
       using that by simp
     also have "\<dots> = ?g"
       by (simp flip: sum.atLeast_atMost_pred_shift [where m=0])
     finally have \<section>: "(\<Sum>a = 0..n. a * x ^ (a - Suc 0) * (c a)) = ?g" .
     show ?thesis
       by (rule derivative_eq_intros \<section> | simp)+
   qed
   then show ?thesis
     by (force intro: DERIV_imp_deriv)
 qed
 
 text \<open>We calculate the coefficients of the $k$th derivative precisely.\<close>
 lemma hf_deriv_int_poly:
   "(deriv^^k) (hf n) = (\<lambda>x. (1/fact n) * (\<Sum>i=0..2*n-k. of_int (int(\<Prod>{i<..i+k}) * cf n (i+k)) * x^i))"
 proof (induction k)
   case 0
   show ?case 
     by (simp add: hf_int_poly)
 next
   case (Suc k)
   define F where "F \<equiv> \<lambda>x. (\<Sum>i = 0..2*n - k. real_of_int (int(\<Prod>{i<..i+k}) * cf n (i+k)) * x^i)"
   have Fd: "F field_differentiable at x" for x
     unfolding field_differentiable_def F_def
     by (rule derivative_eq_intros exI | force)+
   have [simp]: "prod int {i<..Suc (i + k)} = (1 + int i) * prod int {Suc i<..Suc (i + k)}" for i
     by (metis Suc_le_mono atLeastSucAtMost_greaterThanAtMost le_add1 of_nat_Suc prod.head) 
   have "deriv (\<lambda>x. F x / fact n) x 
       = (\<Sum>i = 0..2 * n - Suc k. of_int (int(\<Prod>{i<..i+ Suc k}) * cf n (Suc (i+k))) * x^i) / fact n" for x
     unfolding deriv_cdivide_right [OF Fd]
     by (fastforce simp add: F_def deriv_sum_int cf_def simp flip: of_int_mult intro: sum.cong)
   then show ?case
     by (simp add: Suc F_def)
 qed
 
 lemma hf_deriv_0: "(deriv^^k) (hf n) 0 \<in> \<int>"
 proof (cases "n \<le> k")
   case True
   then obtain j where "(fact k::real) = real_of_int j * fact n"
     by (metis fact_dvd dvd_def mult.commute of_int_fact of_int_mult) 
   moreover have "prod real {0<..k} = fact k"
     by (simp add: fact_prod atLeastSucAtMost_greaterThanAtMost)
   ultimately show ?thesis
     by (simp add: hf_deriv_int_poly dvd_def)
 next
   case False
   then show ?thesis
     by (simp add: hf_deriv_int_poly cf_def)
 qed
 
 lemma deriv_hf_minus: "deriv (hf n) = (\<lambda>x. - deriv (hf n) (1-x))"
 proof 
   fix x
   have "hf n = hf n \<circ> (\<lambda>x. (1-x))"
     by (simp add: fun_eq_iff hf_def mult.commute)
   then have "deriv (hf n) x = deriv (hf n \<circ> (\<lambda>x. (1-x))) x"
     by fastforce
   also have "\<dots> = deriv (hf n) (1-x) * deriv ((-) 1) x"
     by (intro real_derivative_chain) auto
   finally show "deriv (hf n) x = - deriv (hf n) (1-x)"
     by simp
 qed
 
 lemma deriv_n_hf_diffr [iff]: "(deriv^^k) (hf n) field_differentiable at x"
   unfolding field_differentiable_def hf_deriv_int_poly
   by (rule derivative_eq_intros exI | force)+
 
 lemma deriv_n_hf_minus: "(deriv^^k) (hf n) = (\<lambda>x. (-1)^k * (deriv^^k) (hf n) (1-x))"
 proof (induction k)
   case 0
   then show ?case
     by (simp add: fun_eq_iff hf_def)
 next
   case (Suc k)
   have o: "(\<lambda>x. (deriv ^^ k) (hf n) (1-x)) = (deriv ^^ k) (hf n) \<circ> (-) 1"
     by auto
   show ?case
   proof
     fix x
     have [simp]: "((deriv^^k) (hf n) \<circ> (-) 1) field_differentiable at x"
       by (force intro: field_differentiable_compose)
     have "(deriv ^^ Suc k) (hf n) x = deriv (\<lambda>x. (-1) ^ k * (deriv ^^ k) (hf n) (1-x)) x"
       by simp (metis Suc)
     also have "\<dots> = (-1) ^ k * deriv (\<lambda>x. (deriv ^^ k) (hf n) (1-x)) x"
       using o by fastforce
     also have "\<dots> = (-1) ^ Suc k * (deriv ^^ Suc k) (hf n) (1-x)"
       by (subst o, subst deriv_chain, auto)
     finally show "(deriv ^^ Suc k) (hf n) x = (-1) ^ Suc k * (deriv ^^ Suc k) (hf n) (1-x)" .
   qed
 qed
 
 subsection \<open>Towards the main result\<close>
 
 lemma hf_deriv_1: "(deriv^^k) (hf n) 1 \<in> \<int>"
   by (smt (verit, best) Ints_1 Ints_minus Ints_mult Ints_power deriv_n_hf_minus hf_deriv_0)
 
 lemma hf_deriv_eq_0: "k > 2*n \<Longrightarrow> (deriv^^k) (hf n) = (\<lambda>x. 0)"
   by (force simp add: cf_def hf_deriv_int_poly)
 
 text \<open>The case for positive integers\<close>
 lemma exp_nat_irrational:
   assumes "s > 0" shows "exp (real_of_int s) \<notin> \<rat>"
 proof
   assume "exp (real_of_int s) \<in> \<rat>"
   then obtain a b where ab: "a > 0" "b > 0" "coprime a b" and exp_s: "exp s = of_int a / of_int b"
     using Rats_cases' div_0 exp_not_eq_zero of_int_0
     by (smt (verit, best) exp_gt_zero of_int_0_less_iff zero_less_divide_iff)
   define n where "n \<equiv> nat (max (a^2) (3 * s^3))"
   then have ns3: "s^3 \<le> real n / 3"
     by linarith
   have "n > 0"
     using \<open>a > 0\<close> n_def by (smt (verit, best) zero_less_nat_eq zero_less_power)
   then have "s ^ (2*n+1) \<le> s ^ (3*n)"
     using \<open>a > 0\<close> assms by (intro power_increasing) auto
   also have "\<dots> = real_of_int(s^3) ^ n"
     by (simp add: power_mult)
   also have "\<dots> \<le> (n / 3) ^ n"
     using assms ns3 by (simp add: power_mono)
   also have "\<dots> \<le> (n / exp 1) ^ n"
     using exp_le \<open>n > 0\<close>
     by (auto simp add: divide_simps)
   finally have s_le: "s ^ (2*n+1) \<le> (n / exp 1) ^ n"
     by presburger 
   have a_less: "a < sqrt (2*pi*n)"
   proof -
     have "2*pi > 1"
       by (smt (z3) pi_gt_zero sin_gt_zero_02 sin_le_zero)
     have "a = sqrt (a^2)"
       by (simp add: ab(1) order_less_imp_le)
     also have "\<dots> \<le> sqrt n"
       unfolding n_def
       by (smt (verit, ccfv_SIG) int_nat_eq of_nat_less_of_int_iff real_sqrt_le_mono)
     also have "\<dots> < sqrt (2*pi*n)"
       by (simp add: \<open>0 < n\<close> \<open>1 < 2 * pi\<close>)
     finally show ?thesis .
   qed
   have "sqrt (2*pi*n) * (n / exp 1) ^ n > a * s ^ (2*n+1)"
     using mult_strict_right_mono [OF a_less] mult_left_mono [OF s_le]
     by (smt (verit, best) s_le ab(1) assms of_int_1 of_int_le_iff of_int_mult zero_less_power)
   then have n: "fact n > a * s ^ (2*n+1)"
     using fact_bounds(1) by (smt (verit, best) \<open>0 < n\<close> of_int_fact of_int_less_iff)
   define F where "F \<equiv> \<lambda>x. \<Sum>i\<le>2*n. (-1)^i * s^(2*n-i) * (deriv^^i) (hf n) x"
   have Fder: "(F has_real_derivative -s * F x + s^(2*n+1) * hf n x) (at x)" for x
   proof -
     have *: "sum f {..n+n} = sum f {..<n+n}" if "f (n+n) = 0" for f::"nat \<Rightarrow> real"
       by (smt (verit, best) lessThan_Suc_atMost sum.lessThan_Suc that)
     have [simp]: "(deriv ((deriv ^^ (n+n)) (hf n)) x) = 0"
       using hf_deriv_eq_0 [where k= "Suc(n+n)"] by simp
     have \<section>: "(\<Sum>k\<le>n+n. (-1) ^ k * ((deriv ^^ Suc k) (hf n) x * of_int s ^ (n+n - k))) 
            + s * (\<Sum>j=0..n+n. (-1) ^ j * ((deriv ^^ j) (hf n) x * of_int s ^ (n+n - j))) 
            = s * (hf n x * of_int s ^ (n+n))" 
       using \<open>n>0\<close>
       apply (subst sum_Suc_reindex)
       apply (simp add: algebra_simps atLeast0AtMost)
       apply (force simp add: * mult.left_commute [of "of_int s"] minus_nat.diff_Suc sum_distrib_left 
               simp flip: sum.distrib intro: comm_monoid_add_class.sum.neutral split: nat.split_asm)
       done
     show ?thesis
       unfolding F_def 
       apply (rule derivative_eq_intros field_differentiable_derivI | simp)+
       using \<section> by (simp add: algebra_simps atLeast0AtMost eval_nat_numeral)
   qed
   have F01_Ints: "F 0 \<in> \<int>" "F 1 \<in> \<int>"
     by (simp_all add: F_def hf_deriv_0 hf_deriv_1 Ints_sum)
   define sF where "sF \<equiv> \<lambda>x. exp (of_int s * x) * F x"
   define sF' where "sF' \<equiv> \<lambda>x. of_int s ^ Suc(2*n) * (exp (of_int s * x) * hf n x)"
   have sF_der: "(sF has_real_derivative sF' x) (at x)" for x
     unfolding sF_def sF'_def
     by (rule refl Fder derivative_eq_intros | force simp: algebra_simps)+
   let ?N = "b * integral {0..1} sF'"
   have sF'_integral: "(sF' has_integral sF 1 - sF 0) {0..1}"
     by (smt (verit) fundamental_theorem_of_calculus has_field_derivative_iff_has_vector_derivative 
                     has_vector_derivative_at_within sF_der)
   then have "?N = a * F 1 - b * F 0"
     using \<open>b > 0\<close> by (simp add: integral_unique exp_s sF_def algebra_simps)
   also have "\<dots> \<in> \<int>"
     using hf_deriv_1 by (simp add: F01_Ints)
   finally have N_Ints: "?N \<in> \<int>" .
   have "sF' (1/2) > 0" and ge0: "\<And>x. x \<in> {0..1} \<Longrightarrow> 0 \<le> sF' x"
     using assms by (auto simp add: sF'_def hf_def)
   moreover have "continuous_on {0..1} sF'"
     unfolding sF'_def hf_def by (intro continuous_intros) auto
   ultimately have False if "(sF' has_integral 0) {0..1}"
     using has_integral_0_cbox_imp_0 [of 0 1 sF' "1/2"] that by auto
   then have "integral {0..1} sF' > 0"
     by (metis ge0 has_integral_nonneg integral_unique order_le_less sF'_integral) 
   then have "0 < ?N"
     by (simp add: \<open>b > 0\<close>)
   have "integral {0..1} sF' = of_int s ^ Suc(2*n) * integral {0..1} (\<lambda>x. exp (s*x) * hf n x)"
     unfolding sF'_def by force 
   also have "\<dots> \<le> of_int s ^ Suc(2*n) * (exp s * (1 / fact n))"
   proof (rule mult_left_mono)
     have "integral {0..1} (\<lambda>x. exp (s*x) * hf n x) \<le> integral {0..1} (\<lambda>x::real. exp s * (1/fact n))"
     proof (intro mult_mono integral_le)
       show "(\<lambda>x. exp (s*x) * hf n x) integrable_on {0..1}"
         using \<open>0 < ?N\<close> not_integrable_integral sF'_def by fastforce
     qed (use assms hf_nonneg hf_le_inverse_fact in auto)
     also have "\<dots> = exp s * (1 / fact n)"
       by simp
     finally show "integral {0..1} (\<lambda>x. exp (s*x) * hf n x) \<le> exp s * (1 / fact n)" .
   qed (use assms in auto)
   finally have "?N \<le> b * of_int s ^ Suc(2*n) * exp s * (1 / fact n)"
     using \<open>b > 0\<close> by (simp add: sF'_def mult_ac divide_simps)
   also have "\<dots> < 1"
     using n apply (simp add: field_simps exp_s)
     by (metis of_int_fact of_int_less_iff of_int_mult of_int_power)
   finally show False
     using \<open>0 < ?N\<close> Ints_cases N_Ints by force
 qed
 
 theorem exp_irrational:
   fixes q::real assumes "q \<in> \<rat>" "q \<noteq> 0" shows "exp q \<notin> \<rat>"
 proof 
   assume q: "exp q \<in> \<rat>"
   obtain s t where "s \<noteq> 0" "t > 0" "q = of_int s / of_int t"
     by (metis Rats_cases' assms div_0 of_int_0)
   then have "(exp q) ^ (nat t) = exp s"
     by (smt (verit, best) exp_divide_power_eq of_nat_nat zero_less_nat_eq)
   moreover have "exp q ^ (nat t) \<in> \<rat>"
     by (simp add: q)
   ultimately show False
     by (smt (verit, del_insts) Rats_inverse \<open>s \<noteq> 0\<close> exp_minus exp_nat_irrational of_int_of_nat)
 qed
 
 corollary ln_irrational: 
   fixes q::real assumes "q \<in> \<rat>" "q > 0"  "q \<noteq> 1" shows "ln q \<notin> \<rat>"
   using assms exp_irrational [of "ln q"] exp_ln_iff [of q] by force
 
 end
diff --git a/thys/Sunflowers/Erdos_Rado_Sunflower.thy b/thys/Sunflowers/Erdos_Rado_Sunflower.thy
--- a/thys/Sunflowers/Erdos_Rado_Sunflower.thy
+++ b/thys/Sunflowers/Erdos_Rado_Sunflower.thy
@@ -1,358 +1,358 @@
 (* author: R. Thiemann *)
 
 section \<open>The Sunflower Lemma\<close>
 
 text \<open>We formalize the proof of the sunflower lemma of Erd\H{o}s and Rado~\cite{erdos_rado}, 
 as it is presented in the textbook~\cite[Chapter~6]{book}.  
 We further integrate Exercise 6.2 from the textbook,
 which provides a lower bound on the existence of sunflowers.\<close>
 
 theory Erdos_Rado_Sunflower
   imports 
     Sunflower
 begin
 
 text \<open>When removing an element from all subsets, then one can afterwards
   add these elements to a sunflower and get a new sunflower.\<close>
 
 lemma sunflower_remove_element_lift: 
   assumes S: "S \<subseteq> { A - {a} | A . A \<in> F \<and> a \<in> A}" 
     and sf: "sunflower S" 
   shows "\<exists> Sa. sunflower Sa \<and> Sa \<subseteq> F \<and> card Sa = card S \<and> Sa = insert a ` S" 
 proof (intro exI[of _ "insert a ` S"] conjI refl)
   let ?Sa = "insert a ` S" 
   {
     fix B
     assume "B \<in> ?Sa" 
     then obtain C where C: "C \<in> S" and B: "B = insert a C" 
       by auto
     from C S obtain T where "T \<in> F" "a \<in> T" "C = T - {a}" 
       by auto
     with B have "B = T" by auto
     with \<open>T \<in> F\<close> have "B \<in> F" by auto
   } 
   thus SaF: "?Sa \<subseteq> F" by auto
   have inj: "inj_on (insert a) S" using S 
     by (intro inj_on_inverseI[of _ "\<lambda> B. B - {a}"], auto)
   thus "card ?Sa = card S" by (rule card_image)
   show "sunflower ?Sa" unfolding sunflower_def
   proof (intro allI, intro impI)
     fix x
     assume "\<exists>C D. C \<in> ?Sa \<and> D \<in> ?Sa \<and> C \<noteq> D \<and> x \<in> C \<and> x \<in> D"
     then obtain C D where *: "C \<in> ?Sa" "D \<in> ?Sa" "C \<noteq> D" "x \<in> C" "x \<in> D" 
       by auto
     from *(1-2) obtain C' D' where 
       **: "C' \<in> S" "D' \<in> S" "C = insert a C'" "D = insert a D'" 
       by auto
     with \<open>C \<noteq> D\<close> inj have CD': "C' \<noteq> D'" by auto
     show "\<forall>E. E \<in> ?Sa \<longrightarrow> x \<in> E" 
     proof (cases "x = a")
       case False
       with * ** have "x \<in> C'" "x \<in> D'" by auto
       with ** CD' have "\<exists>C D. C \<in> S \<and> D \<in> S \<and> C \<noteq> D \<and> x \<in> C \<and> x \<in> D" by auto
       from sf[unfolded sunflower_def, rule_format, OF this]
       show ?thesis by auto
     qed auto
   qed
 qed
 
 text \<open>The sunflower-lemma of Erd\H{o}s and Rado: 
   if a set has a certain size and all elements
   have the same cardinality, then a sunflower exists.\<close>
 
 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" 
   using assms 
 proof (induct k arbitrary: F)
   case 0
   hence "F = {{}} \<or> F = {}" "card F \<ge> 2" by auto
   hence False by auto
   thus ?case by simp
 next 
   case (Suc k F)
   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)"
   show ?case
   proof (cases "\<exists> t G. pd_sub G t \<and> t \<ge> r")
     case True
     then obtain t G where pd_sub: "pd_sub G t" and t: "t \<ge> r" by auto
     from pd_sub[unfolded pd_sub_def] pairwise_disjnt_imp_sunflower
     have *: "G \<subseteq> F" "card G = t" "sunflower G" "{} \<notin> G" by auto
     from t \<open>card G = t\<close> obtain H where "H \<subseteq> G" "card H = r"
       by (metis obtain_subset_with_card_n)
     with sunflower_subset[OF \<open>H \<subseteq> G\<close>] * show ?thesis by blast
   next
     case False
     define P where "P = (\<lambda> t. \<exists> G. pd_sub G t)" 
     have ex: "\<exists> t. P t" unfolding P_def
       by (intro exI[of _ 0] exI[of _ "{}"], auto simp: pd_sub_def)
     have large': "\<And> t. P t \<Longrightarrow> t < r" using False unfolding P_def by auto
     hence large: "\<And> t. P t \<Longrightarrow> t \<le> r" by fastforce 
     define t where "t = (GREATEST t. P t)"
     from GreatestI_ex_nat[OF ex large, folded t_def] have Pt: "P t" .
     from Greatest_le_nat[of P, OF _ large] 
     have greatest: "\<And> s. P s \<Longrightarrow> s \<le> t" unfolding t_def by auto
     from large'[OF Pt] have tr: "t \<le> r - 1" by simp
     from Pt[unfolded P_def pd_sub_def] obtain G where 
       cardG: "card G = t" and 
       disj: "pairwise disjnt G" and 
       GF: "G \<subseteq> F" 
       by blast
     define A where "A = (\<Union> G)"
     from Suc(3) have "card F > 0" by simp
     hence "finite F" by (rule card_ge_0_finite)
     from GF \<open>finite F\<close> have finG: "finite G" by (rule finite_subset)
-    have "card (\<Union> G) \<le> sum card G" 
-      by (rule card_Union_le_sum_card, insert Suc(2) GF, auto)
-    also have "\<dots> \<le> of_nat (card G) * Suc k" 
-      by (rule sum_bounded_above, insert GF Suc(2), auto)
+    have "card (\<Union> G) \<le> sum card G"
+      using card_Union_le_sum_card by blast 
+    also have "\<dots> \<le> of_nat (card G) * Suc k"
+      by (metis GF Suc.prems(1) le_Suc_eq subsetD sum_bounded_above) 
     also have "\<dots> \<le> (r - 1) * Suc k" 
       using tr[folded cardG] by (metis id_apply mult_le_mono1 of_nat_eq_id)
     finally have cardA: "card A \<le> (r - 1) * Suc k" unfolding A_def .
     {
       fix B
       assume *: "B \<in> F"
       with Suc(2) have nE: "B \<noteq> {}" by auto
       from Suc(2) have eF: "{} \<notin> F" by auto
       have "B \<inter> A \<noteq> {}"
       proof
         assume dis: "B \<inter> A = {}"
         hence disj: "pairwise disjnt ({B} \<union> G)"  using disj unfolding A_def
           by (smt (verit, ccfv_SIG) Int_commute Un_iff 
               Union_disjoint disjnt_def pairwise_def singleton_iff)
         from nE dis have "B \<notin> G" unfolding A_def by auto
         with finG have c: "card ({B} \<union> G) = Suc t" by (simp add: cardG)
         have "P (Suc t)" unfolding P_def pd_sub_def
           by (intro exI[of _ "{B} \<union> G"], insert eF disj c * GF, auto)
         with greatest show False by force
       qed
     } note overlap = this
     have "F \<noteq> {}" using Suc(2-) by auto
     with overlap have Ane: "A \<noteq> {}" unfolding A_def by auto
     have "finite A" unfolding A_def using finG Suc(2-) GF by auto
     let ?g = "\<lambda> B x. x \<in> B \<inter> A" 
     define f where "f = (\<lambda> B. SOME x. ?g B x)" 
     have "f \<in> F \<rightarrow> A"
     proof
       fix B
       assume "B \<in> F" 
       from overlap[OF this] have "\<exists> x. ?g B x" unfolding A_def by auto
       from someI_ex[OF this] show "f B \<in> A" unfolding f_def by auto
     qed
     from pigeonhole_card[OF this \<open>finite F\<close> \<open>finite A\<close> Ane]
     obtain a where a: "a \<in> A" 
       and le: "card F \<le> card (f -` {a} \<inter> F) * card A" by auto
     {
       fix S 
       assume "S \<in> F" "f S \<in> {a}"
       with someI_ex[of "?g S"] a overlap[OF this(1)]
       have "a \<in> S" unfolding f_def by auto
     } note FaS = this
     let ?F = "{S - {a} | S . S \<in> F \<and> f S \<in> {a}}" 
     from cardA have "((r - 1) ^ k * fact k) * card A \<le> ((r - 1) ^ k * fact k) * ((r - 1) * Suc k)"
       by simp
     also have "\<dots> = (r - 1) ^ (Suc k) * fact (Suc k)"
       by (metis (no_types, lifting) fact_Suc mult.assoc mult.commute of_nat_id power_Suc2)
     also have "\<dots> < card (f -` {a} \<inter> F) * card A" 
       using Suc(3) le by auto
     also have "f -` {a} \<inter> F = {S \<in> F. f S \<in> {a}}" by auto
     also have "card \<dots> = card ((\<lambda> S. S - {a}) ` {S \<in> F. f S \<in> {a}})" 
       by (subst card_image; intro inj_onI refl, insert FaS) auto
     also have "(\<lambda> S. S - {a}) ` {S \<in> F. f S \<in> {a}} = ?F" by auto
     finally have lt: "(r - 1) ^ k * fact k < card ?F" by simp
     have "\<forall> A \<in> ?F. finite A \<and> card A = k" using Suc(2) FaS by auto
     from Suc(1)[OF this lt] obtain S
       where "sunflower S" "card S = r" "S \<subseteq> ?F" by auto
     from \<open>S \<subseteq> ?F\<close> FaS have "S \<subseteq> {A - {a} |A. A \<in> F \<and> a \<in> A}" by auto
     from sunflower_remove_element_lift[OF this \<open>sunflower S\<close>] \<open>card S = r\<close>
     show ?thesis by auto
   qed
 qed
 
 text \<open>Using @{thm [source] sunflower_card_subset_lift} we can easily 
   replace the condition that the cardinality is exactly @{term k}
   by the requirement that the cardinality is at most @{term k}. 
   However, then @{term "{} \<notin> S"} cannot be ensured.
   Consider @{term "(r :: nat) = 1 \<and> (k :: nat) > 0 \<and> F = {{}}"}.\<close>
 
 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" 
   by (rule sunflower_card_subset_lift[OF _ assms], 
       metis Erdos_Rado_sunflower_same_card)
 
 text \<open>We further provide a lower bound on the existence of sunflowers, 
 i.e., Exercise 6.2 of the textbook~\cite{book}.
 To be more precise, we prove that there is a set of sets of cardinality 
 @{term \<open>(r - 1 :: nat)^k\<close>}, where each element is a set of cardinality 
 @{term k}, such that there is no subset which is a sunflower with cardinality
 of at least @{term r}.\<close>
 
 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 (cases "r = 1")
   case False
   with r have r: "r > 1" by auto
   show ?thesis
   proof (induct k)
     case 0
     have id: "S \<subseteq> {{}} \<longleftrightarrow> (S = {} \<or> S = {{}})" for S :: "'a set set" by auto 
     show ?case using r
       by (intro exI[of _ "{{}}"], auto simp: id)
   next
     case (Suc k)
     then 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)" 
       by metis
     text \<open>main idea: get @{term "k-1 :: nat"} fresh elements 
       and add one of these to all elements of F\<close>
     have "finite (\<Union> F)" using fin AF by simp
     hence "infinite (UNIV - \<Union> F)" using inf by simp
     from infinite_arbitrarily_large[OF this, of "r - 1"]
     obtain New where New: "finite New" "card New = r - 1" 
       "New \<inter> \<Union> F = {}" by auto
     define G where "G = (\<lambda> (A, a). insert a A) ` (F \<times> New)" 
     show ?case
     proof (intro exI[of _ G] conjI)
       show "finite G" using New fin unfolding G_def by simp
       have "card G = card (F \<times> New)" unfolding G_def
       proof ((subst card_image; (intro refl)?), intro inj_onI, clarsimp, goal_cases)
         case (1 A a B b)
         hence ab: "a = b" using New by auto
         from 1(1) have "insert a A - {a} = insert b B - {a}" by simp
         also have "insert a A - {a} = A" using New 1 by auto
         also have "insert b B - {a} = B" using New 1 ab[symmetric] by auto
         finally show ?case using ab by auto
       qed
       also have "\<dots> = card F * card New" using New fin by auto
       finally show "card G = (r - 1) ^ Suc k" 
         unfolding cardF New by simp
       {
         fix B
         assume "B \<in> G" 
         then obtain a A where G: "a \<in> New" "A \<in> F" "B = insert a A" 
           unfolding G_def by auto
         with AF[of A] New have "finite B" "card B = Suc k" 
           by (auto simp: card_insert_if)
       }
       thus "\<forall>A\<in>G. finite A \<and> card A = Suc k" by auto
       show "\<not> (\<exists>S\<subseteq>G. sunflower S \<and> r \<le> card S)" 
       proof (intro notI, elim exE conjE)
         fix S
         assume *: "S \<subseteq> G" "sunflower S" "r \<le> card S"
         define g where "g B = (SOME a. a \<in> New \<and> a \<in> B)" for B
         {
           fix B
           assume "B \<in> S" 
           with \<open>S \<subseteq> G\<close> have "B \<in> G" by auto
           hence "\<exists> a. a \<in> New \<and> a \<in> B" unfolding G_def by auto
           from someI_ex[OF this, folded g_def]
           have "g B \<in> New" "g B \<in> B" by auto
         } note gB = this
         have "card (g ` S) \<le> card New" 
           by (rule card_mono, insert New gB, auto)
         also have "\<dots> < r" unfolding New using r by simp
         also have "\<dots> \<le> card S" by fact
         finally have "card (g ` S) < card S" .
         from pigeonhole[OF this] have "\<not> inj_on g S" .
         then obtain B1 B2 where B12: "B1 \<in> S" "B2 \<in> S" "B1 \<noteq> B2" "g B1 = g B2" 
           unfolding inj_on_def by auto
         define a where "a = g B2" 
         from B12 gB[of B1] gB[of B2] have a: "a \<in> New" "a \<in> B1" "a \<in> B2"
           unfolding a_def by auto  
         with B12 have "\<exists>B1 B2. B1 \<in> S \<and> B2 \<in> S \<and> B1 \<noteq> B2 \<and> a \<in> B1 \<and> a \<in> B2" 
           unfolding a_def by blast
         from \<open>sunflower S\<close>[unfolded sunflower_def, rule_format, OF this]
         have aS: "B \<in> S \<Longrightarrow> a \<in> B" for B by auto
         define h where "h B = B - {a}" for B
         define T where "T = h ` S" 
         have "\<exists>S\<subseteq>F. sunflower S \<and> r \<le> card S" 
         proof (intro exI[of _ T] conjI)
           {
             fix B
             assume "B \<in> S" 
             have hB: "h B = B - {a}" 
               unfolding h_def T_def by auto
             from aS \<open>B \<in> S\<close> have aB: "a \<in> B" by auto
             from \<open>B \<in> S\<close> \<open>S \<subseteq> G\<close> obtain a' A where AF: "A \<in> F" 
               and B: "B = insert a' A" 
               and a': "a' \<in> New" unfolding G_def by force
             from aB B a' New AF a(1) hB AF have "insert a (h B) = B" "h B = A" by auto
             hence "insert a (h B) = B" "h B \<in> F" "insert a (h B) \<in> S" using AF \<open>B \<in> S\<close> by auto
           } note main = this
           have CTS: "C \<in> T \<Longrightarrow> insert a C \<in> S" for C using main unfolding T_def by force
           show "T \<subseteq> F" unfolding T_def using main by auto
           have "r \<le> card S" by fact
           also have "\<dots> = card T" unfolding T_def
             by (subst card_image, intro inj_on_inverseI[of _ "insert a"], insert main, auto)
           finally show "r \<le> card T" .
           show "sunflower T" unfolding sunflower_def
           proof (intro allI impI, elim exE conjE, goal_cases)
             case (1 x C C1 C2)
             from CTS[OF \<open>C1 \<in> T\<close>] CTS[OF \<open>C2 \<in> T\<close>] CTS[OF \<open>C \<in> T\<close>]
             have *: "insert a C1 \<in> S" "insert a C2 \<in> S" "insert a C \<in> S" by auto          
             from 1 have "insert a C1 \<noteq> insert a C2" using main
               unfolding T_def by auto
             hence "\<exists>A B. A \<in> S \<and> B \<in> S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B" 
               using * 1 by auto          
             from \<open>sunflower S\<close>[unfolded sunflower_def, rule_format, OF this *(3)]
             have "x \<in> insert a C" .
             with 1 show "x \<in> C" unfolding T_def h_def by auto
           qed
         qed
         with sf
         show False ..
       qed
     qed
   qed
 next
   case r: True
   with rk have "k \<noteq> 0" by auto
   then obtain l where k: "k = Suc l" by (cases k, auto)
   show ?thesis unfolding r k
     by (intro exI[of _ "{}"], auto)
 qed
 
 text \<open>The difference between the lower and the
 upper bound on the existence of sunflowers as they have been formalized
 is @{term \<open>fact k\<close>}. There is more recent work with tighter bounds
 \cite{sunflower_new}, but we only integrate the initial 
 result of Erd\H{o}s and Rado in this theory.\<close>
 
 text \<open>We further provide the Erd\H{o}s Rado lemma 
   lifted to obtain non-empty cores or cores of arbitrary cardinality.\<close>
 
 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" 
   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)
 
 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> {}" 
   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)
 
 end