diff --git a/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy b/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy
--- a/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy
+++ b/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy
@@ -1,1668 +1,1643 @@
 section\<open>Roth's Theorem on Arithmetic Progressions\<close>
 
 theory Roth_Arithmetic_Progressions
   imports Szemeredi_Regularity.Szemeredi
       "Random_Graph_Subgraph_Threshold.Subgraph_Threshold"
       "Ergodic_Theory.Asymptotic_Density"
       "HOL-Library.Ramsey" "HOL-Library.Nat_Bijection"
 
 begin
 
 subsection \<open>Miscellaneous Preliminaries\<close>
 
 lemma sum_prod_le_prod_sum:
   fixes a :: "'a \<Rightarrow> 'b::linordered_idom"
   assumes "\<And>i. i \<in> I \<Longrightarrow> a i \<ge> 0 \<and> b i \<ge> 0"
   shows "(\<Sum>i\<in>I. \<Sum>j\<in>I. a i * b j) \<le> (\<Sum>i\<in>I. a i) * (\<Sum>i\<in>I. b i)"
   using assms
   by (induction I rule: infinite_finite_induct) (auto simp add: algebra_simps sum.distrib sum_distrib_left)
 
 lemma real_mult_gt_cube: "A \<ge> (X ::real) \<Longrightarrow> B \<ge> X \<Longrightarrow> C \<ge> X \<Longrightarrow> X \<ge> 0 \<Longrightarrow> A * B * C \<ge> X^3"
   by (simp add: mult_mono' power3_eq_cube)
 
 lemma triple_sigma_rewrite_card: 
   assumes "finite X" "finite Y" "finite Z"
   shows "card {(x, y, z) . x \<in> X \<and> (y, z) \<in> Y \<times> Z \<and> P x y z} = (\<Sum>x\<in> X . card {(y,z) \<in> Y \<times> Z. P x y z})"
 proof -
   define W where "W \<equiv> \<lambda>x. {(y,z) \<in> Y \<times> Z. P x y z}"
   have "W x \<subseteq> Y \<times> Z" for x
     by (auto simp: W_def)
   then have [simp]: "finite (W x)" for x
     by (meson assms finite_SigmaI infinite_super)
   have eq: "{(x, y, z) . x \<in> X \<and> (y, z) \<in> Y \<times> Z \<and> P x y z} = (\<Union>x\<in>X. \<Union>(y, z)\<in>W x. {(x,y,z)})"
     by (auto simp: W_def)
   show ?thesis
     unfolding eq by (simp add: disjoint_iff assms card_UN_disjoint) (simp add: W_def)
 qed
 
 lemma all_edges_between_mono1:
   "Y \<subseteq> Z \<Longrightarrow> all_edges_between Y X G \<subseteq> all_edges_between Z X G"
   by (auto simp: all_edges_between_def)
 
 lemma all_edges_between_mono2:
   "Y \<subseteq> Z \<Longrightarrow> all_edges_between X Y G \<subseteq> all_edges_between X Z G"
   by (auto simp: all_edges_between_def)
 
 lemma uwellformed_alt_fst: 
   assumes "uwellformed G" "{x, y} \<in> uedges G"
   shows "x \<in> uverts G"
   using uwellformed_def assms by simp
 
 lemma uwellformed_alt_snd: 
   assumes "uwellformed G" "{x, y} \<in> uedges G"
   shows "y \<in> uverts G"
   using uwellformed_def assms by simp
 
 lemma all_edges_between_subset_times: "all_edges_between X Y G \<subseteq> (X \<inter> \<Union>(uedges G)) \<times> (Y \<inter> \<Union>(uedges G))"
   by (auto simp: all_edges_between_def)
 
 lemma finite_all_edges_between':
   assumes "finite (uverts G)" "uwellformed G"
   shows "finite (all_edges_between X Y G)"
 proof -
   have "finite (\<Union>(uedges G))"
     by (meson Pow_iff all_edges_subset_Pow assms finite_Sup subsetD wellformed_all_edges)
   with all_edges_between_subset_times show ?thesis
     by (metis finite_Int finite_SigmaI finite_subset)
 qed
 
 lemma max_edges_graph: 
   assumes "uwellformed G" "finite (uverts G)"
   shows "card (uedges G) \<le> (card (uverts G))^2"
 proof -
   have "card (uedges G) \<le> card (uverts G) choose 2" 
     by (metis all_edges_finite assms card_all_edges card_mono wellformed_all_edges)
   thus ?thesis
     by (metis binomial_le_pow le0 neq0_conv order.trans zero_less_binomial_iff) 
 qed
 
 lemma all_edges_between_ss_uedges:  "mk_uedge ` (all_edges_between X Y G) \<subseteq> uedges G" 
   by (auto simp: all_edges_between_def)
 
 lemma all_edges_betw_D3: "(x, y) \<in> all_edges_between X Y G \<Longrightarrow> {x, y} \<in> uedges G"
   by (simp add: all_edges_between_def)
 
 lemma all_edges_betw_I: "x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> {x, y} \<in> uedges G \<Longrightarrow> (x, y) \<in> all_edges_between X Y G"
   by (simp add: all_edges_between_def)
 
 lemma all_edges_between_E_diff: 
   "all_edges_between X Y (V,E-E') = all_edges_between X Y (V,E) - all_edges_between X Y (V,E')"
   by (auto simp: all_edges_between_def)
 
 lemma all_edges_between_E_Un: 
   "all_edges_between X Y (V,E\<union>E') = all_edges_between X Y (V,E) \<union> all_edges_between X Y (V,E')"
   by (auto simp: all_edges_between_def)
 
 lemma all_edges_between_E_UN:
   "all_edges_between X Y (V, \<Union>i\<in>I. E i) = (\<Union>i\<in>I. all_edges_between X Y (V,E i))"
   by (auto simp: all_edges_between_def)
 
 lemma all_edges_preserved: "\<lbrakk>all_edges_between A B G' = all_edges_between A B G; X \<subseteq> A; Y \<subseteq> B\<rbrakk>
     \<Longrightarrow> all_edges_between X Y G' = all_edges_between X Y G"
   by (auto simp: all_edges_between_def)
 
 lemma subgraph_edge_wf:
   assumes "uwellformed G" "uverts H = uverts G" "uedges H \<subseteq> uedges G"
   shows "uwellformed H"
   by (metis assms subsetD uwellformed_def)
 
 
 subsection \<open>Preliminaries on Neighbors in Graphs\<close>
 
 definition neighbor_in_graph::  " uvert \<Rightarrow> uvert \<Rightarrow> ugraph \<Rightarrow>  bool"
   where "neighbor_in_graph x y G \<equiv> (x \<in> (uverts G) \<and> y \<in> (uverts G) \<and> {x,y} \<in> (uedges G))"
 
 definition neighbors :: "uvert \<Rightarrow> ugraph \<Rightarrow> uvert set" where
   "neighbors x G  \<equiv> {y \<in> uverts G . neighbor_in_graph x y G}"
 
 definition neighbors_ss:: "uvert \<Rightarrow> uvert set \<Rightarrow> ugraph \<Rightarrow> uvert set" where
   "neighbors_ss x Y G \<equiv> {y \<in> Y . neighbor_in_graph x y G}"
 
 lemma all_edges_betw_sigma_neighbor: 
 "uwellformed G \<Longrightarrow> all_edges_between X Y G = (SIGMA x:X. neighbors_ss x Y G)"
   by (auto simp add: all_edges_between_def neighbors_ss_def neighbor_in_graph_def 
       uwellformed_alt_fst uwellformed_alt_snd)
 
 lemma card_all_edges_betw_neighbor: 
   assumes "finite X" "finite Y" "uwellformed G"
   shows "card (all_edges_between X Y G) = (\<Sum>x\<in>X. card (neighbors_ss x Y G))"
   using all_edges_betw_sigma_neighbor assms by (simp add: neighbors_ss_def)
 
 
 subsection \<open>Preliminaries on Triangles in Graphs\<close>
 
 definition triangle_in_graph:: "uvert \<Rightarrow> uvert \<Rightarrow> uvert \<Rightarrow> ugraph \<Rightarrow> bool"
   where "triangle_in_graph x y z G 
          \<equiv> ({x,y} \<in> uedges G) \<and> ({y,z} \<in> uedges G) \<and> ({x,z} \<in> uedges G)"
 
 definition triangle_triples
   where "triangle_triples X Y Z G \<equiv> {(x,y,z) \<in> X \<times> Y \<times> Z. triangle_in_graph x y z G}"
 
 lemma triangle_commu1:
   assumes "triangle_in_graph x y z G"
   shows "triangle_in_graph y x z G"
   using assms triangle_in_graph_def by (auto simp add: insert_commute)
 
 lemma triangle_vertices_distinct1:
   assumes wf: "uwellformed G"
   assumes tri: "triangle_in_graph x y z G"
   shows "x \<noteq> y"
 proof (rule ccontr)
   assume a: "\<not> x \<noteq> y"
   have "card {x, y} = 2" using tri wf triangle_in_graph_def
     using uwellformed_def by blast 
   thus False using a by simp
 qed
 
 lemma triangle_vertices_distinct2: 
   assumes "uwellformed G" "triangle_in_graph x y z G"
   shows "y \<noteq> z"
   by (metis assms triangle_vertices_distinct1 triangle_in_graph_def) 
 
 lemma triangle_in_graph_edge_point: 
   assumes "uwellformed G"
   shows "triangle_in_graph x y z G \<longleftrightarrow> {y, z} \<in> uedges G \<and> neighbor_in_graph x y G \<and> neighbor_in_graph x z G"
   by (auto simp add: triangle_in_graph_def neighbor_in_graph_def assms uwellformed_alt_fst uwellformed_alt_snd)
 
 definition 
   "unique_triangles G 
     \<equiv> \<forall>e \<in> uedges G. \<exists>!T. \<exists>x y z. T = {x,y,z} \<and> triangle_in_graph x y z G \<and> e \<subseteq> T"
 
 definition triangle_free_graph:: "ugraph \<Rightarrow> bool"
   where "triangle_free_graph G \<equiv> \<not>(\<exists> x y z. triangle_in_graph x y z G )"
 
 lemma triangle_free_graph_empty: "uedges G = {} \<Longrightarrow> triangle_free_graph G"
   by (simp add: triangle_free_graph_def triangle_in_graph_def)
 
 lemma edge_vertices_not_equal: 
   assumes "uwellformed G" "{x,y} \<in> uedges G"
   shows "x \<noteq> y"
   using assms triangle_in_graph_def triangle_vertices_distinct1 by blast
 
 lemma triangle_in_graph_verts: 
   assumes "uwellformed G" "triangle_in_graph x y z G"
   shows "x \<in> uverts G" "y \<in> uverts G" "z\<in> uverts G"
 proof -
   have 1: "{x, y} \<in> uedges G" using triangle_in_graph_def
     using assms(2) by auto 
   then show "x \<in> uverts G" using uwellformed_alt_fst assms by blast
   then show "y \<in> uverts G" using 1 uwellformed_alt_snd assms by blast
   have "{x, z} \<in> uedges G" using triangle_in_graph_def assms(2) by auto
   then show "z \<in> uverts G" using uwellformed_alt_snd assms by blast
 qed
 
   
 definition triangle_set :: "ugraph \<Rightarrow> uvert set set"
   where "triangle_set G \<equiv> { {x,y,z} | x y z. triangle_in_graph x y z G}"
 
 fun mk_triangle_set :: "(uvert \<times> uvert \<times> uvert) \<Rightarrow> uvert set" 
   where "mk_triangle_set (x, y, z) = {x,y,z}"
 
 lemma finite_triangle_set:
   assumes fin: "finite (uverts G)" and wf: "uwellformed G"
   shows "finite (triangle_set G)"
 proof -
   have "triangle_set G \<subseteq> Pow (uverts G)"
   using insert_iff local.wf triangle_in_graph_def triangle_set_def uwellformed_def by auto
   then show ?thesis
     by (meson fin finite_Pow_iff infinite_super)
 qed
 
 lemma card_triangle_3: 
   assumes "t \<in> triangle_set G" "uwellformed G"
   shows "card t = 3"
   using assms by (auto simp: triangle_set_def edge_vertices_not_equal triangle_in_graph_def)
 
 lemma triangle_set_power_set_ss: "uwellformed G \<Longrightarrow> triangle_set G \<subseteq> Pow (uverts G)"
   by (auto simp add: triangle_set_def triangle_in_graph_def uwellformed_alt_fst  uwellformed_alt_snd)
 
 lemma triangle_in_graph_ss: 
   fixes G :: "ugraph" and Gnew :: "ugraph"
   assumes "uedges Gnew \<subseteq> uedges G" 
   assumes "triangle_in_graph x y z Gnew"
   shows "triangle_in_graph x y z G"
 proof -
   have "{x, y} \<in> uedges G" using assms triangle_in_graph_def by auto 
   have "{y, z} \<in> uedges G" using assms triangle_in_graph_def by auto 
   have "{x, z} \<in> uedges G" using assms triangle_in_graph_def by auto 
   thus ?thesis
     by (simp add: \<open>{x, y} \<in> uedges G\<close> \<open>{y, z} \<in> uedges G\<close> triangle_in_graph_def) 
 qed
 
 lemma triangle_set_graph_edge_ss: 
   fixes G :: "ugraph" and Gnew :: "ugraph"
   assumes "uwellformed G"
   assumes "uedges Gnew \<subseteq> uedges G" 
   assumes "uverts Gnew = uverts G"
   shows "(triangle_set Gnew) \<subseteq> (triangle_set G)"
 proof (intro subsetI)
   fix t assume "t \<in> triangle_set Gnew" 
   then obtain x y z where "t = {x,y,z}" and "triangle_in_graph x y z Gnew"
     using triangle_set_def assms mem_Collect_eq by auto
   then have "triangle_in_graph x y z G" using assms triangle_in_graph_ss by simp
   thus "t \<in> triangle_set G" using triangle_set_def assms
     using \<open>t = {x,y,z}\<close> by auto 
 qed
 
 lemma triangle_set_graph_edge_ss_bound: 
   fixes G :: "ugraph" and Gnew :: "ugraph"
   assumes "uwellformed G" "finite (uverts G)" "uedges Gnew \<subseteq> uedges G" "uverts Gnew = uverts G"
   shows "card (triangle_set G) \<ge> card (triangle_set Gnew)"
   by (simp add: assms card_mono finite_triangle_set triangle_set_graph_edge_ss)
 
 
 subsection \<open>The Triangle Counting Lemma and the Triangle Removal Lemma\<close>
 
 text\<open>We begin with some more auxiliary material to be used in the main lemmas.\<close>
 
-lemma regular_pairI:
-  fixes \<epsilon> :: real and G :: "ugraph" and X :: "uvert set" and Y ::"uvert set"
-  assumes "\<epsilon> > 0" and "regular_pair X Y G \<epsilon>" and xss: "X' \<subseteq> X" and yss: "Y' \<subseteq> Y" and "card X' \<ge> \<epsilon> * card X" and "(card Y' \<ge> \<epsilon> * card Y)"
-  shows "\<bar> edge_density X' Y' G - edge_density X Y G \<bar> \<le> \<epsilon>"
-  using regular_pair_def assms by meson 
-
 lemma regular_pair_neighbor_bound: 
   fixes \<epsilon>::real
   assumes finG: "finite (uverts G)"
   assumes xss: "X \<subseteq> uverts G" and yss: "Y \<subseteq> uverts G" and "card X > 0"
     and wf: "uwellformed G"
     and eg0: "\<epsilon> > 0" and "regular_pair X Y G \<epsilon>" and ed: "edge_density X Y G \<ge> 2*\<epsilon>"
-  shows "card{x \<in> X. card (neighbors_ss x Y G) < (edge_density X Y G - \<epsilon>)* card (Y)} < \<epsilon> * card X" 
-           (is "card (?X') < \<epsilon> * _")
+  defines "X' \<equiv> {x \<in> X. card (neighbors_ss x Y G) < (edge_density X Y G - \<epsilon>) * card (Y)}"
+  shows "card X' < \<epsilon> * card X" 
+    (is "card (?X') < \<epsilon> * _")
 proof (cases "?X' = {}")
   case True
   then show ?thesis
     by (simp add: True \<open>card X > 0\<close> eg0)
- next
+next
   case False
+  let ?rxy = "1/(card X' * card Y)" 
   show ?thesis 
-    proof (rule ccontr)
-      assume "\<not> (card (?X') <  \<epsilon> * card X) " 
-      then have a: "(card(?X') \<ge>  \<epsilon> * card X) " by simp
-      have fin: "finite X" "finite Y" using assms finite_subset by auto
-      have ebound: "\<epsilon> \<le> 1/2"
-        by (metis ed edge_density_le1 le_divide_eq_numeral1(1) mult.commute order_trans)
-      have finx: "finite ?X'" using fin by simp 
-      have "\<And> x. x \<in> ?X'\<Longrightarrow> (card (neighbors_ss x Y G)) < (edge_density X Y G - \<epsilon>) * (card Y)"
-        by blast 
-      then have "(\<Sum>x\<in>?X'. card (neighbors_ss x Y G)) < (\<Sum>x\<in>?X'. ((edge_density X Y G - \<epsilon>)* (card Y)))"
-        using False sum_strict_mono
-        by (smt (verit, del_insts) finx of_nat_sum)
-      then have upper: "(\<Sum>x\<in>?X'. card (neighbors_ss x Y G)) < (card ?X')* ((edge_density X Y G - \<epsilon>)* (card Y))"
-        by (simp add: sum_bounded_above)
-      have sumge0: "(\<Sum>x\<in>?X'. card (neighbors_ss x Y G)) \<ge> 0"
-        by blast 
-      have xge0: "card X > 0"
-        using fin(1) False by fastforce
-      have yge0: "card Y > 0"
-        using False by fastforce
-      then have xyge0: "card X * card Y > 0" using xge0 by simp
-      then have xyne0: "card X * card Y \<noteq> 0" by simp
-      have fracg0:"(1/(card ?X' * card Y)) > 0"
-        using card_0_eq finx False yge0 by fastforce 
-      then have upper2: "(1/(card ?X' * card Y)) * (\<Sum>x\<in>?X'. card (neighbors_ss x Y G)) < (1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \<epsilon>)* (card Y))"
-        using upper mult_less_cancel_left_pos[of "(1/(card ?X' * card Y))" "(\<Sum>x\<in>?X'. card (neighbors_ss x Y G))" "(card ?X')* ((edge_density X Y G - \<epsilon>)* (card Y))"]
-        by linarith 
-      have minuse: "(1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \<epsilon>)* (card Y)) = (edge_density X Y G - \<epsilon>)"
-      proof - 
-        have "(1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \<epsilon>)* (card Y)) = (1/(card ?X' * card Y)) * ((card ?X')* (card Y))*(edge_density X Y G - \<epsilon>)"
-          by (smt (z3) divide_divide_eq_right of_nat_mult times_divide_eq_left)
-        also have "\<dots> = ((card ?X'* card Y)/(card ?X' * card Y)) * (edge_density X Y G - \<epsilon>)" by simp
-        also have "\<dots> = 1 * (edge_density X Y G - \<epsilon>)"
-          using divide_eq_1_iff[of "(card ?X'* card Y)" "(card ?X'* card Y)"] xyne0
-          using finx False by force 
-        finally have "(1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \<epsilon>)* (card Y)) = (edge_density X Y G - \<epsilon>)" by simp
-        thus ?thesis by simp
-      qed
-      then have edlt1: "(1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \<epsilon>)* (card Y)) < edge_density X Y G" 
-        using eg0
-        by linarith
-      then have edlt2: "(1/(card ?X' * card Y))* (\<Sum>x\<in>?X'. card (neighbors_ss x Y G)) < edge_density X Y G" 
-        using upper2 by linarith 
-      then have "\<bar>edge_density X Y G - (1/(card ?X' * card Y))* (\<Sum>x\<in>?X'. card (neighbors_ss x Y G))\<bar> = edge_density X Y G - (1/(card ?X' * card Y))* (\<Sum>x\<in>?X'. card (neighbors_ss x Y G))"
-        by linarith 
-      have "(edge_density X Y G - (1/(card ?X' * card Y))* (\<Sum>x\<in>?X'. card (neighbors_ss x Y G))) > (edge_density X Y G - (1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \<epsilon>)* (card Y)))"
-        using edlt1 edlt2 upper2
-        by linarith  
-      then have "edge_density X Y G - (1/(card ?X' * card Y)) * (\<Sum>x\<in>?X'. card (neighbors_ss x Y G))  >  edge_density X Y G - (edge_density X Y G - \<epsilon>)"
-        using minuse by linarith
-      then have con: "edge_density X Y G - (1/(card ?X' * card Y)) * (\<Sum>x\<in>?X'. card (neighbors_ss x Y G)) > \<epsilon>" by simp
-      have ye: "card Y \<ge> \<epsilon> * (card Y)" using ebound by (simp add: yge0)
-      have xe': "card ?X' \<ge> \<epsilon> * (card X)" using a by fastforce
-      have "?X' \<subseteq> X" by simp
-      then have "\<bar> edge_density ?X' Y G - edge_density X Y G \<bar> \<le> \<epsilon>"
-        using regular_pairI[of "\<epsilon>" "X" "Y" "G" "?X'" "Y"] assms ye xe' by simp
-      then have "\<bar> (card (all_edges_between ?X' Y G))/ (card ?X' * card Y) - edge_density X Y G \<bar> \<le> \<epsilon>"
-        by (simp add: edge_density_def)
-      then have "\<bar> (1/(card ?X' * card Y)) * (card (all_edges_between ?X' Y G)) - edge_density X Y G \<bar> \<le> \<epsilon>"
-        by simp
-      then have "\<bar>(1/(card ?X' * card Y)) * (\<Sum>x\<in>?X'. card (neighbors_ss x Y G)) - edge_density X Y G \<bar> \<le> \<epsilon>"
-        using card_all_edges_betw_neighbor fin wf by simp
-      then have lt: "\<bar>edge_density X Y G - (1/(card ?X' * card Y)) * (\<Sum>x\<in>?X'. card (neighbors_ss x Y G)) \<bar> \<le> \<epsilon>"
-        by simp
-      thus False using lt con by linarith
-    qed (* Following Gowers's proof - more in depth with reasoning on contradiction *)
+  proof (rule ccontr)
+    assume "\<not> (card (X') <  \<epsilon> * card X) " 
+    then have a: "(card(X') \<ge>  \<epsilon> * card X) " by simp
+    have fin: "finite X" "finite Y" using assms finite_subset by auto
+    have ebound: "\<epsilon> \<le> 1/2"
+      by (metis ed edge_density_le1 le_divide_eq_numeral1(1) mult.commute order_trans)
+    have finx: "finite X'" using fin X'_def by simp 
+    have "\<And> x. x \<in> X'\<Longrightarrow> (card (neighbors_ss x Y G)) < (edge_density X Y G - \<epsilon>) * (card Y)"
+      unfolding X'_def by blast 
+    then have "(\<Sum>x\<in>X'. card (neighbors_ss x Y G)) < (\<Sum>x\<in>X'. ((edge_density X Y G - \<epsilon>) * (card Y)))"
+      using False sum_strict_mono X'_def
+      by (smt (verit, del_insts) finx of_nat_sum)
+    then have upper: "(\<Sum>x\<in>X'. card (neighbors_ss x Y G)) < (card X') * ((edge_density X Y G - \<epsilon>) * (card Y))"
+      by (simp add: sum_bounded_above)
+    have yge0: "card Y > 0"
+      by (metis gr0I mult_eq_0_iff of_nat_0 of_nat_less_0_iff upper)
+    have "?rxy > 0"
+      using card_0_eq finx False yge0 X'_def by fastforce 
+    then have upper2: "?rxy * (\<Sum>x\<in>X'. card (neighbors_ss x Y G)) < ?rxy * (card X') * ((edge_density X Y G - \<epsilon>) * (card Y))"
+      by (smt (verit) mult.assoc mult_le_cancel_left upper)
+    have minuse: "?rxy * (card X') * ((edge_density X Y G - \<epsilon>) * (card Y)) = edge_density X Y G - \<epsilon>"
+      using False X'_def finx by force
+    then have edlt1: "?rxy * (card X') * ((edge_density X Y G - \<epsilon>) * (card Y)) < edge_density X Y G" 
+      using eg0 by linarith
+    then have edlt2: "?rxy * (\<Sum>x\<in>X'. card (neighbors_ss x Y G)) < edge_density X Y G" 
+      using upper2 by linarith 
+    have "edge_density X Y G - ?rxy * (\<Sum>x\<in>X'. card (neighbors_ss x Y G)) > edge_density X Y G - (edge_density X Y G - \<epsilon>)"
+      using edlt1 edlt2 upper2 minuse by linarith
+    then have con: "edge_density X Y G - ?rxy * (\<Sum>x\<in>X'. card (neighbors_ss x Y G)) > \<epsilon>" by simp
+    have ye: "card Y \<ge> \<epsilon> * (card Y)" using ebound by (simp add: yge0)
+    have xe': "card X' \<ge> \<epsilon> * (card X)" using a by fastforce
+    have "\<bar>edge_density X Y G - ?rxy * (\<Sum>x\<in>X'. card (neighbors_ss x Y G))\<bar> 
+        = \<bar>?rxy * (card (all_edges_between X' Y G)) - edge_density X Y G\<bar>"
+      using card_all_edges_betw_neighbor fin wf by (simp add: X'_def)
+    also have "... = \<bar>edge_density X' Y G - edge_density X Y G\<bar>"
+      by (simp add: edge_density_def)
+    also have "... \<le> \<epsilon>"
+      using assms ye xe' by (force simp add: X'_def regular_pair_def)
+    finally show False using con by linarith
+  qed (* Following Gowers's proof - more in depth with reasoning on contradiction *)
 qed
 
 lemma neighbor_set_meets_e_reg_cond:
   fixes \<epsilon>::real 
   assumes "X \<subseteq> uverts G" and "Y \<subseteq> uverts G" and enot0: "\<epsilon> > 0"
     and fin: "finite X" "finite Y"  and "uwellformed G"    
     and rp1: "regular_pair X Y G \<epsilon>"
     and ed1: "edge_density X Y G  \<ge> 2*\<epsilon>"
   and "card (neighbors_ss x Y G) \<ge> (edge_density X Y G - \<epsilon>) * card Y"
 shows "card (neighbors_ss x Y G) \<ge> \<epsilon> * card (Y)"
 proof -
   have "card (neighbors_ss x Y G) \<ge> (edge_density X Y G - \<epsilon>) * card Y" using assms by simp
   thus ?thesis
     by (smt (verit, ccfv_SIG) mult_right_mono of_nat_less_0_iff ed1 enot0) 
 qed
 
 lemma all_edges_btwn_neighbour_sets_lower_bound: 
   fixes \<epsilon>::real 
   assumes "X \<subseteq> uverts G" and  "Y \<subseteq> uverts G" and "Z \<subseteq> uverts G" and "\<epsilon> > 0"
     and finG: "finite (uverts G)"
     and wf: "uwellformed G" and fin: "finite X" "finite Y" "finite Z" 
     and  rp1: "regular_pair X Y G \<epsilon> " and rp2: "regular_pair Y Z G \<epsilon>" and  rp3: "regular_pair X Z G \<epsilon>"
     and ed1: "edge_density X Y G  \<ge> 2*\<epsilon>" and ed2: "edge_density X Z G  \<ge> 2*\<epsilon>" and ed3: "edge_density Y Z G  \<ge> 2*\<epsilon>"
     and cond1: "card (neighbors_ss x Y G) \<ge> (edge_density X Y G - \<epsilon>) * card Y"
     and cond2: "card (neighbors_ss x Z G) \<ge> (edge_density X Z G - \<epsilon>) * card Z"
     and "x \<in> X"
   shows "card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G) 
       \<ge> (edge_density Y Z G - \<epsilon>) * card (neighbors_ss x Y G) * card (neighbors_ss x Z G)"
     (is "card (all_edges_between ?Y' ?Z' G) \<ge> (edge_density Y Z G - \<epsilon>) * card ?Y' * card ?Z'")
 proof -
   have yss': "?Y' \<subseteq> Y" using neighbors_ss_def by simp
   have zss': "?Z' \<subseteq> Z" using neighbors_ss_def by simp
-  have min_sizeY: "card ?Y' \<ge> \<epsilon> * card Y" using neighbor_set_meets_e_reg_cond cond1 assms fin by meson
-  have min_sizeZ: "card ?Z' \<ge> \<epsilon> * card Z" using neighbor_set_meets_e_reg_cond cond2 assms fin by meson
+  have min_sizeY: "card ?Y' \<ge> \<epsilon> * card Y" 
+    using neighbor_set_meets_e_reg_cond cond1 assms fin by meson
+  have min_sizeZ: "card ?Z' \<ge> \<epsilon> * card Z" 
+    using neighbor_set_meets_e_reg_cond cond2 assms fin by meson
   then have "\<bar> edge_density ?Y' ?Z' G - edge_density Y Z G \<bar> \<le> \<epsilon>"
-    using min_sizeY regular_pairI[of "\<epsilon>" "Y" "Z" "G" "?Y'" "?Z'"] yss' zss' assms by simp
-  then have "-\<epsilon> \<le> ( edge_density ?Y' ?Z' G - edge_density Y Z G)"
+    using min_sizeY yss' zss' assms by (force simp add: regular_pair_def)
+  then have "-\<epsilon> \<le> (edge_density ?Y' ?Z' G - edge_density Y Z G)"
     by linarith 
   then have "edge_density Y Z G - \<epsilon> \<le> edge_density ?Y' ?Z' G" by linarith
   then have "edge_density Y Z G - \<epsilon> \<le> (card (all_edges_between ?Y' ?Z' G)/(card ?Y' * card ?Z'))" using edge_density_def by simp
   then have "(card ?Y' * card ?Z') * (edge_density Y Z G - \<epsilon>) \<le> (card (all_edges_between ?Y' ?Z' G))"
     by (metis abs_of_nat division_ring_divide_zero le_divide_eq mult_of_nat_commute of_nat_0_le_iff times_divide_eq_right zero_less_abs_iff)
   then show ?thesis
     by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) mult_of_nat_commute of_nat_mult) 
 qed
 
 
 text\<open>We are now ready to show the Triangle Counting Lemma (Theorem 3.13 in Zhao's notes):\<close>
 
 theorem triangle_counting_lemma:
   fixes \<epsilon>::real 
   assumes xss: "X \<subseteq> uverts G" and yss: "Y \<subseteq> uverts G" and zss: "Z \<subseteq> uverts G" and en0: "\<epsilon> > 0"
     and finG: "finite (uverts G)" and wf: "uwellformed G"    
-    and rp1: "regular_pair X Y G \<epsilon> " and rp2: "regular_pair Y Z G \<epsilon>" and  rp3: "regular_pair X Z G \<epsilon>"
-    and ed1: "edge_density X Y G  \<ge> 2*\<epsilon>" and ed2: "edge_density X Z G \<ge> 2*\<epsilon>" and ed3: "edge_density Y Z G  \<ge> 2*\<epsilon>"
+    and rp1: "regular_pair X Y G \<epsilon>" and rp2: "regular_pair Y Z G \<epsilon>" and  rp3: "regular_pair X Z G \<epsilon>"
+    and ed1: "edge_density X Y G \<ge> 2*\<epsilon>" and ed2: "edge_density X Z G \<ge> 2*\<epsilon>" and ed3: "edge_density Y Z G \<ge> 2*\<epsilon>"
   shows "card (triangle_triples X Y Z G)
-      \<ge> (1-2*\<epsilon>)*((edge_density X Y G) - \<epsilon>)*((edge_density X Z G) - \<epsilon>) *((edge_density Y Z G) - \<epsilon>)*
-        (card X)*(card Y)* (card Z)" 
+        \<ge> (1-2*\<epsilon>) * ((edge_density X Y G) - \<epsilon>) * ((edge_density X Z G) - \<epsilon>) * ((edge_density Y Z G) - \<epsilon>)*
+           card X * card Y * card Z" 
 proof -
   let ?T_all = "{(x,y,z) \<in> X \<times> Y \<times> Z. (triangle_in_graph x y z G)}"
   define XF where "XF \<equiv> \<lambda>Y. {x \<in> X. card(neighbors_ss x Y G) < ((edge_density X Y G) - \<epsilon>) * card Y}"
   have fin: "finite X" "finite Y" "finite Z" using finG rev_finite_subset xss yss zss by auto
   have "card X > 0"
     using card_0_eq ed1 edge_density_def en0 fin(1) by fastforce
-  have ebound: "\<epsilon> \<le> 1/2"
+  have "\<epsilon> \<le> 1/2"
     using ed1 edge_density_le1 fin
     by (metis le_divide_eq_numeral1(1) mult.commute order_trans)
   then have ebound2: "1 - 2*\<epsilon> \<ge> 0"
     by linarith 
   
   text\<open> Obtain a subset of @{term X} where all elements meet minimum numbers for neighborhood size
 in @{term Y} and @{term Z}.\<close>
   
   define X2 where "X2 \<equiv> X - (XF Y \<union> XF Z)"
   have xss: "X2 \<subseteq> X"
     by (simp add: X2_def)
   have finx2: "finite X2"
     by (simp add: X2_def fin)
   
   text \<open>Reasoning on the minimum size of @{term X2}:\<close>
   
   have part1: "(XF Y \<union> XF Z) \<union> X2 = X"
     by (auto simp: XF_def X2_def)
   have card_XFY: "card (XF Y) <  \<epsilon> * card X" 
     using regular_pair_neighbor_bound assms \<open>card X > 0\<close> by (simp add: XF_def)
   
   text\<open> We now repeat the same argument as above to the regular pair @{term X} @{term Z} in @{term G}.\<close>
   
   have card_XFZ: "card (XF Z) <  \<epsilon> * card X"
     using regular_pair_neighbor_bound assms \<open>card X > 0\<close> by (simp add: XF_def)
   have "card (XF Y \<union> XF Z) \<le> 2 * \<epsilon> * (card X)"
     by (smt (verit) card_XFY card_XFZ card_Un_le comm_semiring_class.distrib of_nat_add of_nat_mono)
   then have minx2help: "card X2 \<ge> card X -  2 * \<epsilon> * card X" using part1
     by (smt (verit, del_insts) card_Un_le of_nat_add of_nat_mono) 
   then have minx2: "card X2 \<ge> (1 - 2 * \<epsilon>) * card X"
     by (metis mult.commute mult_cancel_left2 right_diff_distrib)
-  have edmultbound: "((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>)* (card Y) * (edge_density X Z G - \<epsilon>)* (card Z) \<ge> 0"  
+  have edmultbound: "((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>) * (card Y) * (edge_density X Z G - \<epsilon>) * (card Z) \<ge> 0"  
     using ed3 ed1 ed2 \<open>\<epsilon> > 0\<close> by auto 
   
   text \<open>Reasoning on the minimum number of edges between neighborhoods of @{term X} in @{term Y} 
 and @{term Z}.\<close>
  
   have edyzgt0: "((edge_density Y Z G) - \<epsilon>) > 0"
    and edxygt0: "((edge_density X Y G) - \<epsilon>) > 0" using ed1 ed3 \<open>\<epsilon> > 0\<close> by linarith+
   have cardnzgt0: "card (neighbors_ss x Z G) \<ge> 0" and cardnygt0: "card (neighbors_ss x Y G) \<ge> 0" 
              if "x \<in> X2" for x
     by auto
   have card_y_bound: "\<And>x. x \<in> X2 \<Longrightarrow> (card (neighbors_ss x Y G)) \<ge> (edge_density X Y G - \<epsilon>) * (card Y)"
     by (auto simp: XF_def X2_def)
   have card_z_bound: "\<And>x. x \<in> X2 \<Longrightarrow> (card (neighbors_ss x Z G)) \<ge> (edge_density X Z G - \<epsilon>) * (card Z)"
     by (auto simp: XF_def X2_def)   
   have card_y_bound': 
           "(\<Sum>x\<in> X2. ((edge_density Y Z G) - \<epsilon>) * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G))) \<ge>
-           (\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>)* (card Y) * (card (neighbors_ss x Z G)))" 
+           (\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>) * (card Y) * (card (neighbors_ss x Z G)))" 
       by (rule sum_mono) (smt (verit, best) Groups.mult_ac(3) card_y_bound edyzgt0 mult.commute mult_right_mono of_nat_0_le_iff)
   have x2_card: "\<And>x. x \<in> X2 \<Longrightarrow> ((edge_density Y Z G) - \<epsilon>) * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G))
                     \<le> card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G)"
     by (meson all_edges_btwn_neighbour_sets_lower_bound assms(1) card_y_bound card_z_bound ed1 ed2 ed3 en0 fin finG local.wf rp1 rp2 rp3 subsetD xss yss zss)
   have card_z_bound': 
-         "(\<Sum>x\<in> X2. ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>)* (card Y) * (card (neighbors_ss x Z G))) \<ge>
-          (\<Sum>x\<in> X2. ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>)* (card Y) * (edge_density X Z G - \<epsilon>)* (card Z))" 
+         "(\<Sum>x\<in> X2. ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>) * (card Y) * (card (neighbors_ss x Z G))) \<ge>
+          (\<Sum>x\<in> X2. ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>) * (card Y) * (edge_density X Z G - \<epsilon>) * (card Z))" 
       using card_z_bound mult_left_mono edxygt0 edyzgt0 by (fastforce intro!: sum_mono)
   have eq_set: "\<And> x. x \<in> X \<Longrightarrow> card {(y, z) . y \<in> Y \<and> z \<in> Z \<and> {y, z} \<in> uedges G \<and> neighbor_in_graph x y G \<and> neighbor_in_graph x z G } = 
 card {(y, z) . y \<in> (neighbors_ss x Y G) \<and> z \<in> (neighbors_ss x Z G) \<and> {y, z} \<in> uedges G }"
     by (metis (no_types, lifting) mem_Collect_eq neighbors_ss_def)
   have "card ?T_all = (\<Sum>x\<in> X . card {(y,z) \<in> Y \<times> Z. triangle_in_graph x y z G})"
     using triple_sigma_rewrite_card fin by force  
   also have "\<dots> = (\<Sum>x\<in> X . card {(y,z) \<in> Y \<times> Z. {y,z} \<in> uedges G \<and> neighbor_in_graph x y G \<and> neighbor_in_graph x z G })"
     using triangle_in_graph_edge_point assms by auto
   also have "\<dots> = (\<Sum>x\<in> X . card {(y, z). y \<in> Y \<and> z \<in> Z \<and> {y, z} \<in> uedges G \<and> neighbor_in_graph x y G \<and> neighbor_in_graph x z G })"
     by simp
   finally have "card ?T_all = (\<Sum>x\<in> X . card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G))"
     using eq_set by (auto simp: all_edges_between_def)
   then have l: "card ?T_all \<ge> (\<Sum>x\<in> X2 . card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G))"
     by (simp add: fin xss sum_mono2)
   have "(\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G))) \<le> 
         (\<Sum>x\<in> X2. real (card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G)))"
     by (meson x2_card finx2 sum_mono)
   then have "card ?T_all \<ge> (\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G)))" 
     using l of_nat_le_iff [symmetric, where 'a=real] by force
-  then have "card ?T_all \<ge> (\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>)* (card Y) * (card (neighbors_ss x Z G)))" 
+  then have "card ?T_all \<ge> (\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>) * (card Y) * (card (neighbors_ss x Z G)))" 
     using card_y_bound' by simp
-  then have tall_gt: "card ?T_all \<ge> (\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>)* (card Y) * (edge_density X Z G - \<epsilon>)* (card Z))" 
+  then have tall_gt: "card ?T_all \<ge> (\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>) * (card Y) * (edge_density X Z G - \<epsilon>) * (card Z))" 
     using card_z_bound' by simp
-  have "(\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>)* (card Y) * (edge_density X Z G - \<epsilon>)* (card Z)) = 
-    card X2 * ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>)* (card Y) * (edge_density X Z G - \<epsilon>)* (card Z)"
+  have "(\<Sum>x\<in> X2 . ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>) * (card Y) * (edge_density X Z G - \<epsilon>) * (card Z)) = 
+    card X2 * ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>) * (card Y) * (edge_density X Z G - \<epsilon>) * (card Z)"
     by simp 
   then have "of_real (card ?T_all) \<ge> card X2 * ((edge_density Y Z G) - \<epsilon>) * (edge_density X Y G - \<epsilon>)* 
-      (card Y) * (edge_density X Z G - \<epsilon>)* (card Z)"
+      (card Y) * (edge_density X Z G - \<epsilon>) * (card Z)"
     using tall_gt
     by force 
   then have "of_real (card ?T_all) \<ge> ((1 - 2 * \<epsilon>) * card X) * ((edge_density Y Z G) - \<epsilon>) * 
-      (edge_density X Y G - \<epsilon>)* (card Y) * (edge_density X Z G - \<epsilon>)* (card Z)"
+      (edge_density X Y G - \<epsilon>) * (card Y) * (edge_density X Z G - \<epsilon>) * (card Z)"
     by (smt (verit, best) ed2 edxygt0 edyzgt0 en0 minx2 mult_right_less_imp_less of_nat_less_0_iff)
   then show ?thesis by (simp add: triangle_triples_def mult.commute mult.left_commute) 
 qed
 
 definition regular_graph :: "uvert set set \<Rightarrow> ugraph \<Rightarrow> real \<Rightarrow> bool"
   where "regular_graph P G \<epsilon> \<equiv> \<forall>R S. R\<in>P \<longrightarrow> S\<in>P \<longrightarrow> regular_pair R S G \<epsilon>" for \<epsilon>::real
 
 text \<open>A minimum density, but empty edge sets are excluded.\<close>
 
 definition edge_dense :: "nat set \<Rightarrow> nat set \<Rightarrow> ugraph \<Rightarrow> real \<Rightarrow> bool"
   where "edge_dense X Y G \<epsilon> \<equiv> all_edges_between X Y G = {} \<or> edge_density X Y G \<ge> \<epsilon>"
 
 definition dense_graph :: "uvert set set \<Rightarrow> ugraph \<Rightarrow> real \<Rightarrow> bool"
   where "dense_graph P G \<epsilon> \<equiv> \<forall>R S. R\<in>P \<longrightarrow> S\<in>P \<longrightarrow> edge_dense R S G \<epsilon>" for \<epsilon>::real
 
 definition decent :: "nat set \<Rightarrow> nat set \<Rightarrow> ugraph \<Rightarrow> real \<Rightarrow> bool"
   where "decent X Y G \<eta> \<equiv> all_edges_between X Y G = {} \<or> (real (card X) \<ge> \<eta> \<and> real (card Y) \<ge> \<eta>)"
 
 definition decent_graph :: "uvert set set \<Rightarrow> ugraph \<Rightarrow> real \<Rightarrow> bool"
   where "decent_graph P G \<eta> \<equiv> \<forall>R S. R\<in>P \<longrightarrow> S\<in>P \<longrightarrow> decent R S G \<eta>" for \<epsilon>::real
 
 text \<open>The proof of the triangle counting lemma requires ordered triples. For each unordered triple 
 there are six permutations, hence the factor of $1/6$ here. This is mentioned briefly on pg 57 of 
 Zhao's notes towards the end of the proof.\<close>
 
 lemma card_convert_triangle_rep:
   fixes G :: "ugraph" 
   assumes "X \<subseteq> uverts G" and "Y \<subseteq> uverts G" and "Z \<subseteq> uverts G" and fin: "finite (uverts G)" 
 and wf: "uwellformed G"
   shows "card (triangle_set G) \<ge> 1/6 * card {(x, y, z) \<in> X \<times> Y \<times> Z . (triangle_in_graph x y z G)}"
          (is  "_ \<ge> 1/6 * card ?TT")
 proof -
   define tofl where "tofl \<equiv> \<lambda>l::nat list. (hd l, hd(tl l), hd(tl(tl l)))"
   have in_tofl: "(x, y, z) \<in> tofl ` permutations_of_set {x,y,z}" if "x\<noteq>y" "y\<noteq>z" "x\<noteq>z" for x y z
   proof -
     have "distinct[x,y,z]"
       using that by simp
     then show ?thesis
       unfolding tofl_def image_iff
       by (smt (verit, best) list.sel(1) list.sel(3) list.simps(15) permutations_of_setI set_empty)
   qed
   have "?TT \<subseteq> {(x, y, z). (triangle_in_graph x y z G)}"
     by auto
   also have "\<dots> \<subseteq> (\<Union>t \<in> triangle_set G. tofl ` permutations_of_set t)"
   proof (clarsimp simp: triangle_set_def)
     fix u v w
     assume t: "triangle_in_graph u v w G"
     then have "(u, v, w) \<in> tofl ` permutations_of_set {u,v,w}"
       by (metis in_tofl local.wf triangle_commu1 triangle_vertices_distinct1 triangle_vertices_distinct2)
     with t show "\<exists>t. (\<exists>x y z. t = {x, y, z} \<and> triangle_in_graph x y z G) \<and> (u, v, w) \<in> tofl ` permutations_of_set t"
       by blast
   qed
   finally have "?TT \<subseteq> (\<Union>t \<in> triangle_set G. tofl ` permutations_of_set t)" .
   then have "card ?TT \<le> card(\<Union>t \<in> triangle_set G. tofl ` permutations_of_set t)" 
     by (intro card_mono finite_UN_I finite_triangle_set) (auto simp: assms)
   also have "\<dots> \<le> (\<Sum>t \<in> triangle_set G. card (tofl ` permutations_of_set t))"
     using card_UN_le fin finite_triangle_set local.wf by blast
   also have "\<dots> \<le> (\<Sum>t \<in> triangle_set G. card (permutations_of_set t))"
     by (meson card_image_le finite_permutations_of_set sum_mono)
   also have "\<dots> \<le> (\<Sum>t \<in> triangle_set G. fact 3)"
     apply (rule sum_mono)
     by (metis card.infinite card_permutations_of_set card_triangle_3 eq_refl local.wf nat.simps(3) numeral_3_eq_3)
   also have "\<dots> = 6 * card (triangle_set G)"
     by (simp add: eval_nat_numeral)
   finally have "card ?TT \<le> 6 * card (triangle_set G)" .
   then show ?thesis
     by (simp add: divide_simps)
 qed
 
 lemma card_convert_triangle_rep_bound: 
   fixes G :: "ugraph" and t :: real
   assumes "card {(x, y, z) \<in> X \<times> Y \<times> Z . (triangle_in_graph x y z G)} \<ge> t"
   assumes "X \<subseteq> uverts G" and "Y \<subseteq> uverts G" and "Z \<subseteq> uverts G" and fin: "finite (uverts G)" 
 and wf: "uwellformed G"
   shows "card (triangle_set G) \<ge> 1/6 *t"
 proof -
   define t' where "t' \<equiv> card {(x, y, z) \<in> X \<times> Y \<times> Z . (triangle_in_graph x y z G)}"
   have "t' \<ge> t" using assms t'_def by simp
   then have tgt: "1/6 * t' \<ge> 1/6 * t" by simp
   have "card (triangle_set G) \<ge> 1/6 *t'" using t'_def card_convert_triangle_rep assms by simp
   thus ?thesis using tgt by linarith
 qed
 
- lemma edge_density_eq0:
+lemma edge_density_eq0:
   assumes "all_edges_between A B G = {}" and "X \<subseteq> A" "Y \<subseteq> B"
   shows "edge_density X Y G = 0"
 proof -
   have "all_edges_between X Y G = {}"
     by (metis all_edges_between_mono1 all_edges_between_mono2 assms subset_empty)
   then show ?thesis
     by (auto simp: edge_density_def)
 qed
 
 text\<open>The following is the Triangle Removal Lemma (Theorem 3.15 in Zhao's notes).\<close>
 
 theorem triangle_removal_lemma:
   fixes \<epsilon> :: real
   assumes egt: "\<epsilon> > 0"
   shows "\<exists>\<delta>::real > 0. \<forall>G. card(uverts G) > 0 \<longrightarrow> uwellformed G \<longrightarrow> 
           card (triangle_set G) \<le> \<delta> * card(uverts G) ^ 3 \<longrightarrow>
-          (\<exists>Gnew. triangle_free_graph Gnew \<and> uverts Gnew = uverts G \<and> (uedges Gnew \<subseteq> uedges G) \<and> 
-          card (uedges G - uedges Gnew) \<le> \<epsilon> * (card (uverts G))\<^sup>2)"
+          (\<exists>G'. triangle_free_graph G' \<and> uverts G' = uverts G \<and> uedges G' \<subseteq> uedges G \<and> 
+          card (uedges G - uedges G') \<le> \<epsilon> * (card (uverts G))\<^sup>2)"
     (is "\<exists>\<delta>::real > 0. \<forall>G. _ \<longrightarrow> _ \<longrightarrow> _ \<longrightarrow> (\<exists>Gnew. ?\<Phi> G Gnew)")
 proof (cases "\<epsilon> < 1")
   case False
   define Gnew where "Gnew \<equiv> \<lambda>G. ((uverts G), {}::uedge set)"
   show ?thesis
   proof (intro exI conjI strip)
     fix G
     assume G: "uwellformed G" "card(uverts G) > 0"
     then show "triangle_free_graph (Gnew G)" "uverts (Gnew G) = uverts G" "uedges (Gnew G) \<subseteq> uedges G"
       by (auto simp: Gnew_def triangle_free_graph_empty)
     have "real (card (uedges G)) \<le> (card (uverts G))\<^sup>2"
       by (meson G card_gt_0_iff max_edges_graph of_nat_le_iff)
     also have "\<dots> \<le> \<epsilon> * (card (uverts G))\<^sup>2"
       using False mult_le_cancel_right1 by fastforce
     finally show "real (card (uedges G - uedges (Gnew G))) \<le> \<epsilon> * real ((card (uverts G))\<^sup>2)"
       by (simp add: Gnew_def)
   qed (rule zero_less_one)
 next
   case True
   have e4gt: "\<epsilon>/4 > 0" using \<open>\<epsilon> > 0\<close> by auto
   then obtain M0 where 
     M0: "\<And>G. card (uverts G) > 0 \<Longrightarrow> \<exists>P. regular_partition (\<epsilon>/4) G P \<and> card P \<le> M0" 
     and "M0>0"
     by (metis Szemeredi_Regularity_Lemma le0 neq0_conv not_le not_numeral_le_zero)
   define D0 where "D0 \<equiv> 1/6 *(1-(\<epsilon>/2))*((\<epsilon>/4)^3)*((\<epsilon> /(4*M0))^3)"
   have "D0 > 0" 
     using \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close> \<open>M0 > 0\<close> by (simp add: D0_def zero_less_mult_iff)
   then obtain \<delta>:: "real" where \<delta>: "0 < \<delta>" "\<delta> < D0"
     by (meson dense)
   show ?thesis
   proof (rule exI, intro conjI strip)
     fix G
     assume "card(uverts G) > 0" and wf: "uwellformed G"
     then have fin: "finite (uverts G)"
       by (simp add: card_gt_0_iff)
     
     text\<open>Assume that, for a yet to be determined $\delta$, we have:\<close>
     assume ineq: "real (card (triangle_set G)) \<le> \<delta> * card (uverts G) ^ 3"
     
     text\<open>Step 1: Partition: Using Szemer\'{e}di's Regularity Lemma, we get an $\epsilon/4$ partition. \<close>
     
     let ?n = "card (uverts G)"
     have vne: "uverts G \<noteq> {}"
       using \<open>0 < card (uverts G)\<close> by force 
     then have ngt0: "?n > 0"
       by (simp add: fin card_gt_0_iff)
     with M0 obtain P where M: "regular_partition (\<epsilon>/4) G P" and "card P \<le> M0"
       by blast
     define M where "M \<equiv> card P"
     have "finite P"
       by (meson M fin finite_elements regular_partition_def)
     with M0 have "M > 0"
       unfolding M_def
       by (metis M card_gt_0_iff partition_onD1 partition_on_empty regular_partition_def vne)
     let ?e4M = "\<epsilon> / (4 * real M)"
     define D where "D \<equiv> 1/6 *(1-(\<epsilon>/2)) * ((\<epsilon>/4)^3) * ?e4M^3"
     have "D > 0" 
       using \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close> \<open>M > 0\<close> by (simp add: D_def zero_less_mult_iff)
     have "D0 \<le> D"
       unfolding D0_def D_def using \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close> \<open>card P \<le> M0\<close> \<open>M > 0\<close>
       by (intro mult_mono) (auto simp: frac_le M_def)
         (* a reminder: as it is implied we have: *)  
     have fin_part: "finite_graph_partition (uverts G) P M"
       using M unfolding regular_partition_def finite_graph_partition_def
       by (metis M_def \<open>0 < M\<close> card_gt_0_iff)
     then have fin_P: "finite R" and card_P_gt0: "card R > 0" if "R\<in>P" for R
       using fin finite_graph_partition_finite finite_graph_partition_gt0 that by auto
     have card_P_le: "card R \<le> ?n" if "R\<in>P" for R
       by (meson card_mono fin fin_part finite_graph_partition_subset that)
     have P_disjnt: "\<And>R S. \<lbrakk>R \<noteq> S; R \<in> P; S \<in> P\<rbrakk> \<Longrightarrow> R \<inter> S = {}"
       using fin_part
       by (metis disjnt_def finite_graph_partition_def insert_absorb pairwise_insert partition_on_def) 
     have sum_card_P: "(\<Sum>R\<in>P. card R) = ?n"
       using card_finite_graph_partition fin fin_part by meson
     
     text\<open>Step 2. Cleaning. For each ordered pair of parts $(P_i,P_j)$, remove all edges between 
       $P_i$ and $P_j$ if (a) it is an irregular pair, (b) its edge density ${} < \epsilon/2$, 
       (c) either $P_i$ or $P_j$ is small (${}\le(\epsilon/4M)n$)
     Process (a) removes at most $(\epsilon/4)n^2$ edges. 
     Process (b) removes at most $(\epsilon/2)n^2$ edges.
     Process (c) removes at most $(\epsilon/4)n^2$ edges. 
    The remaining graph is triangle-free for some choice of $\delta$.
    We call the graph obtained after this process @{term Gnew}.  \<close>
     
     define edge where "edge \<equiv> \<lambda>R S. mk_uedge ` (all_edges_between R S G)"
     have edge_commute: "edge R S = edge S R" for R S
       by (force simp add: edge_def all_edges_between_swap [of S] split: prod.split)
     have card_edge_le_card: "card (edge R S) \<le> card (all_edges_between R S G)" for R S
       by (simp add: card_image_le edge_def fin finite_all_edges_between' local.wf)
     have card_edge_le: "card (edge R S) \<le> card R * card S" if "R\<in>P" "S\<in>P" for R S
       by (meson card_edge_le_card fin_P le_trans max_all_edges_between that)
     
     text \<open>Obtain the set of edges meeting condition (a).\<close>
     
     define irreg_pairs where "irreg_pairs \<equiv> {(R,S). R \<in> P \<and> S \<in> P \<and> \<not> regular_pair R S G (\<epsilon>/4)}"
     define Ea where "Ea \<equiv> (\<Union>(R,S) \<in> irreg_pairs. edge R S)"
     
     text \<open>Obtain the set of edges meeting condition (b).\<close>
     
     define low_density_pairs
       where "low_density_pairs \<equiv> {(R,S). R \<in> P \<and> S \<in> P \<and> \<not> edge_dense R S G (\<epsilon>/2)}"
     define Eb where "Eb \<equiv> (\<Union>(i,j) \<in> low_density_pairs. edge i j)"
     
     text \<open>Obtain the set of edges meeting condition (c).\<close>
     
     define small where "small \<equiv> \<lambda>R. R \<in> P \<and> card R \<le> ?e4M * ?n"
     let ?SMALL = "Collect small"
     define small_pairs where "small_pairs \<equiv> {(R,S). R \<in> P \<and> S \<in> P \<and> (small R \<or> small S)}"
     define Ec where "Ec \<equiv> (\<Union>R \<in> ?SMALL. \<Union>S \<in> P. edge R S)"
     have Ec_def': "Ec = (\<Union>(i,j) \<in> small_pairs. edge i j)"
       by (force simp: edge_commute small_pairs_def small_def Ec_def)
     have eabound: "card Ea \<le> (\<epsilon>/4) * ?n^2"  \<comment>\<open>Count the edge bound for @{term Ea}\<close>
     proof - 
       have \<section>: "\<And>R S. \<lbrakk>R \<in> P; S \<in> P\<rbrakk> \<Longrightarrow> card (edge R S) \<le> card R * card S"
         unfolding edge_def
         by (meson card_image_le fin_P finite_all_edges_between max_all_edges_between order_trans)
       have "irreg_pairs \<subseteq> P \<times> P"
         by (auto simp: irreg_pairs_def)
       then have "finite irreg_pairs"
         by (meson \<open>finite P\<close> finite_SigmaI finite_subset)
       have "card Ea \<le> (\<Sum>(R,S)\<in>irreg_pairs. card (edge R S))"
         by (simp add: Ea_def card_UN_le [OF \<open>finite irreg_pairs\<close>] case_prod_unfold)
       also have "\<dots> \<le> (\<Sum>(R,S) \<in> {(R,S). R\<in>P \<and> S\<in>P \<and> \<not> regular_pair R S G (\<epsilon>/4)}. card R * card S)"
         unfolding irreg_pairs_def using \<section> by (force intro: sum_mono)
       also have "\<dots> = (\<Sum>(R,S) \<in> irregular_set (\<epsilon>/4) G P. card R * card S)"
         by (simp add: irregular_set_def)
       finally have "card Ea \<le> (\<Sum>(R,S) \<in> irregular_set (\<epsilon>/4) G P. card R * card S)" .
       with M show ?thesis
         unfolding regular_partition_def by linarith 
     qed
     have ebbound: "card Eb \<le> (\<epsilon>/2) * (?n^2)"  \<comment>\<open>Count the edge bound for @{term Eb}.\<close>
     proof - 
       have subs: "low_density_pairs \<subseteq> P \<times> P"
         by (auto simp: low_density_pairs_def)
       then have "finite low_density_pairs"
         by (metis \<open>finite P\<close> finite_SigmaI finite_subset)
       have "real (card Eb) \<le> (\<Sum>(i,j)\<in>low_density_pairs. real (card (edge i j)))"
         unfolding Eb_def
         by (smt (verit, ccfv_SIG) \<open>finite low_density_pairs\<close> card_UN_le of_nat_mono of_nat_sum 
  case_prod_unfold sum_mono)
       also have "\<dots> \<le> (\<Sum>(R,S)\<in>low_density_pairs. \<epsilon>/2 * card R * card S)"
         apply (rule sum_mono)
         apply(auto simp add: divide_simps card_P_gt0 low_density_pairs_def edge_density_def 
  edge_dense_def)
         by (smt (verit, best) card_edge_le_card of_nat_le_iff mult.assoc)
       also have "\<dots> \<le> (\<Sum>(R,S)\<in>P \<times> P. \<epsilon>/2 * card R * card S)"
         using subs \<open>\<epsilon> > 0\<close> by (intro sum_mono2) (auto simp: \<open>finite P\<close>)
       also have "\<dots> = \<epsilon>/2 * (\<Sum>(R,S)\<in>P \<times> P. card R * card S)"
         by (simp add: sum_distrib_left case_prod_unfold mult_ac)
       also have "\<dots> \<le> (\<epsilon>/2) * (?n^2)"
         using \<open>\<epsilon>>0\<close> sum_prod_le_prod_sum 
         by (simp add: power2_eq_square sum_product flip: sum.cartesian_product sum_card_P)
       finally show ?thesis .
     qed
     have ecbound: "card Ec \<le> (\<epsilon>/4) * (?n^2)"  \<comment>\<open>Count the edge bound for @{term Ec}.\<close>
     proof - 
       have edge_bound: "(card (edge R S)) \<le> ?e4M * ?n^2"
         if "S \<in> P" "small R" for R S
       proof -
         have "real (card R) \<le> \<epsilon> * ?n / (4 * real M)"
           using that by (simp add: small_def)
         with card_P_le [OF \<open>S\<in>P\<close>]
         have *: "real (card R) * real (card S) \<le> \<epsilon> * card (uverts G) / (4 * real M) * ?n"
           by (meson mult_mono of_nat_0_le_iff of_nat_mono order.trans)
         also have "\<dots> = ?e4M * ?n^2"
           by (simp add: power2_eq_square)
         finally show ?thesis
           by (smt (verit) card_edge_le of_nat_mono of_nat_mult small_def that)
       qed
       have subs: "?SMALL \<subseteq> P"
         by (auto simp: small_def)
       then obtain card_sp: "card (?SMALL) \<le> M" and "finite ?SMALL"
         using M_def \<open>finite P\<close> card_mono by (metis finite_subset)
       have "real (card Ec) \<le> (\<Sum>R \<in> ?SMALL. real (card (\<Union>S \<in> P. edge R S)))"
         unfolding Ec_def
         by (smt (verit, ccfv_SIG) \<open>finite ?SMALL\<close> card_UN_le of_nat_mono of_nat_sum case_prod_unfold sum_mono)
       also have "\<dots> \<le> (\<Sum>R \<in> ?SMALL. ?e4M * ?n^2)"
       proof (intro sum_mono)
         fix R assume i: "R \<in> Collect small"
         then have "R\<in>P" and card_Pi: "card R \<le> ?e4M * ?n"
           by (auto simp: small_def)
         let ?UE = "\<Union>(edge R ` (P))"
         have *: "real (card ?UE) \<le> real (card R * ?n)" 
         proof -
           have "?UE \<subseteq> mk_uedge ` (all_edges_between R (uverts G) G)"
             apply (simp add: edge_def UN_subset_iff Ball_def)
             by (meson all_edges_between_mono2 fin_part finite_graph_partition_subset image_mono)
           then have "card ?UE \<le> card (all_edges_between R (uverts G) G)"
             by (meson card_image_le card_mono fin finite_all_edges_between' finite_imageI wf le_trans)
           then show ?thesis
             by (meson of_nat_mono fin fin_P max_all_edges_between order.trans \<open>R\<in>P\<close>)
         qed
         also have "\<dots> \<le> ?e4M * real (?n\<^sup>2)"
           using card_Pi \<open>M > 0\<close> \<open>?n > 0\<close> by (force simp add: divide_simps power2_eq_square)
         finally show "real (card ?UE) \<le> ?e4M * real (?n\<^sup>2)" .
       qed
       also have "\<dots> \<le> card ?SMALL * (?e4M * ?n^2)"
         by simp
       also have "\<dots> \<le> M * (?e4M * ?n^2)"
         using egt by (intro mult_right_mono) (auto simp add: card_sp)
       also have "\<dots> \<le> (\<epsilon>/4) * (?n^2)"
         using \<open>M > 0\<close> by simp
       finally show ?thesis .
     qed
     \<comment>\<open>total count\<close>
     have prev1: "card (Ea \<union> Eb \<union> Ec) \<le> card (Ea \<union> Eb) + card Ec" by (simp add: card_Un_le)
     also have "\<dots> \<le> card Ea + card Eb + card Ec" by (simp add: card_Un_le)
     also have prev: "\<dots> \<le> (\<epsilon>/4)*(?n^2) + (\<epsilon>/2)*(?n^2) + (\<epsilon>/4)*(?n^2)"
       using eabound ebbound ecbound by linarith 
     finally have cutedgesbound: "card (Ea \<union> Eb \<union> Ec) \<le> \<epsilon> * (?n^2)" by simp
 
     define Gnew where "Gnew \<equiv> (uverts G, uedges G - (Ea \<union> Eb \<union> Ec))"
     show "\<exists>Gnew. ?\<Phi> G Gnew"
     proof (intro exI conjI)
       show verts: "uverts Gnew = uverts G" by (simp add: Gnew_def)
       have allij: "\<And>R S. edge R S \<subseteq> uedges G" 
         using all_edges_between_ss_uedges edge_def by presburger
       then have eae: "Ea \<subseteq> uedges G" by (auto simp: Ea_def) 
       have eab: "Eb \<subseteq> uedges G" using allij by (auto simp: Eb_def)
       have "Ec \<subseteq> uedges G" using allij by (auto simp: Ec_def)
       then have diffedges: "(Ea \<union> Eb \<union> Ec) \<subseteq> uedges G" 
         using eae eab by auto
       then show edges: "uedges Gnew \<subseteq> uedges G"  
         by (simp add: Gnew_def)
       then have "uedges G - (uedges Gnew) = uedges G \<inter> (Ea \<union> Eb \<union> Ec) " 
         by (simp add: Gnew_def Diff_Diff_Int) 
       then have "uedges G - (uedges Gnew) = (Ea \<union> Eb \<union> Ec)" using diffedges
         by (simp add: Int_absorb1) 
       then have cardbound: "card (uedges G - uedges Gnew) \<le> \<epsilon> * (?n^2)" 
         using cutedgesbound by simp
       have graph_partition_new: "finite_graph_partition (uverts Gnew) P M" using verts
         by (simp add: fin_part) 
       have new_wf: "uwellformed Gnew" using subgraph_edge_wf verts edges wf by simp
       have new_fin: "finite (uverts Gnew)" using verts fin by simp
       
       text\<open> The notes by Bell and Grodzicki are quite useful for understanding the lines below.
          See pg 4 in the middle after the summary of the min edge counts.\<close>
       
       have irreg_pairs_swap: "(R,S) \<in> irreg_pairs \<longleftrightarrow> (S, R) \<in> irreg_pairs" for R S
         by (auto simp: irreg_pairs_def regular_pair_commute)
       have low_density_pairs_swap: "(R,S) \<in> low_density_pairs \<longleftrightarrow> (S,R) \<in> low_density_pairs" for R S
         by (simp add: low_density_pairs_def edge_density_commute edge_dense_def)
            (use all_edges_between_swap in blast)
       have small_pairs_swap: "(R,S) \<in> small_pairs \<longleftrightarrow> (S,R) \<in> small_pairs" for R S
         by (auto simp: small_pairs_def)
 
       have all_edges_if: 
         "all_edges_between R S Gnew 
          = (if (R,S) \<in> irreg_pairs \<union> low_density_pairs \<union> small_pairs then {} 
             else all_edges_between R S G)" 
         (is "?lhs = ?rhs")
         if ij: "R \<in> P" "S \<in> P" for R S
       proof
         show "?lhs \<subseteq> ?rhs"
           using that fin_part unfolding Gnew_def Ea_def Eb_def Ec_def'
           apply (simp add: all_edges_between_E_diff all_edges_between_E_Un all_edges_between_E_UN)
           apply (auto simp: edge_def in_mk_uedge_img_iff all_edges_between_def)
           done
       next
         have Ea: "all_edges_between R S (V, Ea) = {}"  
           if "(R,S) \<notin> irreg_pairs" for V
           using ij that P_disjnt
           by (auto simp: Ea_def doubleton_eq_iff edge_def all_edges_between_def irreg_pairs_def; 
               metis regular_pair_commute disjoint_iff_not_equal)
         have Eb: "all_edges_between R S (V, Eb) = {}"  
           if "(R,S) \<notin> low_density_pairs" for V
           using ij that  
           apply (auto simp: Eb_def edge_def all_edges_between_def low_density_pairs_def edge_dense_def)
            apply metis
           by (metis IntI P_disjnt doubleton_eq_iff edge_density_commute equals0D)
         have Ec: "all_edges_between R S (V, Ec) = {}"
           if "(R,S) \<notin> small_pairs" for V
           using ij that 
           by (auto simp: Ec_def' doubleton_eq_iff edge_def all_edges_between_def small_pairs_def;
               metis P_disjnt disjoint_iff)
         show "?rhs \<subseteq> ?lhs"
           by (auto simp add: Gnew_def Ea Eb Ec all_edges_between_E_diff all_edges_between_E_Un)
       qed
 
       have rp: "regular_pair R S Gnew (\<epsilon>/4)" if ij: "R \<in> P" "S \<in> P"  for R S
       proof (cases "(R,S) \<in> irreg_pairs")
         case False
         have ed: "edge_density X Y Gnew =
             (if (R,S) \<in> irreg_pairs \<union> low_density_pairs \<union> small_pairs then 0
              else edge_density X Y G)" 
           if "X \<subseteq> R" "Y \<subseteq> S" for X Y
           using all_edges_if that ij False by (smt (verit) all_edges_preserved edge_density_eq0 
 edge_density_def) 
         show ?thesis
           using that False \<open>\<epsilon> > 0\<close>
           by (auto simp add: irreg_pairs_def regular_pair_def less_le ed)
       next
         case True
         then have ed: "edge_density X Y Gnew = 0"  if "X \<subseteq> R" "Y \<subseteq> S" for X Y
           by (meson edge_density_eq0 all_edges_if that \<open>R \<in> P\<close> \<open>S \<in> P\<close> UnCI)
         with egt that show ?thesis
           by (auto simp: regular_pair_def ed)
       qed
       then have reg_pairs: "regular_graph P Gnew (\<epsilon>/4)"
         by (meson regular_graph_def)
 
       have "edge_dense R S Gnew (\<epsilon>/2)" 
         if "R \<in> P" "S \<in> P" for R S
       proof (cases "(R,S) \<in> low_density_pairs")
         case False
         have ed: "edge_density R S Gnew =
             (if (R,S) \<in> irreg_pairs \<union> low_density_pairs \<union> small_pairs then 0
              else edge_density R S G)" 
           using all_edges_if that that by (simp add: edge_density_def)
         with that \<open>\<epsilon> > 0\<close> False show ?thesis
           by (auto simp: low_density_pairs_def edge_dense_def all_edges_if)
       next
         case True
         then have "edge_density R S Gnew = 0" 
           by (simp add: all_edges_if edge_density_def that)
         with \<open>\<epsilon> > 0\<close> that show ?thesis
           by (simp add: True all_edges_if edge_dense_def)
       qed
       then have density_bound: "dense_graph P Gnew (\<epsilon>/2)"
         by (meson dense_graph_def)
 
       have min_subset_size: "decent_graph P Gnew (?e4M * ?n)"
         using \<open>\<epsilon> > 0\<close> 
         by (auto simp: decent_graph_def small_pairs_def small_def decent_def all_edges_if)
       show "triangle_free_graph Gnew"
       proof (rule ccontr) 
         assume non: "\<not>?thesis"
         then obtain x y z where trig_ex: "triangle_in_graph x y z Gnew" 
           using triangle_free_graph_def non by auto
         then have xin: "x \<in> (uverts Gnew)" and yin: "y \<in> (uverts Gnew)" and zin: "z \<in> (uverts Gnew)" 
           using triangle_in_graph_verts new_wf by auto
         then obtain R S T where xinp: "x \<in> R" and ilt: "R\<in>P" and yinp: "y \<in> S" and jlt: "S\<in>P"
                           and zinp: "z \<in> T" and klt: "T\<in>P" 
           by (metis graph_partition_new xin Union_iff finite_graph_partition_equals)
         then have finitesubsets: "finite R" "finite S" "finite T"
           using new_fin fin_part finite_graph_partition_finite fin by auto
         have subsets: "R \<subseteq> uverts Gnew" "S \<subseteq> uverts Gnew" "T \<subseteq> uverts Gnew" 
           using finite_graph_partition_subset ilt jlt klt graph_partition_new by auto
         have min_sizes: "card R \<ge> ?e4M*?n" "card S \<ge> ?e4M*?n" "card T \<ge> ?e4M*?n"
           using trig_ex min_subset_size xinp yinp zinp ilt jlt klt
           by (auto simp: triangle_in_graph_def decent_graph_def decent_def all_edges_between_def)
         have min_dens: "edge_density R S Gnew \<ge> \<epsilon>/2" "edge_density R T Gnew \<ge> \<epsilon>/2" 
 "edge_density S T Gnew \<ge> \<epsilon>/2" 
           using density_bound subsets ilt jlt klt xinp yinp zinp unfolding dense_graph_def edge_dense_def
           by (metis all_edges_betw_I equals0D triangle_in_graph_def trig_ex)+
         then have min_dens_diff: 
           "edge_density R S Gnew - \<epsilon>/4 \<ge> \<epsilon>/4" "edge_density R T Gnew - \<epsilon>/4 \<ge> \<epsilon>/4" 
 "edge_density S T Gnew - \<epsilon>/4 \<ge> \<epsilon>/4" 
           by auto
-        have mincard0: "(card R)*(card S)* (card T) \<ge> 0" by simp
+        have mincard0: "(card R)*(card S) * (card T) \<ge> 0" by simp
         have gtcube: "((edge_density R S Gnew) - \<epsilon>/4)*((edge_density R T Gnew) - \<epsilon>/4) *((edge_density S T Gnew) - \<epsilon>/4) \<ge> (\<epsilon>/4)^3"
           using min_dens_diff e4gt real_mult_gt_cube by auto 
         then have c1: "((edge_density R S Gnew) - \<epsilon>/4)*((edge_density R T Gnew) - \<epsilon>/4) *((edge_density S T Gnew) - \<epsilon>/4) \<ge> 0"
           by (smt (verit) e4gt zero_less_power) 
         have "?e4M * ?n \<ge> 0"
           using egt by force
         then have "card R * card S * card T \<ge> (?e4M * ?n)*(?e4M * ?n) * (?e4M * ?n)" 
           by (metis (no_types) of_nat_0_le_iff of_nat_mult min_sizes mult_mono)
-        then have "(card R)*(card S)* (card T) \<ge> (?e4M* ?n)^3"
+        then have "(card R)*(card S) * (card T) \<ge> (?e4M* ?n)^3"
           by (simp add: power3_eq_cube) 
         then have cardgtbound:"card R * card S * card T \<ge> ?e4M^ 3 * ?n^3"
           by (metis of_nat_power power_mult_distrib)
 
         have "(1-\<epsilon>/2) * (\<epsilon>/4)^3 * (\<epsilon>/(4*M))^3 * ?n^3 \<le> (1-\<epsilon>/2) * (\<epsilon>/4)^3 * card R * card S * card T"
           using cardgtbound ordered_comm_semiring_class.comm_mult_left_mono True e4gt by fastforce
         also have "... \<le> (1-2*(\<epsilon>/4)) * (edge_density R S Gnew - \<epsilon>/4)*(edge_density R T Gnew - \<epsilon>/4) * (edge_density S T Gnew - \<epsilon>/4) * card R * card S * card T"
           using gtcube c1 \<open>\<epsilon> < 1\<close> mincard0 by (simp add: mult.commute mult.left_commute mult_left_mono)
         also have "... \<le> card (triangle_triples R S T Gnew)"
           by (smt (verit, best) e4gt ilt jlt klt min_dens_diff new_fin new_wf rp
  subsets triangle_counting_lemma)
         finally have "card (triangle_set Gnew) \<ge> D * ?n^3"
           using card_convert_triangle_rep_bound new_wf new_fin subsets 
           by (auto simp: triangle_triples_def D_def)
         then have g_tset_bound: "card (triangle_set G) \<ge> D * ?n^3" 
           using triangle_set_graph_edge_ss_bound by (smt (verit) edges fin local.wf of_nat_mono verts)
         have "card (triangle_set G) > \<delta> * ?n^3" 
         proof -
           have "?n^3 > 0"
             by (simp add: \<open>uverts G \<noteq> {}\<close> card_gt_0_iff fin)
           with \<delta> \<open>D0 \<le> D\<close> have "D * ?n^3 > \<delta> * ?n^3"
             by force
           thus "card (triangle_set G) > \<delta> * ?n ^3" 
             using g_tset_bound unfolding D_def by linarith 
         qed
         thus False
           using ineq by linarith
       qed
       show "real (card (uedges G - uedges Gnew)) \<le> \<epsilon> * real ((card (uverts G))\<^sup>2)"
         using cardbound edges verts by blast 
     qed
   qed (rule \<open>0 < \<delta>\<close>)
 qed
 
 subsection \<open>Roth's Theorem\<close>
 
 text\<open>We will first need the following corollary of the Triangle Removal Lemma.
 This is Corollary 3.18 in Zhao's notes:\<close>
 
-corollary corollary_triangle_removal:
+text \<open>See \<^url>\<open>https://en.wikipedia.org/wiki/Ruzsa–Szemerédi_problem#Upper_bound\<close>.
+Suggested by Yaël Dillies
+\<close>
+corollary ruzsa_szemeredi_upper_bound:
   fixes \<epsilon> :: real 
   assumes "0 < \<epsilon>"
   shows "\<exists>N>0. \<forall>G. card(uverts G) > N \<longrightarrow> uwellformed G \<longrightarrow> unique_triangles G \<longrightarrow>
           card (uedges G) \<le> \<epsilon> * (card (uverts G))\<^sup>2"
 proof -
   have "\<epsilon>/3 > 0"
     using assms by auto
   then obtain \<delta>::real where "\<delta> > 0"
     and \<delta>: "\<And>G. \<lbrakk>card(uverts G) > 0; uwellformed G;
           card (triangle_set G) \<le> \<delta> * card(uverts G) ^ 3\<rbrakk> \<Longrightarrow>
           (\<exists>Gnew. triangle_free_graph Gnew \<and> uverts Gnew = uverts G \<and> (uedges Gnew \<subseteq> uedges G) \<and> 
           card (uedges G - uedges Gnew) \<le> \<epsilon>/3 * (card (uverts G))\<^sup>2)"
     using triangle_removal_lemma by metis
   obtain N::nat where N: "real N \<ge> 1 / (3*\<delta>)"
     by (meson real_arch_simple)
   show ?thesis
   proof (intro exI conjI strip)
     show "N > 0"
       using N \<open>0 < \<delta>\<close> zero_less_iff_neq_zero by fastforce
     fix G 
     let ?n = "card (uverts G)"
     assume G_gt_N: "N < ?n"
       and wf: "uwellformed G"
       and uniq: "unique_triangles G"
     have G_ne: "?n > 0"
       using G_gt_N by linarith
     obtain TF where TF: "\<And>e. e \<in> uedges G \<Longrightarrow> \<exists>x y z. TF e = {x,y,z} \<and> triangle_in_graph x y z G \<and> e \<subseteq> TF e"
       using uniq unfolding unique_triangles_def by metis
     let ?TWO = "(\<lambda>t. [t]\<^bsup>2\<^esup>)"
     have tri_nsets_2: "[{x,y,z}]\<^bsup>2\<^esup> = {{x,y},{y,z},{x,z}}" if "triangle_in_graph x y z G" for x y z
       using that unfolding nsets_def triangle_in_graph_def card_2_iff doubleton_eq_iff
       by (blast dest!: edge_vertices_not_equal [OF wf])
     have tri_nsets_3: "{{x,y},{y,z},{x,z}} \<in> [uedges G]\<^bsup>3\<^esup>" if "triangle_in_graph x y z G" for x y z
       using that 
       by (simp add: nsets_def card_3_iff triangle_in_graph_def) (metis doubleton_eq_iff 
 edge_vertices_not_equal [OF wf])
     have sub: "?TWO ` triangle_set G \<subseteq> [uedges G]\<^bsup>3\<^esup>"
       using tri_nsets_2 tri_nsets_3 triangle_set_def by auto
     have "\<And>i. i \<in> triangle_set G \<Longrightarrow> ?TWO i \<noteq> {}"
       using tri_nsets_2 triangle_set_def by auto
     moreover have dfam: "disjoint_family_on ?TWO (triangle_set G)"
       using sub [unfolded image_subset_iff] uniq
       unfolding disjoint_family_on_def triangle_set_def nsets_def unique_triangles_def
       by (smt (verit) disjoint_iff_not_equal insert_subset mem_Collect_eq mk_disjoint_insert )  
     ultimately have inj: "inj_on ?TWO (triangle_set G)"
       by (simp add: disjoint_family_on_iff_disjoint_image)
     have \<section>: "\<exists>T\<in>triangle_set G. e \<in> [T]\<^bsup>2\<^esup>" if "e \<in> uedges G" for e
       using uniq [unfolded unique_triangles_def] that local.wf
       apply (simp add: triangle_set_def triangle_in_graph_def nsets_def uwellformed_def)
       by (metis (mono_tags, lifting) finite.emptyI finite.insertI finite_subset)
     with sub have "\<Union>(?TWO ` triangle_set G) = uedges G"
       by (auto simp: image_subset_iff nsets_def)
     then have "card (\<Union>(?TWO ` triangle_set G)) = card (uedges G)"
       by simp
     moreover have "card (\<Union>(?TWO ` triangle_set G)) = 3 * card (triangle_set G)"
     proof (subst card_UN_disjoint' [OF dfam])
       show "finite ([i]\<^bsup>2\<^esup>)" if "i \<in> triangle_set G" for i 
         using that tri_nsets_2 triangle_set_def by fastforce
       show "finite (triangle_set G)"
         by (meson G_ne card_gt_0_iff local.wf finite_triangle_set)
       have "card ([i]\<^bsup>2\<^esup>) = 3" if "i \<in> triangle_set G" for i
         using that wf nsets_def tri_nsets_2 tri_nsets_3 triangle_set_def by fastforce
       then show "(\<Sum>i\<in>triangle_set G. card ([i]\<^bsup>2\<^esup>)) = 3 * card (triangle_set G)"
         by simp
     qed
     ultimately have A: "3 * card (triangle_set G) = card (uedges G)" 
       by auto
     have "card (uedges G) \<le> card (all_edges(uverts G))"
       by (meson G_ne all_edges_finite card_gt_0_iff card_mono local.wf wellformed_all_edges)
     also have "\<dots> = card (uverts G) choose 2"
       by (metis G_ne card_all_edges card_eq_0_iff not_less0)
     also have "\<dots> = card (uverts G) * (card (uverts G) - 1) div 2"
       by (meson n_choose_2_nat) 
     also have "\<dots> < (card (uverts G))\<^sup>2"
       by (simp add: G_ne less_imp_diff_less less_mult_imp_div_less power2_eq_square)
     finally have B: "card (uedges G) < (card (uverts G))\<^sup>2" .
 
     have "card (triangle_set G) \<le> (card (uverts G))\<^sup>2 / 3"
       using A B by linarith
     also have "\<dots> \<le> \<delta> * card(uverts G) ^ 3"
     proof -
       have "1 \<le> 3 * \<delta> * N"
         using N \<open>\<delta> > 0\<close> by (simp add: field_simps)
       also have "\<dots> \<le> 3 * \<delta> * ?n"
         using G_gt_N \<open>0 < \<delta>\<close> by force
       finally have "1 * ?n^2 \<le> (3 * \<delta> * ?n) * ?n^2"
         by (simp add: G_ne)
       then show ?thesis
         by (simp add: eval_nat_numeral mult_ac)
     qed
     finally have "card (triangle_set G) \<le> \<delta> * ?n ^ 3" .
     then obtain Gnew where Gnew: "triangle_free_graph Gnew" "uverts Gnew = uverts G" 
       "uedges Gnew \<subseteq> uedges G" and card_edge_diff: "card (uedges G - uedges Gnew) \<le> \<epsilon>/3 * ?n\<^sup>2"
       using G_ne \<delta> local.wf by meson
     
     text\<open>Deleting an edge removes at most one triangle from the graph by assumption,
          so the number of edges removed in this process is at least the number of triangles.\<close>
     
     have False
       if non: "\<And>e. e \<in> uedges G - uedges Gnew \<Longrightarrow> {x,y,z} \<noteq> TF e"
         and tri: "triangle_in_graph x y z G" for x y z
     proof -
       have "\<not> triangle_in_graph x y z Gnew"
         using Gnew triangle_free_graph_def by blast
       with tri obtain e where eG: "e \<in> uedges G - uedges Gnew" and esub: "e \<subseteq> {x,y,z}"
         using insert_commute triangle_in_graph_def by auto
       then show False
         by (metis DiffD1 TF tri uniq unique_triangles_def non [OF eG])
     qed
     then have "triangle_set G \<subseteq> TF ` (uedges G - uedges Gnew)"
       unfolding triangle_set_def by blast
     moreover have "finite (uedges G - uedges Gnew)"
       by (meson G_ne card_gt_0_iff finite_Diff finite_graph_def wf wellformed_finite)
     ultimately have "card (triangle_set G) \<le> card (uedges G - uedges Gnew)"
       by (meson surj_card_le)
     then show "card (uedges G) \<le> \<epsilon> * ?n\<^sup>2"
       using A card_edge_diff by linarith
   qed
 qed
 
 text\<open>We are now ready to proceed to the proof of Roth's Theorem for Arithmetic Progressions. \<close>
 
 definition progression3 :: "'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a set"
   where "progression3 k d \<equiv> {k, k+d, k+d+d}"
 
 lemma p3_int_iff: "progression3 (int k) (int d) \<subseteq> int ` A \<longleftrightarrow> progression3 k d \<subseteq> A"
   apply (simp add: progression3_def image_iff)
   by (smt (verit, best) int_plus of_nat_eq_iff)
 
 text\<open>We assume that a set of naturals $A \subseteq \{...<N \}$ does not have any arithmetic progression. 
 We will then show that @{term A} is of cardinality $o(N)$.\<close>
 
 lemma RothArithmeticProgressions_aux:
   fixes \<epsilon>::real
   assumes "\<epsilon> > 0"
   obtains X where "\<forall>N \<ge> X. \<forall>A \<subseteq> {..<N}. (\<nexists>k d. d>0 \<and> progression3 k d \<subseteq> A) \<longrightarrow> card A < \<epsilon> * real N"
 proof -
   obtain X where "X>0"
     and X: "\<And>G. \<lbrakk>card(uverts G) > X; uwellformed G; unique_triangles G\<rbrakk> 
                 \<Longrightarrow> card (uedges G) \<le> \<epsilon>/12 * (card (uverts G))\<^sup>2"
-    by (metis assms corollary_triangle_removal less_divide_eq_numeral1(1) mult_eq_0_iff)
+    by (metis assms ruzsa_szemeredi_upper_bound less_divide_eq_numeral1(1) mult_eq_0_iff)
   show thesis
   proof (intro strip that)
     fix N A
     assume "X \<le> N" and A: "A \<subseteq> {..<N}"
       and non: "\<nexists>k d. 0 < d \<and> progression3 k d \<subseteq> A"
     then have "N > 0" using \<open>0 < X\<close> by linarith
     define M where "M \<equiv> Suc (2*N)"
     have M_mod_bound[simp]: "x mod M < M" for x
       by (simp add: M_def)
     have "odd M" "M>0" "N<M" by (auto simp: M_def)
     have "coprime M (Suc N)"
       unfolding M_def
       by (metis add.commute coprime_Suc_right_nat coprime_mult_right_iff mult_2 nat_arith.suc1)
     then have cop: "coprime M (1 + int N)"
       by (metis coprime_int_iff of_nat_Suc)
     have A_sub_M: "int ` A \<subseteq> {..<M}"
       using A by (force simp: M_def)
     have non_img_A: "\<nexists>k d. d > 0 \<and> progression3 k d \<subseteq> int ` A"
       by (metis p3_int_iff non pos_int_cases zero_le_imp_eq_int imageE insert_subset of_nat_0_le_iff 
 progression3_def)
     
     text\<open>Construct a tripartite graph @{term G} whose three parts are copies of @{text"\<int>/M\<int>"}.\<close>
     
     define part_of where "part_of \<equiv> \<lambda>\<xi>. (\<lambda>i. prod_encode (\<xi>,i)) ` {..<M}"
     define label_of_part where "label_of_part \<equiv> \<lambda>p. fst (prod_decode p)"
     define from_part where "from_part \<equiv> \<lambda>p. snd (prod_decode p)"
     have enc_iff [simp]: "prod_encode (a,i) \<in> part_of a' \<longleftrightarrow> a'=a \<and> i<M" for a a' i
       using \<open>0 < M\<close> by (clarsimp simp: part_of_def image_iff Bex_def) presburger
     have part_of_M: "p \<in> part_of a \<Longrightarrow> from_part p < M" for a p
       using from_part_def part_of_def by fastforce
     have disjnt_part_of: "a \<noteq> b \<Longrightarrow> disjnt (part_of a) (part_of b)" for a b
       by (auto simp: part_of_def disjnt_iff)
     have from_enc [simp]: "from_part (prod_encode (a,i)) = i" for a i
       by (simp add: from_part_def)
     have finpart [iff]: "finite (part_of a)" for a
       by (simp add: part_of_def \<open>0 < M\<close>)
     have cardpart [simp]: "card (part_of a) = M" for a
       using \<open>0 < M\<close>
       by (simp add: part_of_def eq_nat_nat_iff inj_on_def card_image)
     let ?X = "part_of 0"
     let ?Y = "part_of (Suc 0)"
     let ?Z = "part_of (Suc (Suc 0))"
     define diff where "diff \<equiv> \<lambda>a b. (int a - int b) mod (int M)"
     have inj_on_diff: "inj_on (\<lambda>x. diff x a) {..<M}" for a
       apply (clarsimp simp: diff_def inj_on_def)
       by (metis diff_add_cancel mod_add_left_eq mod_less nat_int of_nat_mod)
     have eq_mod_M: "(x - y) mod int M = (x' - y) mod int M \<Longrightarrow> x mod int M = x' mod int M" for x x' y
       by (simp add: mod_eq_dvd_iff)
 
     have diff_invert: "diff y x = int a \<longleftrightarrow> y = (x + a) mod M" if "y < M" "a\<in>A" for x y a
     proof -
       have "a < M"
         using A \<open>N < M\<close> that by auto
       show ?thesis
       proof
         assume "diff y x = int a"
         with that \<open>a<M\<close> have "int y = int (x+a) mod int M"
           unfolding diff_def by (smt (verit, ccfv_SIG) eq_mod_M mod_less of_nat_add zmod_int)
         with that show "y = (x + a) mod M"
           by (metis nat_int zmod_int)
       qed (simp add: \<open>a < M\<close> diff_def mod_diff_left_eq zmod_int)
     qed
 
     define diff2 where "diff2 \<equiv> \<lambda>a b. ((int a - int b) * int(Suc N)) mod (int M)"
     have inj_on_diff2: "inj_on (\<lambda>x. diff2 x a) {..<M}" for a
       apply (clarsimp simp: diff2_def inj_on_def)
       by (metis eq_mod_M mult_mod_cancel_right [OF _ cop] int_int_eq mod_less zmod_int)
     have [simp]: "(1 + int N) mod int M = 1 + int N"
       using M_def \<open>0 < N\<close> by auto
     have diff2_by2: "(diff2 a b * 2) mod M = diff a b" for a b
     proof -
       have "int M dvd ((int a - int b) * int M)"
         by simp
       then have "int M dvd ((int a - int b) * int (Suc N) * 2 - (int a - int b))"
         by (auto simp: M_def algebra_simps)
       then show ?thesis
         by (metis diff2_def diff_def mod_eq_dvd_iff mod_mult_left_eq)
     qed
     have diff2_invert: "diff2 (((x + a) mod M + a) mod M) x = int a" if "a\<in>A" for x a
     proof -
       have 1: "((x + a) mod M + a) mod M = (x + 2*a) mod M"
         by (metis group_cancel.add1 mod_add_left_eq mult_2)
       have "(int ((x + 2*a) mod M) - int x) * (1 + int N) mod int M 
              = (int (x + 2*a) - int x) * (1 + int N) mod int M"
         by (metis mod_diff_left_eq mod_mult_cong of_nat_mod)
       also have "\<dots> = int (a * (Suc M)) mod int M"
         by (simp add: algebra_simps M_def)
       also have "\<dots> = int a mod int M"
         by simp
       also have "\<dots> = int a"
         using A M_def subsetD that by auto
       finally show ?thesis
         using that by (auto simp: 1 diff2_def)
     qed
 
     define Edges where "Edges \<equiv> \<lambda>X Y df. {{x,y}| x y. x \<in> X \<and> y \<in> Y \<and> df(from_part y) (from_part x) \<in> int ` A}"
     have Edges_subset: "Edges X Y df \<subseteq> Pow (X \<union> Y)" for X Y df
       by (auto simp: Edges_def)
     define XY where "XY \<equiv> Edges ?X ?Y diff"
     define YZ where "YZ \<equiv> Edges ?Y ?Z diff"
     define XZ where "XZ \<equiv> Edges ?X ?Z diff2"
     obtain [simp]: "finite XY" "finite YZ" "finite XZ"
       using Edges_subset unfolding XY_def YZ_def XZ_def
       by (metis finite_Pow_iff finite_UnI finite_subset finpart)
     define G where "G \<equiv> (?X \<union> ?Y \<union> ?Z, XY \<union> YZ \<union> XZ)"
     have finG: "finite (uverts G)" and cardG: "card (uverts G) = 3*M"
       by (simp_all add: G_def card_Un_disjnt disjnt_part_of)
     then have "card(uverts G) > X"
       using M_def \<open>X \<le> N\<close> by linarith 
     have "uwellformed G"
       by (fastforce simp: card_insert_if part_of_def G_def XY_def YZ_def XZ_def Edges_def uwellformed_def)
     have [simp]: "{prod_encode (\<xi>,x), prod_encode (\<xi>,y)} \<notin> XY"  
                  "{prod_encode (\<xi>,x), prod_encode (\<xi>,y)} \<notin> YZ"
                  "{prod_encode (\<xi>,x), prod_encode (\<xi>,y)} \<notin> XZ" for x y \<xi>
       by (auto simp: XY_def YZ_def XZ_def Edges_def doubleton_eq_iff)
     have label_ne_XY [simp]: "label_of_part p \<noteq> label_of_part q" if "{p,q} \<in> XY" for p q
       using that by (auto simp add: XY_def part_of_def Edges_def doubleton_eq_iff label_of_part_def)
     then have [simp]: "{p} \<notin> XY" for p
       by (metis insert_absorb2)
     have label_ne_YZ [simp]: "label_of_part p \<noteq> label_of_part q" if "{p,q} \<in> YZ" for p q
       using that by (auto simp add: YZ_def part_of_def Edges_def doubleton_eq_iff label_of_part_def)
     then have [simp]: "{p} \<notin> YZ" for p
       by (metis insert_absorb2)
     have label_ne_XZ [simp]: "label_of_part p \<noteq> label_of_part q" if "{p,q} \<in> XZ" for p q
       using that by (auto simp add: XZ_def part_of_def Edges_def doubleton_eq_iff label_of_part_def)
     then have [simp]: "{p} \<notin> XZ" for p
       by (metis insert_absorb2)
     have label012: "label_of_part v < 3" if "v \<in> uverts G" for v
       using that by (auto simp add: G_def eval_nat_numeral part_of_def label_of_part_def)
 
     have Edges_distinct: "\<And>p q r \<xi> \<zeta> \<gamma> \<beta> df df'. \<lbrakk>{p,q} \<in> Edges (part_of \<xi>) (part_of \<zeta>) df;
            {q,r} \<in> Edges (part_of \<xi>) (part_of \<zeta>) df;
            {p,r} \<in> Edges (part_of \<gamma>) (part_of \<beta>) df'; \<xi> \<noteq> \<zeta>; \<gamma> \<noteq> \<beta>\<rbrakk> \<Longrightarrow> False"
       apply (auto simp: disjnt_iff Edges_def doubleton_eq_iff conj_disj_distribR ex_disj_distrib)
       apply (metis disjnt_iff disjnt_part_of)+
       done
     have uniq: "\<exists>i<M. \<exists>d\<in>A. \<exists>x \<in> {p,q,r}. \<exists>y \<in> {p,q,r}. \<exists>z \<in> {p,q,r}. 
                    x = prod_encode(0, i)
                  \<and> y = prod_encode(1, (i+d) mod M)
                  \<and> z = prod_encode(2, (i+d+d) mod M)"
       if T: "triangle_in_graph p q r G" for p q r
     proof -
       obtain x y z where xy: "{x,y} \<in> XY" and yz: "{y,z} \<in> YZ" and xz: "{x,z} \<in> XZ"
         and x: "x \<in> {p,q,r}" and y: "y \<in> {p,q,r}" and z: "z \<in> {p,q,r}"
         using T apply (simp add: triangle_in_graph_def G_def XY_def YZ_def XZ_def)
         by (smt (verit, ccfv_SIG) Edges_distinct Zero_not_Suc insert_commute n_not_Suc_n)
       then have "x \<in> ?X" "y \<in> ?Y" "z \<in> ?Z"
         by (auto simp: XY_def YZ_def XZ_def Edges_def doubleton_eq_iff; metis disjnt_iff disjnt_part_of)+
       then obtain i j k where i: "x = prod_encode(0,i)" and j: "y = prod_encode(1,j)" 
 and k: "z = prod_encode(2,k)"
         by (metis One_nat_def Suc_1 enc_iff prod_decode_aux.cases prod_decode_inverse)
       obtain a1 where "a1 \<in> A" and a1: "(int j - int i) mod int M = int a1"
         using xy \<open>x \<in> ?X\<close> i j by (auto simp add: XY_def Edges_def doubleton_eq_iff diff_def)
       obtain a3 where "a3 \<in> A" and a3: "(int k - int j) mod int M = int a3"
         using yz \<open>x \<in> ?X\<close> j k by (auto simp add: YZ_def Edges_def doubleton_eq_iff diff_def)
       obtain a2 where "a2 \<in> A" and a2: "(int k - int i) mod int M = int (a2 * 2) mod int M"
         using xz \<open>x \<in> ?X\<close> i k apply (auto simp add: XZ_def Edges_def doubleton_eq_iff)
         by (metis diff2_by2 diff_def int_plus mult_2_right)
       obtain "a1<N" "a2<N" "a3<N"
         using A \<open>a1 \<in> A\<close> \<open>a2 \<in> A\<close> \<open>a3 \<in> A\<close> by blast
       then obtain "a1+a3 < M" "a2 * 2 < M"
         by (simp add: M_def)
       then have "int (a2 * 2) = int (a2 * 2) mod M"
         by force
       also have "\<dots> = int (a1 + a3) mod int M"
         using a1 a2 a3 by (smt (verit, del_insts) int_plus mod_add_eq)
       also have "\<dots> = int (a1+a3)"
         using \<open>a1 + a3 < M\<close> by force
       finally have "a2*2 = a1+a3"
         by presburger
       then obtain equal: "a3 - a2 = a2 - a1" "a2 - a3 = a1 - a2"
         by (metis Nat.diff_cancel diff_cancel2 mult_2_right)
       with \<open>a1 \<in> A\<close> \<open>a2 \<in> A\<close> \<open>a3 \<in> A\<close> have "progression3 a1 (a2 - a1) \<subseteq> A"
         apply (clarsimp simp: progression3_def)
         by (metis diff_is_0_eq' le_add_diff_inverse nle_le)
       with non equal have "a2 = a1"
         unfolding progression3_def
         by (metis \<open>a2 \<in> A\<close> \<open>a3 \<in> A\<close> add.right_neutral diff_is_0_eq insert_subset 
 le_add_diff_inverse not_gr_zero)
       then have "a3 = a2"
         using \<open>a2 * 2 = a1 + a3\<close> by force
       have k_minus_j: "(int k - int j) mod int M = int a1"
         by (simp add: \<open>a2 = a1\<close> \<open>a3 = a2\<close> a3)
       have i_to_j: "j mod M = (i+a1) mod M"
         by (metis a1 add_diff_cancel_left' add_diff_eq mod_add_right_eq nat_int of_nat_add of_nat_mod)
       have j_to_k: "k mod M = (j+a1) mod M"
         by (metis \<open>a2 = a1\<close> \<open>a3 = a2\<close> a3 add_diff_cancel_left' add_diff_eq mod_add_right_eq 
 nat_int of_nat_add of_nat_mod)
       have "i<M"
         using \<open>x \<in> ?X\<close> i by simp
       then show ?thesis
         using i j k x y z \<open>a1 \<in> A\<close>
         by (metis \<open>y \<in> ?Y\<close> \<open>z \<in>?Z\<close> enc_iff i_to_j j_to_k mod_add_left_eq mod_less)
     qed
     
     text\<open>Every edge of the graph G lies in exactly one triangle.\<close>
     
 have "unique_triangles G"
       unfolding unique_triangles_def
     proof (intro strip)
       fix e
       assume "e \<in> uedges G"
       then consider "e \<in> XY" | "e \<in> YZ" | "e \<in> XZ"
         using G_def by fastforce
       then show "\<exists>!T. \<exists>x y z. T = {x, y, z} \<and> triangle_in_graph x y z G \<and> e \<subseteq> T"
       proof cases
         case 1
         then obtain i j a where eeq: "e = {prod_encode(0,i), prod_encode(1,j)}"
           and "i<M" and "j<M"
           and df: "diff j i = int a" and "a \<in> A"
           by (auto simp: XY_def Edges_def part_of_def)
         let ?x = "prod_encode (0, i)"
         let ?y = "prod_encode (1, j)"
         let ?z = "prod_encode (2, (j+a) mod M)"
         have yeq: "j = (i+a) mod M"
           using diff_invert using \<open>a \<in> A\<close> df \<open>j<M\<close> by blast
         with \<open>a \<in> A\<close> \<open>j<M\<close> have "{?y,?z} \<in> YZ"
           by (fastforce simp: YZ_def Edges_def image_iff diff_invert)
         moreover have "{?x,?z} \<in> XZ"
           using \<open>a \<in> A\<close> by (fastforce simp: XZ_def Edges_def yeq diff2_invert \<open>i<M\<close>)
         ultimately have T: "triangle_in_graph ?x ?y ?z G"
           using \<open>e \<in> uedges G\<close> by (force simp add: G_def eeq triangle_in_graph_def)
         show ?thesis
         proof (intro ex1I)
           show "\<exists>x y z. {?x,?y,?z} = {x, y, z} \<and> triangle_in_graph x y z G \<and> e \<subseteq> {?x,?y,?z}"
             using T eeq by blast
           fix T
           assume "\<exists>p q r. T = {p, q, r} \<and> triangle_in_graph p q r G \<and> e \<subseteq> T"
           then obtain p q r where Teq: "T = {p,q,r}"
             and tri: "triangle_in_graph p q r G" and "e \<subseteq> T"
             by blast
           with uniq
           obtain i' a' x y z where "i'<M" "a' \<in> A"  
                  and x: "x \<in> {p,q,r}" and y: "y \<in> {p,q,r}" and z: "z \<in> {p,q,r}"
                  and xeq: "x = prod_encode(0, i')"
                  and yeq: "y = prod_encode(1, (i'+a') mod M)"
                  and zeq: "z = prod_encode(2, (i'+a'+a') mod M)"
             by metis
           then have sets_eq: "{x,y,z} = {p,q,r}" by auto
           with Teq \<open>e \<subseteq> T\<close> have esub': "e \<subseteq> {x,y,z}" by blast
           have "a' < M"
             using A \<open>N < M\<close> \<open>a' \<in> A\<close> by auto
           obtain "?x \<in> e" "?y \<in> e" using eeq by force
           then have "x = ?x"
             using esub' eeq yeq zeq by simp
           then have "y = ?y"
             using esub' eeq zeq by simp
           obtain eq': "i' = i" "(i'+a') mod M = j"
             using \<open>x = ?x\<close> xeq using \<open>y =?y\<close> yeq by auto
           then have "diff (i'+a') i' = int a'"
             by (simp add: diff_def \<open>a' < M\<close>)
           then have "a' = a"
             by (metis eq' df diff_def mod_diff_left_eq nat_int zmod_int)
           then have "z = ?z"
             by (metis \<open>y = ?y\<close> mod_add_left_eq prod_encode_eq snd_conv yeq zeq)
           then show "T = {?x,?y,?z}"
             using Teq \<open>x = ?x\<close> \<open>y = ?y\<close> sets_eq by presburger
         qed
       next
         case 2
         then obtain j k a where eeq: "e = {prod_encode(1,j), prod_encode(2,k)}"
           and "j<M" "k<M"
           and df: "diff k j = int a" and "a \<in> A"
           by (auto simp: YZ_def Edges_def part_of_def numeral_2_eq_2)
         let ?x = "prod_encode (0, (M+j-a) mod M)"
         let ?y = "prod_encode (1, j)"
         let ?z = "prod_encode (2, k)"
         have zeq: "k = (j+a) mod M"
           using diff_invert using \<open>a \<in> A\<close> df \<open>k<M\<close> by blast
         with \<open>a \<in> A\<close> \<open>k<M\<close> have "{?x,?z} \<in> XZ"
           unfolding XZ_def Edges_def image_iff
           apply (clarsimp simp: mod_add_left_eq doubleton_eq_iff conj_disj_distribR ex_disj_distrib)
           apply (smt (verit, ccfv_threshold) A \<open>N < M\<close> diff2_invert le_add_diff_inverse2 lessThan_iff 
 linorder_not_less mod_add_left_eq 
                      mod_add_self1 not_add_less1 order.strict_trans subsetD)
           done
         moreover 
         have "a < N" using A \<open>a \<in> A\<close> by blast
         with \<open>N < M\<close> have "((M + j - a) mod M + a) mod M = j mod M"
           by (simp add: mod_add_left_eq)
         then have "{?x,?y} \<in> XY"
           using \<open>a \<in> A\<close> \<open>j<M\<close>
           by (force simp add: XY_def Edges_def zeq image_iff diff_invert 
 doubleton_eq_iff ex_disj_distrib)
         ultimately have T: "triangle_in_graph ?x ?y ?z G"
           using \<open>e \<in> uedges G\<close> by (auto simp: G_def eeq triangle_in_graph_def)
         show ?thesis
         proof (intro ex1I)
           show "\<exists>x y z. {?x,?y,?z} = {x, y, z} \<and> triangle_in_graph x y z G \<and> e \<subseteq> {?x,?y,?z}"
             using T eeq by blast
           fix T
           assume "\<exists>p q r. T = {p, q, r} \<and> triangle_in_graph p q r G \<and> e \<subseteq> T"
           then obtain p q r where Teq: "T = {p,q,r}" and tri: "triangle_in_graph p q r G" and "e \<subseteq> T"
             by blast
           with uniq
           obtain i' a' x y z where "i'<M" "a' \<in> A"  
                  and x: "x \<in> {p,q,r}" and y: "y \<in> {p,q,r}" and z: "z \<in> {p,q,r}"
                  and xeq: "x = prod_encode(0, i')"
                  and yeq: "y = prod_encode(1, (i'+a') mod M)"
                  and zeq: "z = prod_encode(2, (i'+a'+a') mod M)"
             by metis
           then have sets_eq: "{x,y,z} = {p,q,r}" by auto
           with Teq \<open>e \<subseteq> T\<close> have esub': "e \<subseteq> {x,y,z}" by blast
           have "a' < M"
             using A \<open>N < M\<close> \<open>a' \<in> A\<close> by auto
           obtain "?y \<in> e" "?z \<in> e"
             using eeq by force
           then have "y = ?y"
             using esub' eeq xeq zeq by simp
           then have "z = ?z"
             using esub' eeq xeq by simp
           obtain eq': "(i'+a') mod M = j" "(i'+a'+a') mod M = k"
             using \<open>y = ?y\<close> yeq using \<open>z =?z\<close> zeq by auto
           then have "diff (i'+a'+a') (i'+a') = int a'"
             by (simp add: diff_def \<open>a' < M\<close>)
           then have "a' = a"
             by (metis M_mod_bound \<open>a' \<in> A\<close> df diff_invert eq' mod_add_eq mod_if of_nat_eq_iff)
           have "(M + ((i'+a') mod M) - a') mod M = i'"
             by (metis Nat.add_diff_assoc2 \<open>a' < M\<close> \<open>i' < M\<close> add.left_commute add_implies_diff 
 less_imp_le_nat mod_add_right_eq mod_add_self2 mod_less)
           with \<open>a' = a\<close> eq' have "(M + j - a) mod M = i'"
             by force
           with xeq have "x = ?x" by blast
           then show "T = {?x,?y,?z}"
             using Teq \<open>z = ?z\<close> \<open>y = ?y\<close> sets_eq by presburger
         qed
       next
         case 3
         then obtain i k a where eeq: "e = {prod_encode(0,i), prod_encode(2,k)}"
           and "i<M" and "k<M"
           and df: "diff2 k i = int a" and "a \<in> A"
           by (auto simp: XZ_def Edges_def part_of_def eval_nat_numeral)
         let ?x = "prod_encode (0, i)"
         let ?y = "prod_encode (1, (i+a) mod M)"
         let ?z = "prod_encode (2, k)"
         have keq: "k = (i+a+a) mod M"
           using diff2_invert [OF \<open>a \<in> A\<close>, of i] df \<open>k<M\<close> using inj_on_diff2 [of i]
           by (simp add: inj_on_def Ball_def mod_add_left_eq)
         with \<open>a \<in> A\<close>  have "{?x,?y} \<in> XY"
           using \<open>a \<in> A\<close> \<open>i<M\<close> \<open>k<M\<close> apply (auto simp: XY_def Edges_def)
           by (metis M_mod_bound diff_invert enc_iff from_enc imageI)
         moreover have "{?y,?z} \<in> YZ"
           apply (auto simp: YZ_def Edges_def image_iff eval_nat_numeral)
           by (metis M_mod_bound \<open>a \<in> A\<close> diff_invert enc_iff from_enc mod_add_left_eq keq)
         ultimately have T: "triangle_in_graph ?x ?y ?z G"
           using \<open>e \<in> uedges G\<close> by (force simp add: G_def eeq triangle_in_graph_def)
         show ?thesis
         proof (intro ex1I)
           show "\<exists>x y z. {?x,?y,?z} = {x, y, z} \<and> triangle_in_graph x y z G \<and> e \<subseteq> {?x,?y,?z}"
             using T eeq by blast
           fix T
           assume "\<exists>p q r. T = {p, q, r} \<and> triangle_in_graph p q r G \<and> e \<subseteq> T"
           then obtain p q r where Teq: "T = {p,q,r}" and tri: "triangle_in_graph p q r G" and "e \<subseteq> T"
             by blast
           with uniq obtain i' a' x y z where "i'<M" "a' \<in> A"  
                  and x: "x \<in> {p,q,r}" and y: "y \<in> {p,q,r}" and z: "z \<in> {p,q,r}"
                  and xeq: "x = prod_encode(0, i')"
                  and yeq: "y = prod_encode(1, (i'+a') mod M)"
                  and zeq: "z = prod_encode(2, (i'+a'+a') mod M)"
             by metis
           then have sets_eq: "{x,y,z} = {p,q,r}" by auto
           with Teq \<open>e \<subseteq> T\<close> have esub': "e \<subseteq> {x,y,z}" by blast
           have "a' < M"
             using A \<open>N < M\<close> \<open>a' \<in> A\<close> by auto
           obtain "?x \<in> e" "?z \<in> e" using eeq by force
           then have "x = ?x"
             using esub' eeq yeq zeq by simp
           then have "z = ?z"
             using esub' eeq yeq by simp
           obtain eq': "i' = i" "(i'+a'+a') mod M = k"
             using \<open>x = ?x\<close> xeq using \<open>z =?z\<close> zeq by auto
           then have "diff (i'+a') i' = int a'"
             by (simp add: diff_def \<open>a' < M\<close>)
           then have "a' = a"
             by (metis \<open>a' \<in> A\<close> add.commute df diff2_invert eq' mod_add_right_eq nat_int)
           then have "y = ?y"
             by (metis \<open>x = ?x\<close> prod_encode_eq snd_conv yeq xeq)
           then show "T = {?x,?y,?z}"
             using Teq \<open>x = ?x\<close> \<open>z = ?z\<close> sets_eq by presburger
         qed
       qed
     qed
     have *: "card (uedges G) \<le> \<epsilon>/12 * (card (uverts G))\<^sup>2"
       using X \<open>X < card (uverts G)\<close> \<open>unique_triangles G\<close> \<open>uwellformed G\<close> by blast
 
     have diff_cancel: "\<exists>j<M. diff j i = int a" if "a \<in> A" for i a
     proof -
       have "int a < int M"
         using A M_def that by auto
       then have "(int ((i + a) mod M) - int i) mod int M = int a"
         by (simp add: mod_diff_left_eq of_nat_mod)
       then show ?thesis
         using \<open>0 < M\<close> diff_def mod_less_divisor by blast
     qed
     have diff2_cancel: "\<exists>j<M. diff2 j i = int a" if "a \<in> A" "i<M" for i a
     proof -
       have "a<M"
         using that M_def A by auto
       have "(int ((i + 2*a) mod M) - int i) * (1 + int N) mod int M =
         (((int i + 2 * int a) mod M) - int i) * (1 + int N) mod int M"
         by (simp add: zmod_int)
       also have "\<dots> = 2 * int a * (1 + int N) mod int M"
         by (smt (verit) mod_diff_left_eq mod_mult_eq mod_mult_right_eq)
       also have "\<dots> = int a mod int M"
       proof -
         have "(2 * int a * (1 + int N) - int a) = M * a"
           by (simp add: M_def algebra_simps)
         then have "M dvd (2 * int a * (1 + int N) - int a)"
           by simp
         then show ?thesis
           using mod_eq_dvd_iff by blast
       qed
       also have "\<dots> = a" by (simp add: \<open>a < M\<close>)
       finally show ?thesis
         by (metis \<open>0 < M\<close> diff2_def mod_less_divisor of_nat_Suc) 
     qed
 
     have card_Edges: "card (Edges (part_of \<xi>) (part_of \<zeta>) df) = M * card A" (is "card ?E = _")
       if "\<xi> \<noteq> \<zeta>" and df_cancel: "\<forall>a\<in>A. \<forall>i<M. \<exists>j<M. df j i = int a" 
                  and df_inj: "\<forall>a. inj_on (\<lambda>x. df x a) {..<M}"  for \<xi> \<zeta> df
     proof -
       define R where "R \<equiv> \<lambda>\<xi> Y df u p. \<exists>x y i a. u = {x,y} \<and> p = (i,a) \<and> x = prod_encode (\<xi>,i) 
                                           \<and> y \<in> Y \<and> a \<in> A \<and> df(from_part y) (from_part x) = int a"
       have R_uniq: "\<lbrakk>R \<xi> (part_of \<zeta>) df u p; R \<xi> (part_of \<zeta>) df u p'; \<xi> \<noteq> \<zeta>\<rbrakk> \<Longrightarrow> p' = p" for u p p' \<xi> \<zeta> df
         by (auto simp add: R_def doubleton_eq_iff)
       define f where "f \<equiv> \<lambda>\<xi> Y df u. @p. R \<xi> Y df u p"
       have f_if_R: "f \<xi> (part_of \<zeta>) df u = p" if "R \<xi> (part_of \<zeta>) df u p" "\<xi> \<noteq> \<zeta>" for u p \<xi> \<zeta> df
         using R_uniq f_def that by blast
       have "bij_betw (f \<xi> (part_of \<zeta>) df) ?E ({..<M} \<times> A)"
         unfolding bij_betw_def inj_on_def
       proof (intro conjI strip)
         fix u u'
         assume "u \<in> ?E" and "u' \<in> ?E" 
           and eq: "f \<xi> (part_of \<zeta>) df u = f \<xi> (part_of \<zeta>) df u'"
         obtain x y a where u: "u = {x,y}" "x \<in> part_of \<xi>" "y \<in> part_of \<zeta>" "a \<in> A" 
           and df: "df (from_part y) (from_part x) = int a"
           using \<open>u \<in> ?E\<close>
           by (force simp add: Edges_def image_iff)
         then obtain i where i: "x = prod_encode (\<xi>,i)"
           using part_of_def by blast
         with u df R_def f_if_R that have fu: "f \<xi> (part_of \<zeta>) df u = (i,a)"
           by blast
         obtain x' y' a' where u': "u' = {x',y'}" "x' \<in> part_of \<xi>" "y' \<in> part_of \<zeta>" "a'\<in>A" 
            and df': "df (from_part y') (from_part x') = int a'"
           using \<open>u' \<in> ?E\<close> by (force simp add: Edges_def image_iff)
         then obtain i' where i': "x' = prod_encode (\<xi>,i')"
           using part_of_def by blast
         with u' df' R_def f_if_R that have fu': "f \<xi> (part_of \<zeta>) df u' = (i',a')" 
           by blast
         have "i'=i" "a' = a"
           using fu fu' eq by auto
         with i i' have "x = x'"
           by meson
         moreover have "from_part y = from_part y'"
           using df df' \<open>x = x'\<close> \<open>a' = a\<close> df_inj u'(3) u(3) 
           by (clarsimp simp add: inj_on_def) (metis part_of_M lessThan_iff)
         then have "y = y'"
           using part_of_def u'(3) u(3) by fastforce
         ultimately show "u = u'"
           using u'(1) u(1) by force
       next
         have "f \<xi> (part_of \<zeta>) df ` ?E \<subseteq> {..<M} \<times> A"
         proof (clarsimp simp: Edges_def)
           fix i a x y b
           assume "x \<in> part_of \<xi>" "y \<in> part_of \<zeta>" "df (from_part y) (from_part x) = int b"
             "b \<in> A" and feq: "(i, a) = f \<xi> (part_of \<zeta>) df {x, y}"
           then have "R \<xi> (part_of \<zeta>) df {x,y} (from_part x, b)"
             by (auto simp: R_def doubleton_eq_iff part_of_def)
           then have "(from_part x, b) = (i, a)"
             by (simp add: f_if_R feq from_part_def that)
           then show "i < M \<and> a \<in> A"
             using \<open>x \<in> part_of \<xi>\<close> \<open>b \<in> A\<close> part_of_M by fastforce
         qed
         moreover have "{..<M} \<times> A \<subseteq> f \<xi> (part_of \<zeta>) df ` ?E"
         proof clarsimp
           fix i a assume "a \<in> A" and "i < M"
           then obtain j where "j<M" and j: "df j i = int a"
             using df_cancel by metis
           then have fj: "f \<xi> (part_of \<zeta>) df {prod_encode (\<xi>, i), prod_encode (\<zeta>, j)} = (i,a)"
             by (metis R_def \<open>a \<in> A\<close> enc_iff f_if_R from_enc \<open>\<xi> \<noteq> \<zeta>\<close>)
           then have "{prod_encode (\<xi>,i), prod_encode (\<zeta>, j mod M)} \<in> Edges (part_of \<xi>) (part_of \<zeta>) df"
             apply (clarsimp simp: Edges_def doubleton_eq_iff)
             by (metis \<open>a \<in> A\<close> \<open>i < M\<close> \<open>j < M\<close> enc_iff from_enc image_eqI j mod_if)
           then show "(i,a) \<in> f \<xi> (part_of \<zeta>) df ` Edges (part_of \<xi>) (part_of \<zeta>) df"
             using \<open>j < M\<close> fj image_iff by fastforce
         qed
         ultimately show "f \<xi> (part_of \<zeta>) df ` ?E = {..<M} \<times> A" by blast
       qed
       then show ?thesis
         by (simp add: bij_betw_same_card card_cartesian_product)
     qed
     have [simp]: "disjnt XY YZ" "disjnt XY XZ" "disjnt YZ XZ"
       using disjnt_part_of unfolding XY_def YZ_def XZ_def Edges_def disjnt_def 
       by (clarsimp simp add: disjoint_iff doubleton_eq_iff, meson disjnt_iff n_not_Suc_n nat.discI)+
     have [simp]: "card XY = M * card A" "card YZ = M * card A"
       by (simp_all add: XY_def YZ_def card_Edges diff_cancel inj_on_diff)
     have [simp]: "card XZ = M * card A"
       by (simp_all add: XZ_def card_Edges diff2_cancel inj_on_diff2)
     have card_edges: "card (uedges G) = 3 * M * card A"
       by (simp add: G_def card_Un_disjnt)
     have "card A \<le> \<epsilon> * (real M / 4)"
       using * \<open>0 < M\<close> by (simp add: cardG card_edges power2_eq_square)
     also have "\<dots> < \<epsilon> * N"
       using \<open>N>0\<close> by (simp add: M_def assms)
     finally show "card A < \<epsilon> * N" .
   qed
 qed
 
 text\<open>We finally present the main statement formulated using the upper asymptotic density condition.\<close>
 
 theorem RothArithmeticProgressions:
   assumes "upper_asymptotic_density A > 0"
   shows "\<exists>k d. d>0 \<and> progression3 k d \<subseteq> A"
 proof (rule ccontr)
   assume non: "\<nexists>k d. 0 < d \<and> progression3 k d \<subseteq> A"
   obtain X where X: "\<forall>N \<ge> X. \<forall>A' \<subseteq> {..<N}. (\<nexists>k d. d>0 \<and> progression3 k d \<subseteq> A') 
                           \<longrightarrow> card A' < upper_asymptotic_density A / 2 * real N"
     by (metis half_gt_zero RothArithmeticProgressions_aux assms)
   then have "\<forall>N \<ge> X. card (A \<inter> {..<N}) < upper_asymptotic_density A / 2 * N"
     by (meson order_trans inf_le1 inf_le2 non)
   then have "upper_asymptotic_density A \<le> upper_asymptotic_density A / 2"
     by (force simp add: eventually_sequentially less_eq_real_def intro!: upper_asymptotic_densityI)
   with assms show False by linarith
 qed
 
 end
 
 
 
diff --git a/thys/Szemeredi_Regularity/Szemeredi.thy b/thys/Szemeredi_Regularity/Szemeredi.thy
--- a/thys/Szemeredi_Regularity/Szemeredi.thy
+++ b/thys/Szemeredi_Regularity/Szemeredi.thy
@@ -1,1018 +1,1018 @@
 section \<open>Szemerédi's Regularity Lemma\<close>
 
 theory Szemeredi
   imports Complex_Main "HOL-Library.Disjoint_Sets" "Girth_Chromatic.Ugraphs"
 
 begin
 
 text\<open>We formalise Szemerédi's Regularity Lemma, which is a major result in the study of large graphs
 (extremal graph theory).
 We follow Yufei Zhao's notes ``Graph Theory and Additive Combinatorics'' (MIT)
 \<^url>\<open>https://ocw.mit.edu/courses/mathematics/18-217-graph-theory-and-additive-combinatorics-fall-2019/lecture-notes/MIT18_217F19_ch3.pdf\<close>
 and W.T. Gowers's notes ``Topics in Combinatorics'' (University of Cambridge, Lent 2004, Chapter 3)
 \<^url>\<open>https://www.dpmms.cam.ac.uk/~par31/notes/tic.pdf\<close>.
 We also refer to a third source, also by Zhao and also entitled 
 ``Graph Theory and Additive Combinatorics'': \<^url>\<open>https://yufeizhao.com/gtac/gtac17.pdf\<close>.\<close>
 
 
 subsection \<open>Miscellaneous\<close>
 
 text \<open>A technical lemma used below in @{text \<open>energy_graph_partition_half\<close>}\<close>
 lemma sum_products_le:
   fixes a :: "'a \<Rightarrow> 'b::linordered_idom"
   assumes "\<And>i. i \<in> I \<Longrightarrow> a i \<ge> 0"
   shows "(\<Sum>i\<in>I. a i * b i)\<^sup>2 \<le> (\<Sum>i\<in>I. a i) * (\<Sum>i\<in>I. a i * (b i)\<^sup>2)"
   using assms
 proof (induction I rule: infinite_finite_induct)
   case (insert j I)
   then have "(\<Sum>i\<in>insert j I. a i * b i)\<^sup>2
           \<le> (a j * b j)\<^sup>2 + 2 * a j * b j * (\<Sum>i\<in>I. a i * b i) + (\<Sum>i\<in>I. a i) * (\<Sum>i\<in>I. a i * (b i)\<^sup>2)"
     using insert by (simp add: algebra_simps power2_eq_square)
   also have "\<dots> \<le> a j * (a j * (b j)\<^sup>2) + (a j * (sum a I * (b j)\<^sup>2 + (\<Sum>i\<in>I. a i * (b i)\<^sup>2)) 
                  + sum a I * (\<Sum>i\<in>I. a i * (b i)\<^sup>2))"
   proof -
     have "0 \<le> (\<Sum>i\<in>I. a i * (b i - b j)\<^sup>2)"
       by (simp add: insert.prems sum_nonneg)
     then have "2 * b j * (\<Sum>i\<in>I. a i * b i) \<le> (sum a I * (b j)\<^sup>2) + (\<Sum>i\<in>I. a i * (b i)\<^sup>2)"
       by (simp add: power2_eq_square algebra_simps sum_subtractf sum.distrib sum_distrib_left)
     then show ?thesis
       by (simp add: insert.prems power2_eq_square mult.commute mult.left_commute mult_left_mono)
   qed
   finally show ?case 
     by (simp add: insert algebra_simps)
 qed auto
 
 subsubsection \<open>Partitions indexed by integers\<close>
 
 definition finite_graph_partition :: "[uvert set, uvert set set, nat] \<Rightarrow> bool"
   where "finite_graph_partition V P n \<equiv> partition_on V P \<and> finite P \<and> card P = n"
 
 lemma finite_graph_partition_0 [iff]:
   "finite_graph_partition V P 0 \<longleftrightarrow> V = {} \<and> P = {}"
   by (auto simp: finite_graph_partition_def partition_on_def)
 
 lemma finite_graph_partition_empty [iff]:
   "finite_graph_partition {} P n \<longleftrightarrow> P = {} \<and> n = 0"
   by (auto simp: finite_graph_partition_def partition_on_def)
 
 lemma finite_graph_partition_equals:
   "finite_graph_partition V P n \<Longrightarrow> (\<Union>P) = V"
   by (meson finite_graph_partition_def partition_on_def)
 
 lemma finite_graph_partition_subset:
   "\<lbrakk>finite_graph_partition V P n; X \<in> P\<rbrakk> \<Longrightarrow> X \<subseteq> V"
   using finite_graph_partition_equals by blast
 
 lemma trivial_graph_partition_exists:
   assumes "V \<noteq> {}"
   shows "finite_graph_partition V {V} (Suc 0)"
   by (simp add: assms finite_graph_partition_def partition_on_space)
 
 lemma finite_graph_partition_finite:
   assumes "finite_graph_partition V P k" "finite V" "X \<in> P"
   shows "finite X"
   by (meson assms finite_graph_partition_subset infinite_super)
 
 lemma finite_graph_partition_gt0:
   assumes "finite_graph_partition V P k" "finite V" "X \<in> P"
   shows "card X > 0"
   by (metis assms card_0_eq finite_graph_partition_def finite_graph_partition_finite gr_zeroI partition_on_def)
 
 lemma card_finite_graph_partition:
   assumes "finite_graph_partition V P k" "finite V"
   shows "(\<Sum>X\<in>P. card X) = card V"
   by (metis assms finite_graph_partition_def finite_graph_partition_finite product_partition)
 
 subsubsection \<open>Tools to combine the refinements of the partition @{term "P i"} for each @{term i}\<close>
 
 text \<open>These are needed to retain the ``intuitive'' idea of partitions as indexed by integers.\<close>
 
 subsection \<open>Edges\<close>
 
 text \<open>All edges between two sets of vertices, @{term X} and @{term Y}, in a graph, @{term G}\<close>
 
 definition all_edges_between :: "nat set \<Rightarrow> nat set \<Rightarrow> nat set \<times> nat set set \<Rightarrow> (nat \<times> nat) set"
   where "all_edges_between X Y G \<equiv> {(x,y). x\<in>X \<and> y\<in>Y \<and> {x,y} \<in> uedges G}"
 
 lemma all_edges_between_subset: "all_edges_between X Y G \<subseteq> X\<times>Y"
   by (auto simp: all_edges_between_def)
 
 lemma max_all_edges_between: 
   assumes "finite X" "finite Y"
   shows "card (all_edges_between X Y G) \<le> card X * card Y"
   by (metis assms card_mono finite_SigmaI all_edges_between_subset card_cartesian_product)
 
 lemma all_edges_between_empty [simp]:
   "all_edges_between {} Z G = {}" "all_edges_between Z {} G = {}"
   by (auto simp: all_edges_between_def)
 
 lemma all_edges_between_disjnt1:
   assumes "disjnt X Y"
   shows "disjnt (all_edges_between X Z G) (all_edges_between Y Z G)"
   using assms by (auto simp: all_edges_between_def disjnt_iff)
 
 lemma all_edges_between_disjnt2:
   assumes "disjnt Y Z"
   shows "disjnt (all_edges_between X Y G) (all_edges_between X Z G)"
   using assms by (auto simp: all_edges_between_def disjnt_iff)
 
 lemma all_edges_between_Un1:
   "all_edges_between (X \<union> Y) Z G = all_edges_between X Z G \<union> all_edges_between Y Z G"
   by (auto simp: all_edges_between_def)
 
 lemma all_edges_between_Un2:
   "all_edges_between X (Y \<union> Z) G = all_edges_between X Y G \<union> all_edges_between X Z G"
   by (auto simp: all_edges_between_def)
 
 lemma finite_all_edges_between:
   assumes "finite X" "finite Y"
   shows "finite (all_edges_between X Y G)"
   by (meson all_edges_between_subset assms finite_cartesian_product finite_subset)
 
 subsection \<open>Edge Density and Regular Pairs\<close>
 
 text \<open>The edge density between two sets of vertices, @{term X} and @{term Y}, in @{term G}.
       Authors disagree on whether the sets are assumed to be disjoint!.
       Quite a few authors assume disjointness, e.g. Malliaris and Shelah \<^url>\<open>https://www.jstor.org/stable/23813167\<close>
       For the following definitions, see pages 49--50 in Zhao's notes.\<close>
 definition "edge_density X Y G \<equiv> card(all_edges_between X Y G) / (card X * card Y)"
 
 lemma edge_density_ge0: "edge_density X Y G \<ge> 0"
   by (auto simp: edge_density_def)
 
 lemma edge_density_le1: "edge_density K Y G \<le> 1"
 proof (cases "finite K \<and> finite Y")
   case True
   then show ?thesis 
     using of_nat_mono [OF max_all_edges_between, of K Y]
     by (fastforce simp add: edge_density_def divide_simps)
 qed (auto simp: edge_density_def)
 
 lemma all_edges_between_swap:
   "all_edges_between X Y G = (\<lambda>(x,y). (y,x)) ` (all_edges_between Y X G)"
   unfolding all_edges_between_def
   by (auto simp add: insert_commute image_iff split: prod.split)
 
 lemma card_all_edges_between_commute:
   "card (all_edges_between X Y G) = card (all_edges_between Y X G)"
 proof -
   have "inj_on (\<lambda>(x, y). (y, x)) A" for A :: "(nat*nat)set"
     by (auto simp: inj_on_def)
   then show ?thesis
     by (simp add: all_edges_between_swap [of X Y] card_image)
 qed
 
 lemma edge_density_commute: "edge_density X Y G = edge_density Y X G"
   by (simp add: edge_density_def card_all_edges_between_commute mult.commute)
 
 
 text \<open>$\epsilon$-regular pairs, for two sets of vertices. Again, authors disagree on whether the
 sets need to be disjoint, though it seems that overlapping sets cause double-counting. Authors also
 disagree about whether or not to use the strict subset relation here. The proofs below are easier if
 it is strict but later proofs require the non-strict version. The two definitions can be proved to
 be equivalent under fairly mild conditions, but even those conditions turn out to be onerous.\<close>
 
 definition regular_pair::  "uvert set  \<Rightarrow> uvert set \<Rightarrow> ugraph \<Rightarrow> real \<Rightarrow> bool"
   where "regular_pair X Y G \<epsilon> \<equiv> 
     \<forall>A B. A \<subseteq> X \<and> B \<subseteq> Y \<and> (card A \<ge> \<epsilon> * card X) \<and> (card B \<ge> \<epsilon> * card Y) \<longrightarrow>
               \<bar>edge_density A B G - edge_density X Y G\<bar> \<le> \<epsilon>" for \<epsilon>::real
 
 lemma regular_pair_commute: "regular_pair X Y G \<epsilon> \<longleftrightarrow> regular_pair Y X G \<epsilon>"
   by (metis edge_density_commute regular_pair_def)
 
 lemma edge_density_Un:
   assumes "disjnt X1 X2" "finite X1" "finite X2"
   shows "edge_density (X1 \<union> X2) Y G = (edge_density X1 Y G * card X1 + edge_density X2 Y G * card X2) / (card X1 + card X2)"
 proof (cases "finite Y")
   case True
   with assms show ?thesis 
     by (simp add: edge_density_def all_edges_between_disjnt1 all_edges_between_Un1 finite_all_edges_between card_Un_disjnt card_ge_0_finite divide_simps)
 qed (simp add: edge_density_def)
 
 lemma edge_density_partition:
   assumes "finite_graph_partition U P n"
   shows "edge_density U W G = (\<Sum>X\<in>P. edge_density X W G * card X) / card U"
 proof (cases "finite U")
   case True
   have "finite P"
     using assms finite_graph_partition_def by blast
   then show ?thesis
     using True assms
   proof (induction P arbitrary: n U)
     case empty
     then show ?case
       by (simp add: edge_density_def finite_graph_partition_def partition_on_def)
   next
     case (insert X P)
     then have "n > 0"
       by (metis finite_graph_partition_0 gr_zeroI insert_not_empty)
     with insert.prems insert.hyps 
     have UX: "finite_graph_partition (U-X) P (n-1)"
       by (auto simp: finite_graph_partition_def partition_on_def disjnt_iff pairwise_insert)
     then have finU: "finite (\<Union>P)"
       by (simp add: finite_graph_partition_equals insert)
     then have sumXP: "card U = card X + card (\<Union>P)"
       by (metis UX card_finite_graph_partition finite_graph_partition_equals insert.hyps insert.prems sum.insert)
     have FUX: "finite (U - X)"
       by (simp add: insert.prems)
     have XUP: "X \<union> (\<Union>P) = U"
       using finite_graph_partition_equals insert.prems(2) by auto
     then have "edge_density U W G = edge_density (X \<union> \<Union>P) W G"
       by auto
     also have "\<dots> = (edge_density X W G * card X + edge_density (\<Union>P) W G * card (\<Union>P)) 
                   / (card X + card (\<Union>P))"
     proof (rule edge_density_Un)
       show "disjnt X (\<Union>P)"
         using UX disjnt_iff finite_graph_partition_equals by auto
       show "finite X"
         using XUP \<open>finite U\<close> by blast
     qed (use finU in auto)
     also have "\<dots> = (edge_density X W G * card X + edge_density (U-X) W G * card (\<Union>P)) 
                   / card U"
       using UX card_finite_graph_partition finite_graph_partition_equals insert.prems(1) insert.prems(2) sumXP by auto
     also have "\<dots> = (\<Sum>Y \<in> insert X P. edge_density Y W G * card Y) / card U"
       using UX insert.prems insert.hyps 
       apply (simp add: insert.IH [OF FUX UX] divide_simps algebra_simps finite_graph_partition_equals)
       by (metis (no_types, lifting) Diff_eq_empty_iff finite_graph_partition_empty sum.empty)
     finally show ?case .
   qed
 qed (simp add: edge_density_def)
 
 text\<open>Let @{term P}, @{term Q} be partitions of a set of vertices @{term V}. 
   Then @{term P} refines @{term Q} if for all @{term \<open>A \<in> P\<close>} there is @{term \<open>B \<in> Q\<close>} 
   such that @{term \<open>A \<subseteq> B\<close>}.\<close>
 
 text \<open>For the sake of generality, and following Zhao's Online Lecture 
 \<^url>\<open>https://www.youtube.com/watch?v=vcsxCFSLyP8&t=16s\<close>
 we do not impose disjointness: we do not include @{term "i\<noteq>j"} below.\<close>
 
 definition irregular_set:: "[real, ugraph, uvert set set] \<Rightarrow> (uvert set \<times> uvert set) set"
   where "irregular_set \<equiv> \<lambda>\<epsilon>::real. \<lambda>G P. {(R,S)|R S. R\<in>P \<and> S\<in>P \<and> \<not> regular_pair R S G \<epsilon>}"
 
 text\<open>A regular partition may contain a few irregular pairs as long as their total size is bounded as follows.\<close>
 definition regular_partition:: "[real, ugraph, uvert set set] \<Rightarrow> bool"
   where
   "regular_partition \<equiv> \<lambda>\<epsilon>::real. \<lambda>G P . 
-     partition_on (uverts G) P  \<and>
+     partition_on (uverts G) P \<and>
      (\<Sum>(R,S) \<in> irregular_set \<epsilon> G P. card R * card S) \<le> \<epsilon> * (card (uverts G))\<^sup>2"
 
 lemma irregular_set_subset: "irregular_set \<epsilon> G P \<subseteq> P \<times> P"
   by (auto simp: irregular_set_def)
 
 lemma irregular_set_swap: "(i,j) \<in> irregular_set \<epsilon> G P \<longleftrightarrow> (j,i) \<in> irregular_set \<epsilon> G P"
   by (auto simp add: irregular_set_def regular_pair_commute)
 
 lemma finite_irregular_set [simp]: "finite P \<Longrightarrow> finite (irregular_set \<epsilon> G P)"
   by (metis finite_SigmaI finite_subset irregular_set_subset)
 
 subsection \<open>Energy of a Graph\<close>
 
 text \<open>Definition 3.7 (Energy), written @{term "q(U,W)"}\<close>
 definition energy_graph_subsets:: "[uvert set, uvert set, ugraph] \<Rightarrow> real" where
   "energy_graph_subsets U W G \<equiv>
      card U * card W * (edge_density U W G)\<^sup>2 / (card (uverts G))\<^sup>2"
 
 text \<open>Definition for partitions\<close>
 definition energy_graph_partitions :: "[ugraph, uvert set set, uvert set set] \<Rightarrow> real"
   where "energy_graph_partitions G U W \<equiv> \<Sum>R\<in>U.\<Sum>S\<in>W. energy_graph_subsets R S G"
 
 lemma energy_graph_subsets_0 [simp]: 
      "energy_graph_subsets {} B G = 0" "energy_graph_subsets A {} G = 0"
   by (auto simp: energy_graph_subsets_def)
 
 lemma energy_graph_subsets_ge0 [simp]:
   "energy_graph_subsets U W G \<ge> 0"
   by (auto simp: energy_graph_subsets_def)
 
 lemma energy_graph_partitions_ge0 [simp]:
   "energy_graph_partitions G U W \<ge> 0"
   by (auto simp: sum_nonneg energy_graph_partitions_def)
 
 lemma energy_graph_subsets_commute: 
   "energy_graph_subsets U W G = energy_graph_subsets W U G"
   by (simp add: energy_graph_subsets_def edge_density_commute)
 
 lemma energy_graph_partitions_commute:
   "energy_graph_partitions G W U = energy_graph_partitions G U W"
   by (simp add: energy_graph_partitions_def energy_graph_subsets_commute sum.swap [where A=W])
 
 text\<open>Definition 3.7 (Energy of a Partition), or following Gowers, mean square density:
  a version of energy for a single partition of the vertex set. \<close> 
 
 abbreviation mean_square_density :: "[ugraph, uvert set set] \<Rightarrow> real"
   where "mean_square_density G U \<equiv> energy_graph_partitions G U U"
 
 lemma mean_square_density: 
   "mean_square_density G U \<equiv> 
           (\<Sum>R\<in>U. \<Sum>S\<in>U. card R * card S * (edge_density R S G)\<^sup>2) / (card (uverts G))\<^sup>2"
   by (simp add: energy_graph_partitions_def energy_graph_subsets_def sum_divide_distrib)
 
 text\<open>Observation: the energy is between 0 and 1 because the edge density is bounded above by 1.\<close>
 
 lemma sum_partition_le:
   assumes "finite_graph_partition V P k" "finite V"
   shows "(\<Sum>R\<in>P. \<Sum>S\<in>P. real (card R * card S)) \<le> (real(card V))\<^sup>2"
 proof -
   have "finite P"
     using assms finite_graph_partition_def by blast
   then show ?thesis
     using assms
   proof (induction P arbitrary: V k)
     case (insert X P)
     have [simp]: "finite Y" if "Y \<in> insert X P" for Y
       by (meson finite_graph_partition_finite insert.prems that)
     have C: "card Y \<le> card V" if"Y \<in> insert X P" for Y
       by (meson card_mono finite_graph_partition_subset insert.prems that)
     have D [simp]: "(\<Sum>Y\<in>P. real (card Y)) = real (card V) - real (card X)"
       by (smt (verit) card_finite_graph_partition insert.hyps insert.prems of_nat_sum sum.cong sum.insert)
     have "disjnt X (\<Union>P)"
       using insert.prems insert.hyps
       by (auto simp add: finite_graph_partition_def disjnt_iff pairwise_insert partition_on_def)
     with insert have *: "(\<Sum>R\<in>P. \<Sum>S\<in>P. real (card R * card S)) \<le> (real (card (V - X)))\<^sup>2"
       unfolding finite_graph_partition_def
       by (simp add: lessThan_Suc partition_on_insert disjoint_family_on_insert sum.distrib)
     have [simp]: "V \<inter>X = X"
       using finite_graph_partition_equals insert.prems by blast 
     have "(\<Sum>R \<in> insert X P. \<Sum>S \<in> insert X P. real (card R * card S)) 
       = real (card X * card X) + 2 * (card V - card X) * card X
         + (\<Sum>R\<in>P. \<Sum>S\<in>P. real (card R * card S))"
       using \<open>X \<notin> P\<close> \<open>finite P\<close>
       by (simp add: C of_nat_diff sum.distrib algebra_simps flip: sum_distrib_right)
     also have "\<dots> \<le> real (card X * card X) + 2 * (card V - card X) * card X + (real (card (V - X)))\<^sup>2"
       using * by linarith
     also have "\<dots> \<le> (real (card V))\<^sup>2"
       by (simp add: of_nat_diff C card_Diff_subset_Int algebra_simps power2_eq_square)
     finally show ?case .
   qed auto
 qed
 
 lemma mean_square_density_bounded: 
   assumes "finite_graph_partition (uverts G) P k" "finite (uverts G)" 
   shows "mean_square_density G P \<le> 1"
 proof-
   have "(\<Sum>R\<in>P. \<Sum>S\<in>P. real (card R * card S) * (edge_density R S G)\<^sup>2) 
      \<le> (\<Sum>R\<in>P. \<Sum>S\<in>P. real (card R * card S))"
     by (intro sum_mono mult_right_le_one_le) (auto simp: abs_square_le_1 edge_density_ge0 edge_density_le1)
   also have "\<dots> \<le> (real(card (uverts G)))\<^sup>2"
     using sum_partition_le assms by blast 
   finally show ?thesis 
     by (simp add: mean_square_density divide_simps)
 qed
 
 subsection \<open>Partitioning and Energy\<close>
 
 text\<open>Zhao's Lemma 3.8 and Gowers's remark after Lemma 11. 
  Further partitioning of subsets of the vertex set cannot make the energy decrease. 
  We follow Gowers's proof, which avoids the use of probability.\<close>
 
 lemma energy_graph_partition_half:
   assumes P: "finite_graph_partition U P n"
   shows "card U * (edge_density U W G)\<^sup>2 \<le> (\<Sum>R\<in>P. card R * (edge_density R W G)\<^sup>2)"
 proof (cases "finite U")
   case True
   have \<section>: "(\<Sum>R\<in>P. card R * edge_density R W G)\<^sup>2 
          \<le> (sum card P) * (\<Sum>R\<in>P. card R * (edge_density R W G)\<^sup>2)"
     by (simp add: sum_products_le)
   have "card U * (edge_density U W G)\<^sup>2 = (\<Sum>R\<in>P. card R * (edge_density U W G)\<^sup>2)"
     by (metis \<open>finite U\<close> P sum_distrib_right card_finite_graph_partition of_nat_sum)
   also have "\<dots> = edge_density U W G * (\<Sum>R\<in>P. edge_density U W G * card R)"
     by (simp add: sum_distrib_left power2_eq_square mult_ac)
   also have "\<dots> = (\<Sum>R\<in>P. edge_density R W G * real (card R)) * edge_density U W G"
   proof -
     have "edge_density U W G * (\<Sum>R\<in>P. edge_density R W G * card R) 
         = edge_density U W G * (edge_density U W G * (\<Sum>R\<in>P. card R))"
       using \<open>finite U\<close> assms card_finite_graph_partition  by (auto simp: edge_density_partition [OF P])
     then show ?thesis
       by (simp add: mult.commute sum_distrib_left)
   qed
   also have "\<dots> = (\<Sum>R\<in>P. card R * edge_density R W G) * edge_density U W G"
     by (simp add: sum_distrib_left mult_ac)
   also have "\<dots> = (\<Sum>R\<in>P. card R * edge_density R W G)\<^sup>2 / card U"
     using assms by (simp add: edge_density_partition [OF P] mult_ac flip: power2_eq_square)
   also have "\<dots> \<le> (\<Sum>R\<in>P. card R * (edge_density R W G)\<^sup>2)"
     using \<section> P card_finite_graph_partition \<open>finite U\<close> 
     by (force simp add: mult_ac divide_simps simp flip: of_nat_sum)
   finally show ?thesis .
 qed (simp add: sum_nonneg)
 
 proposition energy_graph_partition_increase:
   assumes P: "finite_graph_partition U P k" and V: "finite_graph_partition W Q l"
   shows "energy_graph_partitions G P Q \<ge> energy_graph_subsets U W G" 
 proof -
   have "(card U * card W) * (edge_density U W G)\<^sup>2 = card W * (card U * (edge_density U W G)\<^sup>2)"
     by (simp add: mult_ac)
   also have "\<dots> \<le> card W * (\<Sum>R\<in>P. card R * (edge_density R W G)\<^sup>2)"
     by (intro mult_left_mono energy_graph_partition_half) (use assms in auto)
   also have "\<dots> = (\<Sum>R\<in>P. card R * (card W * (edge_density W R G)\<^sup>2))"
     by (simp add: sum_distrib_left edge_density_commute mult_ac)
   also have "\<dots> \<le> (\<Sum>R\<in>P. card R * (\<Sum>S\<in>Q. card S * (edge_density S R G)\<^sup>2))"
     by (intro mult_left_mono energy_graph_partition_half sum_mono) (use assms in auto)
   also have "\<dots> \<le> (\<Sum>R\<in>P. \<Sum>S\<in>Q. (card R * card S) * (edge_density R S G)\<^sup>2)"
     by (simp add: sum_distrib_left edge_density_commute mult_ac)
   finally
   have "(card U * card W) * (edge_density U W G)\<^sup>2 
     \<le> (\<Sum>R\<in>P. \<Sum>S\<in>Q. (card R * card S) * (edge_density R S G)\<^sup>2)" .
   then show ?thesis
     unfolding energy_graph_partitions_def energy_graph_subsets_def
     by (simp add: divide_simps flip: sum_divide_distrib)
 qed
 
 text \<open>The following is the fully general version of Gowers's Lemma 11 and Zhao's Lemma 3.9. 
 Further partitioning of subsets of the vertex set cannot make the energy decrease.
 Note that @{term V} should be @{term "uverts G"} even though this more general version holds.\<close>
 
 lemma energy_graph_partitions_increase_half:
   assumes ref: "refines V Y X" and "finite V" and part_VX: "partition_on V X"
     and U: "{} \<notin> U"
   shows "energy_graph_partitions G Y U \<ge> energy_graph_partitions G X U" 
         (is "?Y \<ge> ?X")
 proof -
   have "\<exists>F. partition_on R F \<and> F = {S\<in>Y. S \<subseteq> R}" if "R\<in>X" for R
     using ref refines_obtains_subset that by blast
   then obtain F where F: "\<And>R. R \<in> X \<Longrightarrow> partition_on R (F R) \<and> F R = {S\<in>Y. S \<subseteq> R}"
     by fastforce
   have injF: "inj_on F X"
     by (metis F inj_on_inverseI partition_on_def)
   have finite_X: "finite R" if "R \<in> X" for R
     by (metis Union_upper \<open>finite V\<close> part_VX finite_subset partition_on_def that)
   then have finite_F: "finite (F R)" if "R \<in> X" for R
     using that by (simp add: F)
   have dFX: "disjoint (F ` X)"
     using part_VX 
     by (smt (verit, best) F Union_upper disjnt_iff disjointD le_inf_iff pairwise_imageI partition_on_def subset_empty)
   have F_ne: "F R \<noteq> {}" if "R \<in> X" for R
     by (metis F Sup_empty part_VX partition_on_def that)
   have F_sums_Y: "(\<Sum>R\<in>X. \<Sum>U\<in>F R. f U) = (\<Sum>S\<in>Y. f S)" for f :: "nat set \<Rightarrow> real"
   proof -
     have Yn_eq: "Y = (\<Union>R \<in> X. F R)"
       using ref by (force simp add: refines_def dest: F)
     then have "(\<Sum>S\<in>Y. f S) = sum f (\<Union>R \<in> X. F R)"
       by blast
     also have "\<dots> = (sum \<circ> sum) f (F ` X)"
       by (smt (verit, best) dFX disjnt_def finite_F image_iff pairwiseD sum.Union_disjoint)
     also have "\<dots> = (\<Sum>R \<in> X. \<Sum>U\<in>F R. f U)"
       unfolding comp_apply by (metis injF sum.reindex_cong)
     finally show ?thesis
       by simp
   qed
   have "?X = (\<Sum>R \<in> X. \<Sum>T\<in>U. energy_graph_subsets R T G)"
     by (simp add: energy_graph_partitions_def)
   also have "\<dots> \<le> (\<Sum>R\<in>X. \<Sum>T\<in>U. energy_graph_partitions G (F R) {T})"
   proof -
     have "finite_graph_partition R (F R) (card (F R))"
       if "R \<in> X" for R
       by (meson F finite_F finite_graph_partition_def that) 
     moreover have "finite_graph_partition T {T} (Suc 0)"
       if "T \<in> U" for T
       using U by (metis that trivial_graph_partition_exists)
     ultimately show ?thesis
       using finite_X  by (intro sum_mono energy_graph_partition_increase) auto
   qed
   also have "\<dots> = (\<Sum>R \<in> X. \<Sum>D \<in> F R. \<Sum>T\<in>U. energy_graph_subsets D T G)"
     by (simp add: energy_graph_partitions_def sum.swap [where B = "U"])
   also have "\<dots> = ?Y"
     by (simp add: energy_graph_partitions_def F_sums_Y)
   finally show ?thesis .
 qed
 
 proposition energy_graph_partitions_increase:
   assumes "refines V Y X" "refines V' W U" 
     and "finite V" "finite V'" 
   shows "energy_graph_partitions G Y W \<ge> energy_graph_partitions G X U"
 proof -
   obtain "{} \<notin> U" "{} \<notin> Y"
     using assms unfolding refines_def partition_on_def by presburger
   then show ?thesis
     using assms unfolding refines_def
     by (smt (verit, ccfv_SIG) assms energy_graph_partitions_commute energy_graph_partitions_increase_half)
 qed
 
 text \<open>The original version of Gowers's Lemma 11 and Zhao's Lemma 3.9 
       is not general enough to be used for anything.\<close>
 corollary mean_square_density_increase:
   assumes "refines V Y X" "finite V"
   shows "mean_square_density G Y \<ge> mean_square_density G X"
   using assms energy_graph_partitions_increase by presburger 
 
 
 text\<open>The Energy Boost Lemma (Lemma 3.10 in Zhao's notes) says that an 
 irregular partition increases the energy substantially. We assume that @{term "\<U> \<subseteq> uverts G"} 
 and @{term "\<W> \<subseteq> uverts G"} are not irregular, as witnessed by their subsets @{term"U1 \<subseteq> \<U>"} and @{term"W1 \<subseteq> \<W>"}.
 The proof follows Lemma 12 of Gowers. \<close>
 
 definition "part2 X Y \<equiv> if X \<subset> Y then {X,Y-X} else {Y}"
 
 lemma card_part2: "card (part2 X Y) \<le> 2"
   by (simp add: part2_def card_insert_if)
 
 lemma sum_part2: "\<lbrakk>X \<subseteq> Y; f{} = 0\<rbrakk> \<Longrightarrow> sum f (part2 X Y) = f X + f (Y-X)"
   by (force simp add: part2_def sum.insert_if)
 
 lemma partition_part2:
   assumes "A \<subseteq> B" "A \<noteq> {}"
   shows "partition_on B (part2 A B)"
   using assms by (auto simp add: partition_on_def part2_def disjnt_iff pairwise_insert)
 
 proposition energy_boost:
   fixes \<epsilon>::real and U W G
   defines "alpha \<equiv> edge_density U W G"
   defines "u \<equiv> \<lambda>X Y. edge_density X Y G - alpha"
   assumes "finite U" "finite W"
     and "U' \<subseteq> U" "W' \<subseteq> W" "\<epsilon> > 0"
     and U': "card U' \<ge> \<epsilon> * card U" and W': "card W' \<ge> \<epsilon> * card W"
     and gt: "\<bar>u U' W'\<bar> > \<epsilon>"
   shows "(\<Sum>A \<in> part2 U' U. \<Sum>B \<in> part2 W' W. energy_graph_subsets A B G)
          \<ge> energy_graph_subsets U W G + \<epsilon>^4 * (card U * card W) / (card (uverts G))\<^sup>2"
           (is "?lhs \<ge> ?rhs")
 proof -
   define UF where "UF \<equiv> part2 U' U"
   define WF where "WF \<equiv> part2 W' W"
   obtain [simp]: "finite U" "finite W"
     using assms by (meson finite_subset)
   obtain card': "card U' > 0" "card W' > 0"
     using gt \<open>\<epsilon> > 0\<close> U' W'
     by (force simp: u_def alpha_def edge_density_def mult_le_0_iff zero_less_mult_iff)
   then obtain card: "card U > 0" "card W > 0"
     using assms by fastforce
   then obtain [simp]: "finite U'" "finite W'"
     by (meson card' card_ge_0_finite)
   obtain [simp]: "W' \<noteq> W - W'" "U' \<noteq> U - U'"
     by (metis DiffD2 card' all_not_in_conv card.empty less_irrefl)
   have UF_ne: "card x \<noteq> 0" if "x \<in> UF" for x
     using card' assms that by (auto simp: UF_def part2_def split: if_split_asm)
   have WF_ne: "card x \<noteq> 0" if "x \<in> WF" for x
     using card' assms that by (auto simp: WF_def part2_def split: if_split_asm)
   have cardUW: "card U = card U' + card(U - U')" "card W = card W' + card(W - W')"
     using card card' \<open>U' \<subseteq> U\<close> \<open>W' \<subseteq> W\<close>
     by (metis card_eq_0_iff card_Diff_subset card_mono le_add_diff_inverse less_le)+
   have "U = (U - U') \<union> U'" "disjnt (U - U') U'"
     using \<open>U' \<subseteq> U\<close> by (force simp: disjnt_iff)+
   then have CU: "card (all_edges_between U Z G) 
           = card (all_edges_between (U - U') Z G) + card (all_edges_between U' Z G)" 
       if "finite Z" for Z 
     by (metis \<open>finite U'\<close> all_edges_between_Un1 all_edges_between_disjnt1 \<open>finite U\<close> 
         card_Un_disjnt finite_Diff finite_all_edges_between that)
 
   have "W = (W - W') \<union> W'" "disjnt (W - W') W'"
     using \<open>W' \<subseteq> W\<close> by (force simp: disjnt_iff)+
   then have CW: "card (all_edges_between Z W G) 
           = card (all_edges_between Z (W - W') G) + card (all_edges_between Z W' G)"
     if "finite Z" for Z
     by (metis \<open>finite W'\<close> all_edges_between_Un2 all_edges_between_disjnt2 \<open>finite W\<close>
         card_Un_disjnt finite_Diff2 finite_all_edges_between that)
   have *: "(\<Sum>X\<in>UF. \<Sum>Y\<in>WF. real (card (all_edges_between X Y G))) 
          = card (all_edges_between U W G)"
     by (simp add: UF_def WF_def cardUW CU CW sum_part2 \<open>U' \<subseteq> U\<close> \<open>W' \<subseteq> W\<close>)
   have **: "real (card U) * real (card W) = (\<Sum>X\<in>UF. \<Sum>Y\<in>WF. card X * card Y)"
     by (simp add: UF_def WF_def cardUW sum_part2 \<open>U' \<subseteq> U\<close> \<open>W' \<subseteq> W\<close> algebra_simps)
 
   let ?S = "\<Sum>X\<in>UF. \<Sum>Y\<in>WF. (card X * card Y) / (card U * card W) * (edge_density X Y G)\<^sup>2"
   define T where "T \<equiv> (\<Sum>X\<in>UF. \<Sum>Y\<in>WF. (card X * card Y) / (card U * card W) * (edge_density X Y G))"
   have \<section>: "2 * T = alpha + alpha * (\<Sum>X\<in>UF. \<Sum>Y\<in>WF. (card X * card Y) / (card U * card W))"
     unfolding alpha_def T_def
     by (simp add: * ** edge_density_def divide_simps sum_part2 \<open>U' \<subseteq> U\<close> \<open>W' \<subseteq> W\<close> UF_ne WF_ne flip: sum_divide_distrib)
   have "\<epsilon> * \<epsilon> \<le> u U' W' * u U' W'"
     by (metis abs_ge_zero abs_mult_self_eq \<open>\<epsilon> > 0\<close> gt less_le mult_mono)
   then have "(\<epsilon>*\<epsilon>)*(\<epsilon>*\<epsilon>) \<le> (card U' * card W') / (card U * card W) * (u U' W')\<^sup>2"
     using card mult_mono [OF U' W']  \<open>\<epsilon> > 0\<close>
     apply (simp add: divide_simps eval_nat_numeral)
     by (smt (verit, del_insts) mult.assoc mult.commute mult_mono' of_nat_0_le_iff zero_le_mult_iff)
   also have "\<dots> \<le> (\<Sum>X\<in>UF. \<Sum>Y\<in>WF.  (card X * card Y) / (card U * card W) * (u X Y)\<^sup>2)"
     by (simp add: UF_def WF_def sum_part2 \<open>U' \<subseteq> U\<close> \<open>W' \<subseteq> W\<close>)
   also have "\<dots> = ?S - 2 * T * alpha
                  + alpha\<^sup>2 * (\<Sum>X\<in>UF. \<Sum>Y\<in>WF. (card X * card Y) / (card U * card W))"
     by (simp add: u_def T_def power2_diff mult_ac ring_distribs divide_simps 
           sum_distrib_left sum_distrib_right sum_subtractf sum.distrib flip: sum_divide_distrib)
   also have "\<dots> = ?S - alpha\<^sup>2"
     using \<section> by (simp add: power2_eq_square algebra_simps)
   finally have 12: "alpha\<^sup>2 + \<epsilon>^4 \<le> ?S"
     by (simp add: eval_nat_numeral)
   have "?rhs = (alpha\<^sup>2 + \<epsilon>^4) * (card U * card W / (card (uverts G))\<^sup>2)"
     unfolding alpha_def energy_graph_subsets_def
     by (simp add: ring_distribs divide_simps power2_eq_square)
   also have "\<dots> \<le> ?S * (card U * card W / (card (uverts G))\<^sup>2)"
     by (rule mult_right_mono [OF 12]) auto
   also have "\<dots> = ?lhs"
     using card unfolding energy_graph_subsets_def UF_def WF_def
     by (auto simp add: algebra_simps sum_part2 \<open>U' \<subseteq> U\<close> \<open>W' \<subseteq> W\<close> )
   finally show ?thesis .
 qed
 
 subsection \<open>Towards Zhao's Lemma 3.11\<close>
 
 text\<open>Lemma 3.11 says that we can always find a refinement
 that increases the energy by a certain amount.\<close>
 
 text \<open>A necessary lemma for the tower of exponentials in the result. Angeliki's proof\<close>
 lemma le_tower_2: "k * (2 ^ Suc k) \<le> 2^(2^k)"
 proof (induction k rule: less_induct)
   case (less k)
   show ?case 
   proof (cases "k \<le> Suc (Suc 0)")
     case False
     define j where "j = k - Suc 0"
     have kj: "k = Suc j"
       using False j_def by force
     with False have \<section>: "(2^j + 3) \<le> (2::nat) ^ k"
       by (simp add: Suc_leI le_less_trans not_less_eq_eq numeral_3_eq_3)
     have "k * (2 ^ Suc k) \<le> 6 * j * 2^j"
       using False by (simp add: kj)
     also have "\<dots> \<le> 6 * 2^(2^j)"
       using kj less.IH by force
     also have "\<dots> < 2^(2^j + 3)"
       by (simp add: power_add) 
     also have "\<dots> \<le> 2^2^k"
       by (simp add: \<section>)
     finally show ?thesis
       by simp      
   qed (auto simp: le_Suc_eq)
 qed
 
 
 text \<open>Zhao's actual Lemma 3.11. However, the bound $m \le k 2 ^{k+1}$  
 comes from a different source by Zhao: ``Graph Theory and Additive Combinatorics'', \<^url>\<open>https://yufeizhao.com/gtac/gtac17.pdf\<close>.
 Zhao's original version, and Gowers', both have incorrect bounds.\<close>
 proposition exists_refinement:
   assumes fgp: "finite_graph_partition (uverts G) P k" and "finite (uverts G)" 
     and irreg: "\<not> regular_partition \<epsilon> G P" and "\<epsilon> > 0"
   obtains Q where "refines (uverts G) Q P"                     
                     "mean_square_density G Q \<ge> mean_square_density G P + \<epsilon>^5" 
                     "\<And>R. R\<in>P \<Longrightarrow> card {S\<in>Q. S \<subseteq> R} \<le> 2 ^ Suc k"
                     "card Q \<le> k * 2 ^ Suc k"
 proof -
   define sum_pp where "sum_pp \<equiv> (\<Sum>(R,S) \<in> irregular_set \<epsilon> G P. card R * card S)"
   have cardP: "card P = k"
     using fgp finite_graph_partition_def by force
   then have "k \<noteq> 0"
     using assms unfolding regular_partition_def irregular_set_def finite_graph_partition_def by fastforce
   with assms have G_nonempty: "0 < card (uverts G)"
     by (metis card_gt_0_iff finite_graph_partition_empty)
   have part_GP: "partition_on (uverts G) P"
     using fgp finite_graph_partition_def by blast 
   then have finP: "finite R" "R \<noteq> {}" if "R\<in>P" for R
     using assms that partition_onD3 finite_graph_partition_finite by blast+
   have spp: "sum_pp > \<epsilon> * (card (uverts G))\<^sup>2"
     by (metis irreg not_le part_GP regular_partition_def sum_pp_def)
   then have sum_irreg_pos: "sum_pp > 0"
     using \<open>\<epsilon> > 0\<close> G_nonempty less_asym by fastforce
   have "\<exists>X\<subseteq>R. \<exists>Y\<subseteq>S. \<epsilon> * card R \<le> card X \<and> \<epsilon> * card S \<le> card Y \<and>
                      \<bar>edge_density X Y G - edge_density R S G\<bar> > \<epsilon>"
     if "(R,S) \<in> irregular_set \<epsilon> G P" for R S
     using that fgp finite_graph_partition_subset by (simp add: irregular_set_def regular_pair_def not_le) 
   then obtain X0 Y0 
     where XY0_psub_P: "\<And>R S. \<lbrakk>(R,S) \<in> irregular_set \<epsilon> G P\<rbrakk> \<Longrightarrow> X0 R S \<subseteq> R \<and> Y0 R S \<subseteq> S"
     and XY0_eps:
     "\<And>R S. (R,S) \<in> irregular_set \<epsilon> G P
         \<Longrightarrow> \<epsilon> * card R \<le> card (X0 R S) \<and> \<epsilon> * card S \<le> card (Y0 R S) \<and>
             \<bar>edge_density (X0 R S) (Y0 R S) G - edge_density R S G\<bar> > \<epsilon>"
     by metis
   obtain iP where iP: "bij_betw iP P {..<k}"
     by (metis fgp finite_graph_partition_def to_nat_on_finite cardP)
   define X where "X \<equiv> \<lambda>R S. if iP R < iP S then Y0 S R else X0 R S"
   define Y where "Y \<equiv> \<lambda>R S. if iP R < iP S then X0 S R else Y0 R S"
   have XY_psub_P: "\<And>R S. \<lbrakk>(R,S) \<in> irregular_set \<epsilon> G P\<rbrakk> \<Longrightarrow> X R S \<subseteq> R \<and> Y R S \<subseteq> S"
     using XY0_psub_P by (force simp: X_def Y_def irregular_set_swap)
   have XY_eps:
     "\<And>R S. (R,S) \<in> irregular_set \<epsilon> G P
         \<Longrightarrow> \<epsilon> * card R \<le> card (X R S) \<and> \<epsilon> * card S \<le> card (Y R S) \<and>
             \<bar>edge_density (X R S) (Y R S) G - edge_density R S G\<bar> > \<epsilon>"
     using XY0_eps by (force simp: X_def Y_def edge_density_commute irregular_set_swap)
   have card_elem_P: "card R > 0" if "R\<in>P" for R
     by (metis card_eq_0_iff finP neq0_conv that)
   have XY_nonempty: "X R S \<noteq> {}" "Y R S \<noteq> {}" if "(R,S) \<in> irregular_set \<epsilon> G P" for R S
     using XY_eps [OF that] that \<open>\<epsilon> > 0\<close> card_elem_P [of R] card_elem_P [of S]
     by (auto simp: irregular_set_def mult_le_0_iff)
 
   text\<open>By the assumption that our partition is irregular, there are many irregular pairs.
        For each irregular pair, find pairs of subsets that witness irregularity.\<close>
   define XP where "XP R \<equiv> ((\<lambda>S. part2 (X R S) R) ` {S. (R,S) \<in> irregular_set \<epsilon> G P})" for R
   define YP where "YP S \<equiv> ((\<lambda>R. part2 (Y R S) S) ` {R. (R,S) \<in> irregular_set \<epsilon> G P})" for S
 
   text \<open>include degenerate partition to ensure it works whether or not there's an irregular pair\<close>
   define PP where "PP \<equiv> \<lambda>R. insert {R} (XP R \<union> YP R)"
   define QS where "QS R \<equiv> common_refinement (PP R)" for R
   define r where "r R \<equiv> card (QS R)" for R
   have "finite P"
     using fgp finite_graph_partition_def by blast
   then have finPP: "finite (PP R)" for R
     by (simp add: PP_def XP_def YP_def irregular_set_def)
   have inPP_fin: "P \<in> PP R \<Longrightarrow> finite P" for P R
     by (auto simp: PP_def XP_def YP_def part2_def)
   have finite_QS: "finite (QS R)" for R
     by (simp add: QS_def finPP finite_common_refinement inPP_fin)
 
   have part_QS: "partition_on R (QS R)" if "R \<in> P" for R
     unfolding QS_def
   proof (intro partition_on_common_refinement partition_onI)
     show "\<And>\<A>. \<A> \<in> PP R \<Longrightarrow> {} \<notin> \<A>"
       using that XY_nonempty XY_psub_P finP
       by (fastforce simp add: PP_def XP_def YP_def part2_def)
   qed (auto simp: disjnt_iff PP_def XP_def YP_def part2_def dest: XY_psub_P)
 
   have part_P_QS: "finite_graph_partition R (QS R) (r R)" if "R\<in>P" for R
     by (simp add: finite_QS finite_graph_partition_def part_QS r_def that)
   then have fin_SQ [simp]: "finite (QS R)" if "R\<in>P" for R
     using QS_def finite_QS by force
   have QS_ne: "{} \<notin> QS R" if "R\<in>P" for R
     using QS_def part_QS partition_onD3 that by blast 
   have QS_subset_P: "q \<in> QS R \<Longrightarrow> q \<subseteq> R" if "R\<in>P" for R q
     by (meson finite_graph_partition_subset part_P_QS that)
   then have QS_inject: "R = R'" 
     if "R\<in>P" "R'\<in>P" "q \<in> QS R" "q \<in> QS R'" for R R' q
     by (metis UnionI disjnt_iff equals0I pairwiseD part_GP part_QS partition_on_def that)
   define Q where "Q \<equiv> (\<Union>R\<in>P. QS R)"
   define m where "m \<equiv> \<Sum>R\<in>P. r R"
   show thesis
   proof
     show ref_QP: "refines (uverts G) Q P"
       unfolding refines_def
     proof (intro conjI strip part_GP)
       fix X
       assume "X \<in> Q"
       then show "\<exists>Y\<in>P. X \<subseteq> Y"
         by (metis QS_subset_P Q_def UN_iff)
     next
       show "partition_on (uverts G) Q"
       proof (intro conjI partition_onI)
         show "\<Union>Q = uverts G"
         proof
           show "\<Union>Q \<subseteq> uverts G"
             using QS_subset_P Q_def fgp finite_graph_partition_equals by fastforce
           show "uverts G \<subseteq> \<Union>Q"
             by (metis Q_def Sup_least UN_upper Union_mono part_GP part_QS partition_onD1)
         qed
         show "disjnt p q" if "p \<in> Q" and "q \<in> Q" and "p \<noteq> q" for p q
         proof -
           from that 
           obtain R S where "R\<in>P" "S\<in>P" 
             and *: "p \<in> QS R" "q \<in> QS S"
             by (auto simp: Q_def QS_def)
           show ?thesis
           proof (cases "R=S")
             case True
             then show ?thesis
               using part_QS [of R]
               by (metis \<open>R \<in> P\<close> * pairwiseD partition_on_def \<open>p \<noteq> q\<close>)
           next
             case False
             with * show ?thesis
               by (metis QS_subset_P \<open>R \<in> P\<close> \<open>S \<in> P\<close> disjnt_iff pairwiseD part_GP partition_on_def subsetD)
           qed
         qed
         show "{} \<notin> Q"
           using QS_ne Q_def by blast
       qed
     qed 
     have disj_QSP: "disjoint_family_on QS P"
       unfolding disjoint_family_on_def by (metis Int_emptyI QS_inject)
     let ?PP = "P \<times> P"
     let ?REG = "?PP - irregular_set \<epsilon> G P"
     define sum_eps where "sum_eps \<equiv> (\<Sum>(R,S) \<in> irregular_set \<epsilon> G P. \<epsilon>^4 * (card R * card S) / (card (uverts G))\<^sup>2)"
     have A: "energy_graph_subsets R S G + \<epsilon>^4 * (card R * card S) / (card (uverts G))\<^sup>2
           \<le> energy_graph_partitions G (part2 (X R S) R) (part2 (Y R S) S)"
           (is "?L \<le> ?R")
           if *: "(R,S) \<in> irregular_set \<epsilon> G P" for R S
     proof -
       have "R\<in>P" "S\<in>P"
         using * by (auto simp: irregular_set_def)
       have "?L \<le> (\<Sum>A \<in> part2 (X R S) R. \<Sum>B \<in> part2 (Y R S) S. energy_graph_subsets A B G)"
         using XY_psub_P [OF *] XY_eps [OF *] assms
         by (intro energy_boost \<open>R \<in> P\<close> \<open>S \<in> P\<close> finP \<open>\<epsilon>>0\<close>) auto
       also have "\<dots> \<le> ?R"
         by (simp add: energy_graph_partitions_def)
       finally show ?thesis .
     qed
     have B: "energy_graph_partitions G (part2 (X R S) R) (part2 (Y R S) S)
           \<le> energy_graph_partitions G (QS R) (QS S)"
       if "(R,S) \<in> irregular_set \<epsilon> G P" for R S
     proof -
       have "R\<in>P" "S\<in>P" using that by (auto simp: irregular_set_def)
       have [simp]: "\<not> X R S \<subset> R \<longleftrightarrow> X R S = R" "\<not> Y R S \<subset> S \<longleftrightarrow> Y R S = S"
         using XY_psub_P that by blast+
       have XPX: "part2 (X R S) R \<in> PP R"
         using that by (simp add: PP_def XP_def)
       have I: "partition_on R (QS R)"
         using QS_def \<open>R \<in> P\<close> part_QS by force
       moreover have "\<forall>q \<in> QS R. \<exists>b \<in> part2 (X R S) R. q \<subseteq> b"
         using common_refinement_exists [OF _ XPX] by (simp add: QS_def)
       ultimately have ref_XP: "refines R (QS R) (part2 (X R S) R)"
         by (simp add: refines_def XY_nonempty XY_psub_P that partition_part2)
       have YPY: "part2 (Y R S) S \<in> PP S"
         using that by (simp add: PP_def YP_def)
       have J: "partition_on S (QS S)"
         using QS_def \<open>S \<in> P\<close> part_QS by force
       moreover have "\<forall>q \<in> QS S. \<exists>b \<in> part2 (Y R S) S. q \<subseteq> b"
         using common_refinement_exists [OF _ YPY] by (simp add: QS_def)
       ultimately have ref_YP: "refines S (QS S) (part2 (Y R S) S)"
         by (simp add: XY_nonempty XY_psub_P that partition_part2 refines_def)
       show ?thesis
         using \<open>R \<in> P\<close> \<open>S \<in> P\<close>
         by (simp add: finP energy_graph_partitions_increase [OF ref_XP ref_YP])
     qed
     have "mean_square_density G P + \<epsilon>^5 \<le> mean_square_density G P + sum_eps"
     proof -
       have "\<epsilon>^5 = (\<epsilon> * (card (uverts G))\<^sup>2) * (\<epsilon>^4 / (card (uverts G))\<^sup>2)"
         using G_nonempty by (simp add: field_simps eval_nat_numeral)
       also have "\<dots> \<le> sum_pp * (sum_eps / sum_pp)"
       proof (rule mult_mono)
         show "\<epsilon>^4 / real ((card (uverts G))\<^sup>2) \<le> sum_eps / sum_pp"
           using sum_irreg_pos sum_eps_def sum_pp_def
           by (auto simp add: case_prod_unfold sum.neutral simp flip: sum_distrib_left sum_divide_distrib of_nat_sum of_nat_mult)
       qed (use spp sum_nonneg in auto)
       also have "\<dots> \<le> sum_eps"
         by (simp add: sum_irreg_pos)
       finally show ?thesis by simp
     qed
     also have "\<dots> = (\<Sum>(i,j)\<in>?REG. energy_graph_subsets i j G) 
                    + (\<Sum>(i,j)\<in>irregular_set \<epsilon> G P. energy_graph_subsets i j G) + sum_eps"
       by (simp add: \<open>finite P\<close> energy_graph_partitions_def sum.cartesian_product irregular_set_subset sum.subset_diff)
     also have "\<dots> \<le> (\<Sum>(i,j) \<in> ?REG. energy_graph_subsets i j G)
                    + (\<Sum>(i,j) \<in> irregular_set \<epsilon> G P. energy_graph_partitions G (part2 (X i j) i) (part2 (Y i j) j))"
       using A unfolding sum_eps_def case_prod_unfold
       by (force intro: sum_mono simp flip: sum.distrib)
     also have "\<dots> \<le> (\<Sum>(i,j) \<in> ?REG. energy_graph_partitions G (QS i) (QS j))
                    + (\<Sum>(i,j) \<in> irregular_set \<epsilon> G P. energy_graph_partitions G (part2 (X i j) i) (part2 (Y i j) j))"
       by (auto intro!: part_P_QS sum_mono energy_graph_partition_increase)
     also have "\<dots> \<le> (\<Sum>(i,j) \<in> ?REG. energy_graph_partitions G (QS i) (QS j)) 
                   + (\<Sum>(i,j) \<in> irregular_set \<epsilon> G P. energy_graph_partitions G (QS i) (QS j))"
       using B
     proof (intro sum_mono add_mono ordered_comm_monoid_add_class.sum_mono2)
     qed (auto split: prod.split)
     also have "\<dots> = (\<Sum>(i,j) \<in> ?PP. energy_graph_partitions G (QS i) (QS j))"
       by (metis (no_types, lifting) \<open>finite P\<close> finite_SigmaI irregular_set_subset sum.subset_diff)
     also have "\<dots> = (\<Sum>i\<in>P. \<Sum>j\<in>P. energy_graph_partitions G (QS i) (QS j))"
       by (simp flip: sum.cartesian_product)
     also have "\<dots> = (\<Sum>A \<in> Q. \<Sum>B \<in> Q. energy_graph_subsets A B G)"
       unfolding energy_graph_partitions_def Q_def
       by (simp add: disj_QSP \<open>finite P\<close> sum.UNION_disjoint_family sum.swap [of _ "P" "QS _"])
     also have "\<dots> = mean_square_density G Q"
       by (simp add: mean_square_density energy_graph_subsets_def sum_divide_distrib)
     finally show "mean_square_density G P + \<epsilon> ^ 5 \<le> mean_square_density G Q" .
 
     define QinP where "QinP \<equiv> \<lambda>i. {j\<in>Q. j \<subseteq> i}"
     show card_QP: "card (QinP i) \<le> 2 ^ Suc k"
       if "i \<in> P" for i 
     proof -
       have less_cardP: "iP i < k"
         using iP bij_betwE that by blast
       have card_cr: "card (QS i) \<le> 2 ^ Suc k"
       proof -
         have "card (QS i) \<le> prod card (PP i)"
           by (simp add: QS_def card_common_refinement finPP inPP_fin) 
         also have "\<dots> = prod card (XP i \<union> YP i)"
           using finPP by (simp add: PP_def prod.insert_if)
         also have "\<dots> \<le> 2 ^ Suc k" 
         proof (rule prod_le_power)
           define XS where "XS \<equiv> (\<Union>R \<in> {R\<in>P. iP R \<le> iP i}. {part2 (X0 i R) i})"
           define YS where "YS \<equiv> (\<Union>R \<in> {R\<in>P. iP R \<ge> iP i}. {part2 (Y0 R i) i})"
           have 1: "{R \<in> P. iP R \<le> iP i} \<subseteq> iP -` {..iP i} \<inter> P"
             by auto
           have "card XS \<le> card {R \<in> P. iP R \<le> iP i}"
             by (force simp add: XS_def \<open>finite P\<close> intro: order_trans [OF card_UN_le])
           also have "\<dots> \<le> card (iP -` {..iP i} \<inter> P)"
             using 1 by (simp add: \<open>finite P\<close> card_mono)
           also have "\<dots> \<le> Suc (iP i)"
             by (metis card_vimage_inj_on_le bij_betw_def card_atMost finite_atMost iP)
           finally have cXS: "card XS \<le> Suc (iP i)" .
           have 2: "{R \<in> P. iP R \<ge> iP i} \<subseteq> iP -` {iP i..<k} \<inter> P"
             by clarsimp (meson bij_betw_apply iP lessThan_iff nat_less_le)
           have "card YS \<le> card {R \<in> P. iP R \<ge> iP i}"
             by (force simp add: YS_def \<open>finite P\<close> intro: order_trans [OF card_UN_le])
           also have "\<dots> \<le> card (iP -` {iP i..<k} \<inter> P)"
             using 2 by (simp add: \<open>finite P\<close> card_mono)
           also have "\<dots> \<le> card {iP i..<k}"
             by (meson bij_betw_def card_vimage_inj_on_le finite_atLeastLessThan iP)
           finally have "card YS \<le> k - iP i" 
             by simp
           with less_cardP cXS have k': "card XS + card YS \<le> Suc k"
             by linarith
           have finXYS: "finite (XS \<union> YS)"
             unfolding XS_def YS_def using \<open>finite P\<close> by (auto intro: finite_vimageI) 
           have "XP i \<union> YP i \<subseteq> XS \<union> YS"
             apply (simp add: XP_def X_def YP_def Y_def XS_def YS_def irregular_set_def image_def subset_iff)
             by (metis insert_iff linear not_le)
           then have "card (XP i \<union> YP i) \<le> card XS + card YS"
             by (meson card_Un_le card_mono finXYS order_trans)
           then show "card (XP i \<union> YP i) \<le> Suc k"
             using k' le_trans by blast
           fix x
           assume "x \<in> XP i \<union> YP i"
           then show "0 \<le> card x \<and> card x \<le> 2"
             using XP_def YP_def card_part2 by force
         qed auto
         finally show ?thesis .
       qed
       have "i' = i" if "q \<subseteq> i" "i'\<in>P" "q \<in> QS i'" for i' q
         by (metis QS_ne QS_subset_P \<open>i \<in> P\<close> disjnt_iff equals0I pairwiseD part_GP partition_on_def subset_eq that)
       then have "QinP i \<subseteq> QS i"
         by (auto simp: QinP_def Q_def)
       then have "card (QinP i) \<le> card (QS i)"
         by (simp add: card_mono that)
       also have "\<dots> \<le> 2 ^ Suc k"
         using QS_def card_cr by presburger
       finally show ?thesis .
     qed
     have "card Q \<le> card (\<Union>i\<in>P. QinP i)"
       unfolding Q_def
     proof (rule card_mono)
       show "(\<Union> (QS ` P)) \<subseteq> (\<Union>i\<in>P. QinP i)"
         using ref_QP QS_subset_P Q_def QinP_def by blast
       show "finite (\<Union>i\<in>P. QinP i)"
         by (simp add: Q_def QinP_def \<open>finite P\<close>)
     qed 
     also have "\<dots> \<le> (\<Sum>i\<in>P. 2 ^ Suc k)"
       by (smt (verit) \<open>finite P\<close> card_QP card_UN_le order_trans sum_mono)
     finally show "card Q \<le> k * 2 ^ Suc k" 
       by (simp add: cardP)
   qed
 qed
 
 subsection \<open>The Regularity Proof Itself\<close>
 
 text\<open>Szemerédi's Regularity Lemma is Theorem 3.5 in Zhao's notes.\<close>
 
 text\<open>We start with a trivial partition (one part). If it is already $\epsilon$-regular, we are done. If
 not, we refine it by applying lemma @{thm[source]"exists_refinement"} above, which increases the
 energy. We can repeat this step, but it cannot increase forever: by @{thm [source]
 mean_square_density_bounded} it cannot exceed~1. This defines an algorithm that must stop
 after at most $\epsilon^{-5}$ steps, resulting in an $\epsilon$-regular partition.\<close>
 theorem Szemeredi_Regularity_Lemma:
   assumes "\<epsilon> > 0"
   obtains M where "\<And>G. card (uverts G) > 0 \<Longrightarrow> \<exists>P. regular_partition \<epsilon> G P \<and> card P \<le> M"
 proof 
   fix G
   assume "card (uverts G) > 0"
   then obtain finG: "finite (uverts G)" and nonempty: "uverts G \<noteq> {}"
     by (simp add: card_gt_0_iff) 
   define \<Phi> where "\<Phi> \<equiv> \<lambda>Q P. refines (uverts G) Q P \<and> 
                                  mean_square_density G Q \<ge> mean_square_density G P + \<epsilon>^5 \<and> 
                                  card Q \<le> card P * 2 ^ Suc (card P)"
   define nxt where "nxt \<equiv> \<lambda>P. if regular_partition \<epsilon> G P then P else SOME Q. \<Phi> Q P"
   define iter where "iter \<equiv> \<lambda>i. (nxt ^^ i) {uverts G}"
   define last where "last \<equiv> Suc (nat\<lceil>1 / \<epsilon> ^ 5\<rceil>)"
   have iter_Suc [simp]: "iter (Suc i) = nxt (iter i)" for i
     by (simp add: iter_def)
   have \<Phi>: "\<Phi> (nxt P) P"
     if Pk: "partition_on (uverts G) P" and irreg: "\<not> regular_partition \<epsilon> G P" for P
   proof -
     have "finite_graph_partition (uverts G) P (card P)"
       by (meson Pk finG finite_elements finite_graph_partition_def)
     then show ?thesis
       using that exists_refinement [OF _ finG irreg assms] irreg Pk
       unfolding \<Phi>_def nxt_def by (smt (verit) someI)
   qed
   have partition_on: "partition_on (uverts G) (iter i)" for i
   proof (induction i)
     case 0
     then show ?case
       by (simp add: iter_def nonempty trivial_graph_partition_exists partition_on_space)
   next
     case (Suc i)
     with \<Phi> show ?case
       by (metis \<Phi>_def iter_Suc nxt_def refines_def)
   qed
   have False if irreg: "\<And>i. i\<le>last \<Longrightarrow> \<not> regular_partition \<epsilon> G (iter i)"
   proof -
     have \<Phi>_loop: "\<Phi> (nxt (iter i)) (iter i)" if "i\<le>last" for i
       using \<Phi> irreg partition_on that by blast
     have iter_grow: "mean_square_density G (iter i) \<ge> i * \<epsilon>^5" if "i\<le>last" for i
       using that
     proof (induction i)
       case (Suc i)
       then show ?case
         by (clarsimp simp: algebra_simps) (smt (verit, best) Suc_leD \<Phi>_def \<Phi>_loop)
     qed (auto simp: iter_def)
     have "last * \<epsilon>^5 \<le> mean_square_density G (iter last)"
       by (simp add: iter_grow)
     also have "\<dots> \<le> 1"
       by (meson finG finite_elements finite_graph_partition_def mean_square_density_bounded partition_on)
     finally have "real last * \<epsilon> ^ 5 \<le> 1" .
     with assms show False
       unfolding last_def by (meson lessI natceiling_lessD not_less pos_divide_less_eq zero_less_power)
   qed
   then obtain i where "i \<le> last" and "regular_partition \<epsilon> G (iter i)"
     by force
   then have reglar: "regular_partition \<epsilon> G (iter (i + d))" for d
     by (induction d) (auto simp add: nxt_def)
   define tower where "tower \<equiv> \<lambda>k. (power(2::nat) ^^ k) 2"
   have [simp]: "tower (Suc k) = 2 ^ tower k" for k
     by (simp add: tower_def)
   have iter_tower: "card (iter i) \<le> tower (2*i)" for i
   proof (induction i)
     case (Suc i)
     then have Qm: "card (iter i) \<le> tower (2 * i)"
       by simp
     then have *: "card (nxt (iter i)) \<le> card (iter i) * 2 ^ Suc (card (iter i))"
       using \<Phi> by (simp add: \<Phi>_def nxt_def partition_on)
     also have "\<dots> \<le> 2 ^ 2 ^ tower (2 * i)"
       by (metis One_nat_def Suc.IH le_tower_2 lessI numeral_2_eq_2 order.trans power_increasing_iff)
     finally show ?case
       by (simp add: Qm)
   qed (auto simp: iter_def tower_def)
   then show "\<exists>P. regular_partition \<epsilon> G P \<and> card P \<le> tower(2 * last)"
     by (metis \<open>i \<le> last\<close> nat_le_iff_add reglar)
 qed 
 
 text \<open>The actual value of the bound is visible above: a tower of exponentials of height $2(1 + \epsilon^{-5})$.\<close>
 
 end