diff --git a/src/analysis/special_functions/explicit_stirling.lean b/src/analysis/special_functions/explicit_stirling.lean
index b3471ba6db460..b244946da357f 100644
--- a/src/analysis/special_functions/explicit_stirling.lean
+++ b/src/analysis/special_functions/explicit_stirling.lean
@@ -55,6 +55,10 @@ begin
   all_goals { positivity },
 end
 
+/--
+an explicit function of the central binomial coefficient which we will show is always less than
+√π, to get a lower bound on the central binomial coefficient
+-/
 def central_binomial_lower (n : ℕ) : ℝ := central_binom n * sqrt (n + 1 / 4) / 4 ^ n
 
 lemma central_binomial_lower_monotone : monotone central_binomial_lower :=
@@ -72,6 +76,10 @@ begin
   { positivity }
 end
 
+/--
+an explicit function of the central binomial coefficient which we will show is always more than
+√π, to get an upper bound on the central binomial coefficient
+-/
 def central_binomial_upper (n : ℕ) : ℝ := central_binom n * sqrt (n + 1 / 3) / 4 ^ n
 
 lemma central_binomial_upper_monotone : antitone central_binomial_upper :=
diff --git a/src/combinatorics/simple_graph/basic_mathlib.lean b/src/combinatorics/simple_graph/basic_mathlib.lean
index 5892c69286694..0315d5b756b58 100644
--- a/src/combinatorics/simple_graph/basic_mathlib.lean
+++ b/src/combinatorics/simple_graph/basic_mathlib.lean
@@ -26,6 +26,11 @@ begin
   cases hi.ne (subsingleton.elim _ _)
 end
 
+/--
+The edge set of the complete graph on V is in bijection with the off-diagonal elements of sym2 V
+TODO: maybe this should be an equality of sets?
+and then turn it into a bijection of types
+-/
 def top_edge_set_equiv : (⊤ : simple_graph V).edge_set ≃ {a : sym2 V // ¬a.is_diag} :=
 equiv.subtype_equiv_right $ λ i, sym2.induction_on i $ λ x y, iff.rfl
 
@@ -54,6 +59,7 @@ lemma top_hom_injective (f : (⊤ : simple_graph V') →g G) :
   function.injective f :=
 λ x y h, by_contra (λ z, (f.map_rel z).ne h)
 
+/-- graph embeddings from a complete graph are in bijection with graph homomorphisms from it -/
 def top_hom_graph_equiv :
   ((⊤ : simple_graph V') ↪g G) ≃ ((⊤ : simple_graph V') →g G) :=
 { to_fun := λ f, f,
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/basic.lean b/src/combinatorics/simple_graph/exponential_ramsey/basic.lean
index 9a0a8f62fb2ae..974ecb8d590c9 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/basic.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/basic.lean
@@ -58,16 +58,111 @@ by rw [col_density, edge_density_empty_right, rat.cast_zero]
 localized "notation `red_density` χ:1024 := simple_graph.col_density χ 0" in exponential_ramsey
 localized "notation `blue_density` χ:1024 := simple_graph.col_density χ 1" in exponential_ramsey
 
+/-- the set of neighbours of x which are connected to it by edges labelled k -/
 def col_neighbors [fintype V] [decidable_eq V] [decidable_eq K] (χ : top_edge_labelling V K)
   (k : K) (x : V) : finset V :=
 neighbor_finset (χ.label_graph k) x
 
+section
+
+variables {χ : top_edge_labelling V K}
+
+namespace top_edge_labelling
+
+/-- The predicate `χ.monochromatic_between X Y k` says every edge between `X` and `Y` is labelled
+`k` by the labelling `χ`. -/
+def monochromatic_between (χ : top_edge_labelling V K) (X Y : finset V) (k : K) : Prop :=
+∀ ⦃x⦄, x ∈ X → ∀ ⦃y⦄, y ∈ Y → x ≠ y → χ.get x y = k
+
+instance [decidable_eq V] [decidable_eq K] {X Y : finset V} {k : K} :
+  decidable (monochromatic_between χ X Y k) :=
+finset.decidable_dforall_finset
+
+@[simp] lemma monochromatic_between_empty_left {Y : finset V} {k : K} :
+  χ.monochromatic_between ∅ Y k :=
+by simp [monochromatic_between]
+
+@[simp] lemma monochromatic_between_empty_right {X : finset V} {k : K} :
+  χ.monochromatic_between X ∅ k :=
+by simp [monochromatic_between]
+
+lemma monochromatic_between_singleton_left {x : V} {Y : finset V} {k : K} :
+  χ.monochromatic_between {x} Y k ↔ ∀ ⦃y⦄, y ∈ Y → x ≠ y → χ.get x y = k :=
+by simp [monochromatic_between]
+
+lemma monochromatic_between_singleton_right {y : V} {X : finset V} {k : K} :
+  χ.monochromatic_between X {y} k ↔ ∀ ⦃x⦄, x ∈ X → x ≠ y → χ.get x y = k :=
+by simp [monochromatic_between]
+
+lemma monochromatic_between_union_left [decidable_eq V] {X Y Z : finset V} {k : K} :
+  χ.monochromatic_between (X ∪ Y) Z k ↔
+    χ.monochromatic_between X Z k ∧ χ.monochromatic_between Y Z k :=
+by simp only [monochromatic_between, mem_union, or_imp_distrib, forall_and_distrib]
+
+lemma monochromatic_between_union_right [decidable_eq V] {X Y Z : finset V} {k : K} :
+  χ.monochromatic_between X (Y ∪ Z) k ↔
+    χ.monochromatic_between X Y k ∧ χ.monochromatic_between X Z k :=
+by simp only [monochromatic_between, mem_union, or_imp_distrib, forall_and_distrib]
+
+lemma monochromatic_between_self {X : finset V} {k : K} :
+  χ.monochromatic_between X X k ↔ χ.monochromatic_of X k :=
+by simp only [monochromatic_between, monochromatic_of, mem_coe]
+
+lemma _root_.disjoint.monochromatic_between {X Y : finset V} {k : K} (h : disjoint X Y) :
+  χ.monochromatic_between X Y k ↔
+    ∀ ⦃x⦄, x ∈ X → ∀ ⦃y⦄, y ∈ Y → χ.get x y (h.forall_ne_finset ‹_› ‹_›) = k :=
+forall₄_congr $ λ x hx y hy, by simp [h.forall_ne_finset hx hy]
+
+lemma monochromatic_between.subset_left {X Y Z : finset V} {k : K}
+  (hYZ : χ.monochromatic_between Y Z k) (hXY : X ⊆ Y) :
+  χ.monochromatic_between X Z k :=
+λ x hx y hy h, hYZ (hXY hx) hy _
+
+lemma monochromatic_between.subset_right {X Y Z : finset V} {k : K}
+  (hXZ : χ.monochromatic_between X Z k) (hXY : Y ⊆ Z) :
+  χ.monochromatic_between X Y k :=
+λ x hx y hy h, hXZ hx (hXY hy) _
+
+lemma monochromatic_between.subset {W X Y Z : finset V} {k : K}
+  (hWX : χ.monochromatic_between W X k) (hYW : Y ⊆ W) (hZX : Z ⊆ X) :
+  χ.monochromatic_between Y Z k :=
+λ x hx y hy h, hWX (hYW hx) (hZX hy) _
+
+lemma monochromatic_between.symm {X Y : finset V} {k : K}
+  (hXY : χ.monochromatic_between X Y k) :
+  χ.monochromatic_between Y X k :=
+λ y hy x hx h, by { rw get_swap _ _ h.symm, exact hXY hx hy _ }
+
+lemma monochromatic_between.comm {X Y : finset V} {k : K} :
+  χ.monochromatic_between Y X k ↔ χ.monochromatic_between X Y k :=
+⟨monochromatic_between.symm, monochromatic_between.symm⟩
+
+lemma monochromatic_of_union {X Y : finset V} {k : K} :
+  χ.monochromatic_of (X ∪ Y) k ↔
+    χ.monochromatic_of X k ∧ χ.monochromatic_of Y k ∧ χ.monochromatic_between X Y k :=
+begin
+  have : χ.monochromatic_between X Y k ∧ χ.monochromatic_between Y X k ↔
+    χ.monochromatic_between X Y k := (and_iff_left_of_imp (monochromatic_between.symm)),
+  rw ←this,
+  simp only [monochromatic_of, set.mem_union, or_imp_distrib, forall_and_distrib, mem_coe,
+    monochromatic_between],
+  tauto,
+end
+
+end top_edge_labelling
+
+end
+
 localized "notation `red_neighbors` χ:1024 := simple_graph.col_neighbors χ 0" in exponential_ramsey
 localized "notation `blue_neighbors` χ:1024 := simple_graph.col_neighbors χ 1" in exponential_ramsey
 
 open_locale exponential_ramsey
 
-variables [fintype V] [decidable_eq V]
+variables [decidable_eq V]
+
+section
+
+variables [fintype V]
 
 lemma mem_col_neighbors [decidable_eq K] {χ : top_edge_labelling V K} {x y : V} {k : K} :
   y ∈ col_neighbors χ k x ↔ ∃ (H : x ≠ y), χ.get x y = k :=
@@ -84,6 +179,8 @@ by rw [mem_col_neighbors, mem_col_neighbors']
 lemma not_mem_col_neighbors [decidable_eq K] {χ : top_edge_labelling V K} {x : V} {k : K} :
   x ∉ col_neighbors χ k x := not_mem_neighbor_finset_self _ _
 
+end
+
 lemma interedges_card_eq_sum {V : Type*} [decidable_eq V] [fintype V] {G : simple_graph V}
   [decidable_rel G.adj] {A B : finset V} :
   (G.interedges A B).card = ∑ x in A, (G.neighbor_finset x ∩ B).card :=
@@ -104,7 +201,7 @@ begin
   simp only [function.embedding.coe_fn_mk, mem_neighbor_finset, iff_self, implies_true_iff],
 end
 
-lemma col_density_eq_sum {K : Type*} [decidable_eq K] {χ : top_edge_labelling V K} {k : K}
+lemma col_density_eq_sum {K : Type*} [fintype V] [decidable_eq K] {χ : top_edge_labelling V K} {k : K}
   {A B : finset V} :
   col_density χ k A B = (∑ x in A, (col_neighbors χ k x ∩ B).card) / (A.card * B.card) :=
 begin
@@ -113,6 +210,10 @@ begin
   refl,
 end
 
+section
+
+variable [fintype V]
+
 /--
 Define the weight of an ordered pair for the book algorithm.
 `pair_weight χ X Y x y` corresponds to `ω(x, y)` in the paper, see equation (3).
@@ -129,6 +230,8 @@ Define the weight of a vertex for the book algorithm.
 noncomputable def weight (χ : top_edge_labelling V (fin 2)) (X Y : finset V) (x : V) : ℝ :=
 ∑ y in X.erase x, pair_weight χ X Y x y
 
+end
+
 /-- Define the function `q` from the paper, see equation (5).  -/
 noncomputable def q_function (k : ℕ) (p₀ : ℝ) (h : ℕ) : ℝ :=
 p₀ + ((1 + k^(- 1/4 : ℝ)) ^ h - 1) / k
@@ -195,99 +298,14 @@ begin
     sub_sub_sub_cancel_right, pow_succ, ←sub_one_mul, add_sub_cancel', nat.add_sub_cancel]
 end
 
-section
-
-variables {χ : top_edge_labelling V K}
-
-namespace top_edge_labelling
-
-/-- The predicate `χ.monochromatic_between X Y k` says every edge between `X` and `Y` is labelled
-`k` by the labelling `χ`. -/
-def monochromatic_between (χ : top_edge_labelling V K) (X Y : finset V) (k : K) : Prop :=
-∀ ⦃x⦄, x ∈ X → ∀ ⦃y⦄, y ∈ Y → x ≠ y → χ.get x y = k
-
-instance [decidable_eq K] {X Y : finset V} {k : K} : decidable (monochromatic_between χ X Y k) :=
-finset.decidable_dforall_finset
-
-@[simp] lemma monochromatic_between_empty_left {Y : finset V} {k : K} :
-  χ.monochromatic_between ∅ Y k :=
-by simp [monochromatic_between]
-
-@[simp] lemma monochromatic_between_empty_right {X : finset V} {k : K} :
-  χ.monochromatic_between X ∅ k :=
-by simp [monochromatic_between]
-
-lemma monochromatic_between_singleton_left {x : V} {Y : finset V} {k : K} :
-  χ.monochromatic_between {x} Y k ↔ ∀ ⦃y⦄, y ∈ Y → x ≠ y → χ.get x y = k :=
-by simp [monochromatic_between]
-
-lemma monochromatic_between_singleton_right {y : V} {X : finset V} {k : K} :
-  χ.monochromatic_between X {y} k ↔ ∀ ⦃x⦄, x ∈ X → x ≠ y → χ.get x y = k :=
-by simp [monochromatic_between]
-
-lemma monochromatic_between_union_left {X Y Z : finset V} {k : K} :
-  χ.monochromatic_between (X ∪ Y) Z k ↔
-    χ.monochromatic_between X Z k ∧ χ.monochromatic_between Y Z k :=
-by simp only [monochromatic_between, mem_union, or_imp_distrib, forall_and_distrib]
-
-lemma monochromatic_between_union_right {X Y Z : finset V} {k : K} :
-  χ.monochromatic_between X (Y ∪ Z) k ↔
-    χ.monochromatic_between X Y k ∧ χ.monochromatic_between X Z k :=
-by simp only [monochromatic_between, mem_union, or_imp_distrib, forall_and_distrib]
-
-lemma monochromatic_between_self {X : finset V} {k : K} :
-  χ.monochromatic_between X X k ↔ χ.monochromatic_of X k :=
-by simp only [monochromatic_between, monochromatic_of, mem_coe]
-
-lemma _root_.disjoint.monochromatic_between {X Y : finset V} {k : K} (h : disjoint X Y) :
-  χ.monochromatic_between X Y k ↔
-    ∀ ⦃x⦄, x ∈ X → ∀ ⦃y⦄, y ∈ Y → χ.get x y (h.forall_ne_finset ‹_› ‹_›) = k :=
-forall₄_congr $ λ x hx y hy, by simp [h.forall_ne_finset hx hy]
-
-lemma monochromatic_between.subset_left {X Y Z : finset V} {k : K}
-  (hYZ : χ.monochromatic_between Y Z k) (hXY : X ⊆ Y) :
-  χ.monochromatic_between X Z k :=
-λ x hx y hy h, hYZ (hXY hx) hy _
-
-lemma monochromatic_between.subset_right {X Y Z : finset V} {k : K}
-  (hXZ : χ.monochromatic_between X Z k) (hXY : Y ⊆ Z) :
-  χ.monochromatic_between X Y k :=
-λ x hx y hy h, hXZ hx (hXY hy) _
-
-lemma monochromatic_between.subset {W X Y Z : finset V} {k : K}
-  (hWX : χ.monochromatic_between W X k) (hYW : Y ⊆ W) (hZX : Z ⊆ X) :
-  χ.monochromatic_between Y Z k :=
-λ x hx y hy h, hWX (hYW hx) (hZX hy) _
-
-lemma monochromatic_between.symm {X Y : finset V} {k : K}
-  (hXY : χ.monochromatic_between X Y k) :
-  χ.monochromatic_between Y X k :=
-λ y hy x hx h, by { rw get_swap _ _ h.symm, exact hXY hx hy _ }
-
-lemma monochromatic_between.comm {X Y : finset V} {k : K} :
-  χ.monochromatic_between Y X k ↔ χ.monochromatic_between X Y k :=
-⟨monochromatic_between.symm, monochromatic_between.symm⟩
-
-lemma monochromatic_of_union {X Y : finset V} {k : K} :
-  χ.monochromatic_of (X ∪ Y) k ↔
-    χ.monochromatic_of X k ∧ χ.monochromatic_of Y k ∧ χ.monochromatic_between X Y k :=
-begin
-  have : χ.monochromatic_between X Y k ∧ χ.monochromatic_between Y X k ↔
-    χ.monochromatic_between X Y k := (and_iff_left_of_imp (monochromatic_between.symm)),
-  rw ←this,
-  simp only [monochromatic_of, set.mem_union, or_imp_distrib, forall_and_distrib, mem_coe,
-    monochromatic_between],
-  tauto,
-end
-
-end top_edge_labelling
-
-end
-
 variable {χ : top_edge_labelling V (fin 2)}
 
 open top_edge_labelling
 
+/--
+the quadruple of sets X,Y,A,B that we keep track of in the book algorithm, bundled with the
+properties which are needed for it
+-/
 structure book_config (χ : top_edge_labelling V (fin 2)) :=
   (X Y A B : finset V)
   (hXY : disjoint X Y)
@@ -306,6 +324,10 @@ namespace book_config
 /-- Define `p` from the paper at a given configuration. -/
 def p (C : book_config χ) : ℝ := red_density χ C.X C.Y
 
+section
+
+variable [fintype V]
+
 /-- Given a vertex set `X`, construct the initial configuration where `X` is as given. -/
 def start (X : finset V) : book_config χ :=
 begin
@@ -313,6 +335,9 @@ begin
   all_goals { simp }
 end
 
+-- todo: this instance shouldn't need fintype; just use everything empty
+instance : inhabited (book_config χ) := ⟨start ∅⟩
+
 /-- Take a red step for the book algorithm, given `x ∈ X`. -/
 def red_step_basic (C : book_config χ) (x : V) (hx : x ∈ C.X) : book_config χ :=
 { X := red_neighbors χ x ∩ C.X, Y := red_neighbors χ x ∩ C.Y, A := insert x C.A, B := C.B,
@@ -366,6 +391,10 @@ lemma red_step_basic_A {C : book_config χ} {x : V} (hx : x ∈ C.X) :
 lemma red_step_basic_B {C : book_config χ} {x : V} (hx : x ∈ C.X) :
   (red_step_basic C x hx).B = C.B := rfl
 
+end
+
+section
+
 /-- Take a big blue step for the book algorithm, given a blue book `(S, T)` contained in `X`. -/
 def big_blue_step_basic (C : book_config χ) (S T : finset V) (hS : S ⊆ C.X) (hT : T ⊆ C.X)
   (hSS : χ.monochromatic_of S 1) (hST : disjoint S T) (hST' : χ.monochromatic_between S T 1) :
@@ -390,6 +419,8 @@ def big_blue_step_basic (C : book_config χ) (S T : finset V) (hS : S ⊆ C.X) (
     exact ⟨C.blue_XB.subset_left hT, hST'.symm⟩,
   end }
 
+variable [fintype V]
+
 /-- Take a density boost step for the book algorithm, given `x ∈ X`. -/
 def density_boost_step_basic (C : book_config χ) (x : V) (hx : x ∈ C.X) : book_config χ :=
 { X := blue_neighbors χ x ∩ C.X, Y := red_neighbors χ x ∩ C.Y, A := C.A, B := insert x C.B,
@@ -439,6 +470,10 @@ lemma density_boost_step_basic_A {C : book_config χ} {x : V} (hx : x ∈ C.X) :
 lemma density_boost_step_basic_B {C : book_config χ} {x : V} (hx : x ∈ C.X) :
   (density_boost_step_basic C x hx).B = insert x C.B := rfl
 
+end
+
+section
+
 /-- Take a degree regularisation step for the book algorithm, given `U ⊆ X` for the vertices we want
 to keep in `X`. -/
 def degree_regularisation_step_basic (C : book_config χ) (U : finset V) (h : U ⊆ C.X) :
@@ -455,6 +490,8 @@ def degree_regularisation_step_basic (C : book_config χ) (U : finset V) (h : U
   blue_B := C.blue_B,
   blue_XB := C.blue_XB.subset_left h }
 
+variable [fintype V]
+
 /-- Take a degree regularisation step, choosing the set of vertices as in the paper. -/
 noncomputable def degree_regularisation_step (k : ℕ) (p₀ : ℝ) (C : book_config χ) :
   book_config χ :=
@@ -482,15 +519,19 @@ lemma degree_regularisation_step_B {k : ℕ} {p₀ : ℝ} {C : book_config χ} :
 lemma degree_regularisation_step_X_subset {k : ℕ} {p₀ : ℝ} {C : book_config χ} :
   (degree_regularisation_step k p₀ C).X ⊆ C.X := filter_subset _ _
 
+end
+
 /-- Get the set of appropriately sized blue books contained in `X`. We will take a maximal
 one of these later. -/
-noncomputable def useful_blue_books (χ : top_edge_labelling V (fin 2)) (μ : ℝ) (X : finset V) :
+noncomputable def useful_blue_books {V : Type*} [decidable_eq V] (χ : top_edge_labelling V (fin 2))
+  (μ : ℝ) (X : finset V) :
   finset (finset V × finset V) :=
 (X.powerset.product X.powerset).filter
   (λ ST, disjoint ST.1 ST.2 ∧ χ.monochromatic_of ST.1 1 ∧ χ.monochromatic_between ST.1 ST.2 1
     ∧ μ ^ ST.1.card * X.card / 2 ≤ ST.2.card)
 
-lemma mem_useful_blue_books {μ : ℝ} {X : finset V} {ST : finset V × finset V} :
+lemma mem_useful_blue_books
+  {μ : ℝ} {X : finset V} {ST : finset V × finset V} :
   ST ∈ useful_blue_books χ μ X ↔
     ST.1 ⊆ X ∧ ST.2 ⊆ X ∧ disjoint ST.1 ST.2 ∧ χ.monochromatic_of ST.1 1 ∧
       χ.monochromatic_between ST.1 ST.2 1 ∧ μ ^ ST.1.card * X.card / 2 ≤ ST.2.card :=
@@ -512,7 +553,7 @@ begin
   exact half_le_self (nat.cast_nonneg _),
 end
 
-lemma exists_blue_book_one_le_S (μ : ℝ) (X : finset V)
+lemma exists_blue_book_one_le_S [fintype V] (μ : ℝ) (X : finset V)
   (hX : ∃ x ∈ X, μ * X.card ≤ (blue_neighbors χ x ∩ X).card) :
   ∃ ST : finset V × finset V, ST ∈ useful_blue_books χ μ X ∧ 1 ≤ ST.1.card :=
 begin
@@ -536,7 +577,8 @@ begin
   positivity
 end
 
-lemma exists_maximal_blue_book_aux (χ : top_edge_labelling V (fin 2)) (μ : ℝ) (X : finset V) :
+lemma exists_maximal_blue_book_aux (χ : top_edge_labelling V (fin 2))
+  (μ : ℝ) (X : finset V) :
   ∃ (ST ∈ useful_blue_books χ μ X), ∀ (ST' ∈ useful_blue_books χ μ X),
     finset.card (prod.fst ST') ≤ finset.card (prod.fst ST) :=
 finset.exists_max_image (useful_blue_books χ μ X) (λ ST, ST.1.card) (exists_useful_blue_book _ _)
@@ -573,6 +615,10 @@ lemma get_book_max {μ : ℝ} {X : finset V} (S T : finset V)
   (hST : (S, T) ∈ useful_blue_books χ μ X) : S.card ≤ (get_book χ μ X).1.card :=
 (exists_maximal_blue_book_aux χ μ X).some_spec.some_spec (S, T) hST
 
+section
+
+variable [fintype V]
+
 lemma one_le_card_get_book_fst {μ : ℝ} {X : finset V}
   (hX : ∃ x ∈ X, μ * X.card ≤ (blue_neighbors χ x ∩ X).card) :
   1 ≤ (get_book χ μ X).1.card :=
@@ -609,6 +655,8 @@ begin
   positivity,
 end
 
+end
+
 /-- Perform a big blue step, picking an appropriate blue book. -/
 noncomputable def big_blue_step (μ : ℝ) (C : book_config χ) : book_config χ :=
 big_blue_step_basic C (get_book χ μ C.X).1 (get_book χ μ C.X).2 get_book_fst_subset
@@ -626,6 +674,10 @@ lemma big_blue_step_A {μ : ℝ} {C : book_config χ} :
 lemma big_blue_step_B {μ : ℝ} {C : book_config χ} :
   (big_blue_step μ C).B = C.B ∪ (get_book χ μ C.X).1 := rfl
 
+section
+
+variable [fintype V]
+
 /-- The set of viable central vertices. -/
 noncomputable def central_vertices (μ : ℝ) (C : book_config χ) : finset V :=
 C.X.filter (λ x, ↑(blue_neighbors χ x ∩ C.X).card ≤ μ * C.X.card)
@@ -677,8 +729,12 @@ begin
   simp,
 end
 
+end
+
 end book_config
 
+variable [fintype V]
+
 /-- The book algorithm as an infinite sequence which is eventually constantly nothing. -/
 noncomputable def algorithm_option (μ : ℝ) (k l : ℕ) (ini : book_config χ) :
     ℕ → option (book_config χ)
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/constructive.lean b/src/combinatorics/simple_graph/exponential_ramsey/constructive.lean
index 1a9d2b28090d0..a8e2de29db341 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/constructive.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/constructive.lean
@@ -16,7 +16,10 @@ namespace product
 
 open finset
 
-
+/--
+an explicit two-labelling of [k] x [l] which should, by construction, not contain an 0-labelled k+1
+or 1-labelled l+1 clique
+-/
 def my_labelling (k l : ℕ) : top_edge_labelling (fin k × fin l) (fin 2) :=
 top_edge_labelling.mk (λ x y h, if x.2 = y.2 then 0 else 1)
   (λ x y h, by simp only [@eq_comm (fin l)])
@@ -58,20 +61,10 @@ begin
   rwa [←ramsey_number_le_iff, fintype.card_prod, fintype.card_fin, fintype.card_fin, not_le] at this
 end
 
-def my_other_labelling (k l : ℕ) : top_edge_labelling (fin (k + 2) × fin l) (fin 2) :=
-top_edge_labelling.mk
-  (λ x y h,
-    if x.1 = y.1 ∨
-      ((⟦(x.1, y.1)⟧ : sym2 (fin (k + 2))) = ⟦(0, 1)⟧ ∧ x.2 = y.2) ∨
-      ((⟦(x.1, y.1)⟧ : sym2 (fin (k + 2))) ≠ ⟦(0, 1)⟧ ∧ x.2 ≠ y.2)
-    then 1
-    else 0)
-  begin
-    intros x y h,
-    refine if_congr _ rfl rfl,
-    rw [sym2.eq_swap, ne.def y.2, @eq_comm _ y.1, @eq_comm _ y.2],
-  end
-
+/--
+an explicit two-labelling of α x [l] which should, by construction, not contain an 0-labelled |α|
+clique or 1-labelled l+2 clique
+-/
 def my_other_labelling' (α : Type*) [decidable_eq α] (l : ℕ) (a b : α) :
   top_edge_labelling (α × fin l) (fin 2) :=
 top_edge_labelling.mk
@@ -159,10 +152,11 @@ begin
   rw [←h₂ z hxz.symm, h₃ z hyz.symm],
 end
 
-lemma is_ramsey_valid_my_other_labelling_one {α : Type*} [decidable_eq α] [fintype α] {l : ℕ}
+lemma is_ramsey_valid_my_other_labelling_one {α : Type*} [decidable_eq α] [finite α] {l : ℕ}
   {m : finset (α × fin l)} (x y : α) (h : x ≠ y) :
   ¬ ((my_other_labelling' α l x y).monochromatic_of m 1 ∧ l + 2 = m.card) :=
 begin
+  casesI nonempty_fintype α,
   rintro ⟨hm, hm'⟩,
   let f' : α → finset (α × fin l) := λ i, m.filter (λ x, x.1 = i),
   -- let s₁₂ : finset α := {x}ᶜ,
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/log2_estimates.lean b/src/combinatorics/simple_graph/exponential_ramsey/log2_estimates.lean
index ae6155511809d..6c81b5b415d3e 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/log2_estimates.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/log2_estimates.lean
@@ -33,6 +33,7 @@ lemma logb_div_base' {b x : ℝ} (hb : 0 < b) (hb' : b ≠ 1) (hx : x ≠ 0) :
   logb b (x / b) = logb b x - 1 :=
 by rw [logb_div hx hb.ne', logb_base hb hb']
 
+/-- the form of goal which is used to prove log2 estimates -/
 def log_base2_goal (x₁ x₂ a₁ a₂ : ℝ) : Prop :=
 0 < x₁ → x₁ ≤ x₂ → a₁ < logb 2 x₁ ∧ logb 2 x₂ < a₂
 
@@ -86,6 +87,7 @@ namespace interactive
 
 setup_tactic_parser
 
+/-- a quick macro to simplify log2 estimate proofs -/
 meta def weaken (t u : parse parser.pexpr) : tactic unit :=
 `[refine log_base2_weaken %%t %%u _ (by norm_num1) (by norm_num1) (by norm_num1)]
 
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/necessary_log_estimates.lean b/src/combinatorics/simple_graph/exponential_ramsey/necessary_log_estimates.lean
index d30ab9c97edfa..3a02b6f5c19ce 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/necessary_log_estimates.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/necessary_log_estimates.lean
@@ -462,6 +462,7 @@ end
 section values
 open real
 
+/-- the first x value to estimate log2 for -/
 noncomputable def x_value : ℝ := (0.4339 + 2727 / 8000) / 0.4339
 lemma x_value_eq : x_value = 30991 / 17356 := by norm_num [x_value]
 
@@ -535,9 +536,11 @@ end
 lemma logb_two_x_value_interval : logb 2 x_value ∈ Icc (0.8364148 : ℝ) 0.8364149 :=
 ⟨logb_x_value.1.le, logb_x_value.2.le⟩
 
+/-- the second x value to estimate log2 for -/
 noncomputable def x_value2 : ℝ := 1 / (2 - 0.817)
 lemma x_value2_eq : x_value2 = 1000 / 1183 := by norm_num [x_value2]
 
+/-- the third x value to estimate log2 for -/
 noncomputable def x_value3 : ℝ := 1 - 1 / (2 - 0.817)
 lemma x_value3_eq : x_value3 = 183 / 1183 := by norm_num [x_value3]
 
@@ -658,6 +661,7 @@ end values
 open real simple_graph
 
 -- this expression is nicer to compare to g
+/-- the special case of g on the line -/
 noncomputable def g' (y : ℝ) := logb 2 (5 / 2) + (3 / 5 * y + 0.5454) * logb 2 (5 / 3) +
     y * logb 2 ((y + 2727 / 8000) / ((25 / 16) * y))
 
@@ -726,11 +730,11 @@ begin
   linarith
 end
 
--- for diff
+/-- an expression for the derivative of g' which is convenient to differentiate -/
 noncomputable def g'_deriv (y : ℝ) : ℝ := ((4 - 7 / 5 * logb 2 5 - 3 / 5 * logb 2 3) +
     ((logb 2 (y + 2727 / 8000) - logb 2 y) - 2727 / 8000 / log 2 / (y + 2727 / 8000)))
 
--- for eval
+/-- an expression for the derivative of g' which is convenient to evaluate -/
 noncomputable def g'_deriv_alt (y : ℝ) : ℝ := ((4 - 7 / 5 * logb 2 5 - 3 / 5 * logb 2 3) +
     ((logb 2 ((y + 2727 / 8000) / y)) - 2727 / 8000 / (y + 2727 / 8000) * (1 / log 2)))
 
@@ -874,15 +878,15 @@ begin
     linarith only [this, hy.2] },
 end
 
-lemma claim_a2 {x y : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 0.75)
+lemma claim_a2 {x y : ℝ} (hy : y ∈ Icc (0 : ℝ) 0.75)
   (h : x = 3 / 5 * y + 0.5454) :
   simple_graph.g x y < 1.9993 :=
 begin
-  clear hx,
   rw [g_line h],
   exact claim_a2_aux hy
 end
 
+/-- the function `f` on the line -/
 noncomputable def f' (x : ℝ) : ℝ := 8 / 3 * x - 0.909 + (2 - x) * bin_ent 2 (1 / (2 - x))
 
 lemma continuous_f' : continuous f' :=
@@ -948,7 +952,7 @@ begin
   linarith only [this],
 end
 
-lemma claim_a3 {x y : ℝ} (hx : x ∈ Icc (0 : ℝ) 0.75) (hy : y ∈ Icc (0 : ℝ) 0.75)
+lemma claim_a3 {x y : ℝ} (hx : x ∈ Icc (0 : ℝ) 0.75)
   (h : x = 3 / 5 * y + 0.5454) :
   f1 x y < 1.9993 :=
 begin
@@ -957,11 +961,13 @@ begin
   exact f'_max.trans_le (by norm_num1),
 end
 
+/-- an expression for f2 on the line -/
 noncomputable def f2' (x : ℝ) : ℝ := f' x - 1 / (log 2 * 40) * (1 - 1 / (2 - x))
 
 lemma f2'_eq {x : ℝ} : f2' x = f' x - (1 / log 2) * ((1 / 40) * (1 - 1 / (2 - x))) :=
 by rw [f2', ←one_div_mul_one_div, mul_assoc]
 
+/-- an expression for the derivative of f2 -/
 noncomputable def f2'_deriv (x : ℝ) : ℝ :=
   8 / 3 + logb 2 ((1 - x) / (2 - x)) + 1 / (log 2 * 40) * (1 / (2 - x) ^ 2)
 
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section10.lean b/src/combinatorics/simple_graph/exponential_ramsey/section10.lean
index 5044ee2d7c6a8..2fe2ef836ec96 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section10.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section10.lean
@@ -276,7 +276,7 @@ begin
     exact (end_state γ k l ini).red_XYA.symm.subset_right
       (hm₀.trans (finset.subset_union_right _ _)) },
   rwa [finset.card_union_eq, add_le_add_iff_right],
-  { exact t_le_A_card γ (hk₀ k hlk).ne' (hk₀ l le_rfl).ne' ini },
+  { exact t_le_A_card γ k l ini },
   exact (end_state γ k l ini).hYA.symm.mono_right hm₀,
 end
 
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section11.lean b/src/combinatorics/simple_graph/exponential_ramsey/section11.lean
index 4e40cd8ef8657..e5e1c98ad9fdf 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section11.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section11.lean
@@ -356,7 +356,7 @@ begin
   clear hf₁ hf₂ hf₅,
   have hsk : (density_steps μ k k ini).card ≤ k,
   { exact (four_four_blue_density μ hk₀.ne' hk₀.ne' hχ ini).trans' le_add_self },
-  have htk : (red_steps μ k k ini).card ≤ k := four_four_red μ hk₀.ne' hk₀.ne' hχ ini,
+  have htk : (red_steps μ k k ini).card ≤ k := four_four_red μ hχ ini,
   specialize hf₁' n hn'' χ hχ ini hini hn',
   specialize hf₂' k le_rfl μ le_rfl le_rfl n χ hχ ini hini,
   specialize hβ k le_rfl μ le_rfl le_rfl n χ ini hini,
@@ -388,7 +388,7 @@ begin
     exact hf₅' (hf₂' hk) },
 end
 
-lemma Y_small {μ k n} (hk : k ≠ 0) {χ : top_edge_labelling (fin n) (fin 2)} {ini : book_config χ}
+lemma Y_small {μ k n} {χ : top_edge_labelling (fin n) (fin 2)} {ini : book_config χ}
   (hχ : ¬ (∃ (m : finset (fin n)) (c : fin 2), χ.monochromatic_of m c ∧ ![k, k] c ≤ m.card))
   {i : ℕ} (hi : i ≤ final_step μ k k ini) :
   (algorithm μ k k ini i).Y.card ≤
@@ -408,7 +408,7 @@ begin
     refine (algorithm μ k k ini i).red_XYA.subset_left _,
     exact hm.1.trans (finset.subset_union_right _ _) },
   rw [finset.card_union_eq],
-  { exact add_le_add_left (four_four_red_aux hk hk _ _ hi) _ },
+  { exact add_le_add_left (four_four_red_aux _ _ hi) _ },
   exact (algorithm μ k k ini i).hYA.mono_left hm.1,
 end
 
@@ -434,7 +434,7 @@ begin
     n hn χ hχ ini hini hn' i hi,
   clear hf',
   specialize hf k le_rfl μ le_rfl le_rfl n χ hχ ini hini i hi,
-  replace hf := hf.trans (nat.cast_le.2 (Y_small hk₀.ne' hχ hi)),
+  replace hf := hf.trans (nat.cast_le.2 (Y_small hχ hi)),
   rw mul_right_comm at hf,
   have : 2 ^ (- ((red_steps μ k k ini ∩ finset.range i).card +
                  (density_steps μ k k ini ∩ finset.range i).card : ℝ)) ≤
@@ -929,7 +929,7 @@ begin
   suffices : (red_steps (2 / 5) k k ini).card ≤ k,
   { refine ⟨this, div_le_one_of_le _ (nat.cast_nonneg _)⟩,
     rwa nat.cast_le },
-  exact four_four_red _ hk₀.ne' hk₀.ne' hχ _
+  exact four_four_red _ hχ _
 end
 
 lemma y_le_3_4 :
@@ -950,7 +950,7 @@ begin
   have : ((red_steps (2 / 5) k k ini).card : ℝ) / k ≤ 1,
   { refine div_le_one_of_le _ (nat.cast_nonneg _),
     rw nat.cast_le,
-    exact four_four_red _ hk₀.ne' hk₀.ne' hχ _ },
+    exact four_four_red _ hχ _ },
   norm_num1,
   linarith only [this],
 end
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section12.lean b/src/combinatorics/simple_graph/exponential_ramsey/section12.lean
index e900850df7106..b6da1af57575b 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section12.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section12.lean
@@ -85,7 +85,7 @@ begin
   rw [f],
   split_ifs with h₁ h₁,
   { exact claim_a4 ⟨h₁, hx.2⟩ hy h },
-  exact claim_a3 ⟨hx.1, le_of_not_le h₁⟩ hy h,
+  exact claim_a3 ⟨hx.1, le_of_not_le h₁⟩ h,
 end
 
 lemma main_calculation {x y : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 0.75) :
@@ -98,7 +98,7 @@ begin
   set xy := 3 / 5 * y + 0.5454,
   cases le_total x xy,
   { refine (min_le_right _ _).trans_lt _,
-    refine (claim_a2 hxy hy rfl).trans_le' _,
+    refine (claim_a2 hy rfl).trans_le' _,
     exact g_monotone hy.1 (hy.2.trans (by norm_num1)) hx.1 h },
   refine (min_le_left _ _).trans_lt _,
   refine (claim_a34 hxy hy rfl).trans_le' _,
@@ -162,4 +162,35 @@ theorem theorem_one' :
 theorem theorem_one'' : ∃ c < 4, ∀ᶠ k : ℕ in at_top, (ramsey_number ![k, k] : ℝ) ≤ c ^ k :=
 ⟨3.999, by norm_num1, exponential_ramsey⟩
 
+-- -- (4 ^ x / sqrt x) ^ (1 / x) ≤ 4 - c
+-- -- 4 * (1 / sqrt x) ^ (1 / x) ≤ 4 - c
+-- -- (1 / sqrt x) ^ (1 / x) ≤ 1 - c / 4
+-- -- c / 4 ≤ 1 - (1 / sqrt x) ^ (1 / x)
+-- -- c ≤ 4 - 4 * (1 / sqrt x) ^ (1 / x)
+-- theorem global_bound : ∃ ε > 0, ∀ k, (ramsey_number ![k, k] : ℝ) ≤ (4 - ε) ^ k :=
+-- begin
+--   obtain ⟨K, hK⟩ := exponential_ramsey',
+--   rcases K.eq_zero_or_pos with rfl | hK',
+--   { exact ⟨0.001, by norm_num1, λ k, (hK _ (by simp)).trans (by norm_num) ⟩ },
+--   let c := 4 - 4 * (1 / sqrt K) ^ (1 / K : ℝ),
+--   have : 0 < c,
+--   { rw [sub_pos, one_div, inv_rpow (sqrt_nonneg _), mul_lt_iff_lt_one_right],
+--     swap, { norm_num1 },
+--     refine inv_lt_one _,
+--     refine one_lt_rpow _ (by positivity),
+--     simp
+--     -- refine one_lt_p
+
+--     -- simp only [one_div, inv_pow, mul_lt_iff_lt_one_right, zero_lt_bit0, zero_lt_one],
+
+--   },
+--   refine ⟨min 0.001 c, lt_min (by norm_num1) sorry, _⟩,
+--   intro k,
+--   cases le_total K k,
+--   { refine (hK k h).trans _,
+--     refine pow_le_pow_of_le_left (by norm_num1) sorry _ },
+--   refine diagonal_ramsey_upper_bound_simpler.trans _,
+
+-- end
+
 end simple_graph
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section4.lean b/src/combinatorics/simple_graph/exponential_ramsey/section4.lean
index 9aa59992e877c..15348fb3bcb83 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section4.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section4.lean
@@ -74,6 +74,7 @@ begin
   exact hf.2 hx hy ha hb hab,
 end
 
+/-- the descending factorial but with a more general setting -/
 def desc_factorial {α : Type*} [has_one α] [has_mul α] [has_sub α] [has_nat_cast α] (x : α) : ℕ → α
 | 0 := 1
 | (k + 1) := (x - k) * desc_factorial k
@@ -168,6 +169,7 @@ begin
 end
 
 -- is equal to desc_factorial for all naturals x, and for all x ≥ k - 1
+/-- a variant of the descending factorial which truncates at k-1 -/
 noncomputable def my_desc_factorial (x : ℝ) (k : ℕ) : ℝ :=
 if x < k - 1 then 0 else desc_factorial x k
 
@@ -208,6 +210,7 @@ begin
   exact nat.pred_lt hk,
 end
 
+/-- a definition of the generalized binomial coefficient -/
 noncomputable def my_generalized_binomial (x : ℝ) (k : ℕ) : ℝ :=
 (k.factorial : ℝ)⁻¹ • my_desc_factorial x k
 
@@ -588,6 +591,7 @@ begin
   rwa nat.cast_pos,
 end
 
+/-- the set of vertices which are connected to S by only blue edges -/
 def common_blues (χ : top_edge_labelling V (fin 2)) (S : finset V) :
   finset V := univ.filter (λ i, ∀ j ∈ S, i ∈ blue_neighbors χ j)
 
@@ -964,7 +968,7 @@ begin
   rwa nat.cast_pos
 end
 
-lemma four_four_red_aux {μ : ℝ} {k l : ℕ} (hk : k ≠ 0) (hl : l ≠ 0)
+lemma four_four_red_aux {μ : ℝ} {k l : ℕ}
   (ini : book_config χ) (i : ℕ) (hi : i ≤ final_step μ k l ini) :
   (red_steps μ k l ini ∩ range i).card ≤ (algorithm μ k l ini i).A.card :=
 begin
@@ -1019,10 +1023,10 @@ begin
   exact book_config.get_central_vertex_mem_X _ _ _,
 end
 
-lemma t_le_A_card (μ : ℝ) {k l : ℕ} (hk : k ≠ 0) (hl : l ≠ 0) (ini : book_config χ) :
+lemma t_le_A_card (μ : ℝ) (k l : ℕ) (ini : book_config χ) :
   (red_steps μ k l ini).card ≤ (end_state μ k l ini).A.card :=
 begin
-  have hl := four_four_red_aux hk hl ini (final_step μ k l ini) le_rfl,
+  have hl := four_four_red_aux ini (final_step μ k l ini) le_rfl,
   have : red_steps μ k l ini ∩ range (final_step μ k l ini) = red_steps μ k l ini,
   { rw [inter_eq_left_iff_subset],
     exact red_steps_subset_red_or_density_steps.trans (filter_subset _ _) },
@@ -1030,12 +1034,12 @@ begin
 end
 
 -- observation 4.4
-lemma four_four_red (μ : ℝ) {k l : ℕ} (hk : k ≠ 0) (hl : l ≠ 0)
+lemma four_four_red (μ : ℝ) {k l : ℕ}
   (h : ¬ (∃ (m : finset V) (c : fin 2), χ.monochromatic_of m c ∧ ![k, l] c ≤ m.card))
   (ini : book_config χ) :
   (red_steps μ k l ini).card ≤ k :=
 begin
-  have hl := t_le_A_card μ hk hl ini,
+  have hl := t_le_A_card μ k l ini,
   simp only [fin.exists_fin_two, matrix.cons_val_zero, matrix.cons_val_one, matrix.head_cons,
     exists_or_distrib, not_or_distrib, not_exists, not_and, not_le] at h,
   exact hl.trans (h.1 _ (end_state μ k l ini).red_A).le,
@@ -1069,7 +1073,7 @@ lemma four_four_degree (μ : ℝ) {k l : ℕ} (hk : k ≠ 0) (hl : l ≠ 0)
 begin
   refine (num_degree_steps_le_add).trans _,
   rw [add_le_add_iff_right, add_assoc],
-  exact add_le_add (four_four_red μ hk hl h _) (four_four_blue_density μ hk hl h _),
+  exact add_le_add (four_four_red μ h _) (four_four_blue_density μ hk hl h _),
 end
 
 end simple_graph
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section6.lean b/src/combinatorics/simple_graph/exponential_ramsey/section6.lean
index f369adaf12e87..740bc61000c6b 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section6.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section6.lean
@@ -134,7 +134,8 @@ begin
   exact mul_nonneg (rpow_nonneg_of_nonneg (nat.cast_nonneg _) _) (α_nonneg _ _),
 end
 
-lemma book_config.get_book_snd_nonempty {μ : ℝ} (hμ₀ : 0 < μ) {X : finset V} (hX : X.nonempty) :
+lemma book_config.get_book_snd_nonempty {V : Type*} [decidable_eq V] {χ} {μ : ℝ} (hμ₀ : 0 < μ)
+  {X : finset V} (hX : X.nonempty) :
   (book_config.get_book χ μ X).2.nonempty :=
 begin
   rw [←card_pos, ←@nat.cast_pos ℝ],
@@ -622,7 +623,7 @@ begin
   have : (RZ.card : ℝ) ≤ k,
   { rw nat.cast_le,
     refine (card_le_of_subset (filter_subset _ _)).trans _,
-    exact four_four_red μ (hl₀.trans_le hlk).ne' hl₀.ne' hχ ini },
+    exact four_four_red μ hχ ini },
   rw [nsmul_eq_mul],
   refine (mul_le_mul_of_nonneg_right this _).trans_eq _,
   { positivity },
@@ -1051,7 +1052,7 @@ begin
   { rw [two_mul],
     refine add_le_add _ _,
     { refine (card_le_of_subset (inter_subset_left _ _)).trans _,
-      exact (four_four_red μ (hl₀ _ hlk).ne' (hl₀ _ le_rfl).ne' hχ ini) },
+      exact (four_four_red μ hχ ini) },
     { refine (card_le_of_subset (inter_subset_left _ _)).trans _,
       have := (four_four_blue_density μ (hl₀ _ hlk).ne' (hl₀ _ le_rfl).ne' hχ ini),
       exact hlk.trans' (this.trans' le_add_self) } },
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section7.lean b/src/combinatorics/simple_graph/exponential_ramsey/section7.lean
index 477e38bdd9d31..1579162b62f48 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section7.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section7.lean
@@ -127,7 +127,7 @@ begin
   { rw [neg_div, neg_div, neg_le_neg_iff],
     exact div_le_div_of_le_left (by norm_num1) (sub_pos_of_lt hμ₁) (sub_le_sub_left hμu _) },
   { rw nat.cast_le,
-    exact four_four_red μ (hk₀ k hlk).ne' (hk₀ l le_rfl).ne' hχ ini },
+    exact four_four_red μ hχ ini },
   exact div_nonpos_of_nonpos_of_nonneg (by norm_num) (sub_pos_of_lt (hμu.trans_lt hμ₁)).le,
 end
 
@@ -413,7 +413,7 @@ begin
   filter_upwards [top_adjuster (eventually_gt_at_top 0),
     six_five_red, six_five_degree] with l hl₀ hk hk'
     k hlk μ n χ hχ ini,
-  have := four_four_red μ (hl₀ k hlk).ne' (hl₀ l le_rfl).ne' hχ ini,
+  have := four_four_red μ hχ ini,
   rw ←@nat.cast_le ℝ at this,
   refine (mul_le_mul_of_nonpos_left this (by norm_num1)).trans _,
   rw [mul_comm, ←nsmul_eq_mul],
@@ -1061,7 +1061,7 @@ begin
   have h₁ : (-2 : ℝ) * k ≤ ∑ i in red_or_density_steps μ k l ini,
     ((height k ini.p (algorithm μ k l ini (i + 1)).p : ℝ) -
       height k ini.p (algorithm μ k l ini i).p),
-  { have := four_four_red μ (hl₀ k hlk).ne' (hl₀ l le_rfl).ne' hχ ini,
+  { have := four_four_red μ hχ ini,
     rw ←@nat.cast_le ℝ at this,
     refine (mul_le_mul_of_nonpos_left this (by norm_num1)).trans _,
     rw [mul_comm, ←nsmul_eq_mul, ←red_steps_union_density_steps,
@@ -1270,7 +1270,7 @@ begin
     k hlk μ n χ hχ ini,
   refine (card_nsmul_le_sum _ _ _ (hr k hlk μ n χ hχ ini)).trans' _,
   rw [nsmul_eq_mul', neg_mul, neg_mul, neg_mul, neg_le_neg_iff],
-  refine mul_le_mul _ (nat.cast_le.2 (four_four_red μ (h₀ _ hlk).ne' (h₀ _ le_rfl).ne' hχ ini))
+  refine mul_le_mul _ (nat.cast_le.2 (four_four_red μ hχ ini))
     (nat.cast_nonneg _) (mul_nonneg zero_lt_two.le (α_nonneg _ _)),
   rw [α_one, α_function, mul_div_assoc', mul_comm, nat.add_succ_sub_one],
   refine div_le_div_of_le (nat.cast_nonneg _) (mul_le_mul_of_nonneg_right _ (by positivity)),
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section8.lean b/src/combinatorics/simple_graph/exponential_ramsey/section8.lean
index 8071e1254131d..cc0e16ed6858c 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section8.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section8.lean
@@ -793,8 +793,8 @@ begin
   refine hl.trans _,
   refine (add_le_add hk₂ (mul_le_mul_of_nonneg_right hk₁ (nat.cast_nonneg _))).trans _,
   rw [add_comm, one_add_mul, add_assoc, add_le_add_iff_left, ←le_sub_iff_add_le, ←sub_mul],
-  refine (mul_le_mul_of_nonneg_left (nat.cast_le.2 (four_four_red μ (hk₀ _ hlk).ne'
-    (hk₀ _ le_rfl).ne' hχ ini)) (by positivity)).trans _,
+  refine (mul_le_mul_of_nonneg_left (nat.cast_le.2 (four_four_red μ hχ ini))
+    (by positivity)).trans _,
   rw [mul_assoc, ←rpow_add_one],
   { norm_num },
   rw nat.cast_ne_zero,
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section9.lean b/src/combinatorics/simple_graph/exponential_ramsey/section9.lean
index b5c42eb4b45c1..479aab21e202d 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section9.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section9.lean
@@ -443,7 +443,7 @@ begin
       ←inv_rpow (sub_nonneg_of_le hγ₁.le)],
     refine rpow_le_rpow (exp_pos _).le (exp_le_one_sub_inv hγ₁) (sub_nonneg_of_le _),
     rw nat.cast_le,
-    exact four_four_red _ (hk₀ _ hlk).ne' (hk₀ _ le_rfl).ne' hχ _ },
+    exact four_four_red _ hχ _ },
   rw mul_right_comm at h₁,
   clear hn hδ hχ hini hn' hγ,
   replace h₁ := (mul_le_mul_of_nonneg_left this (by positivity)).trans h₁,
@@ -987,7 +987,7 @@ begin
   specialize hβ₀ k hlk γ hγl hγu n χ ini hp₀',
   specialize hf₂ k γ η hγl hη hγη n χ hχ ini hini hγu hγ₁ hlk hp₀',
   have htk : (red_steps γ k l ini).card ≤ k :=
-    four_four_red _ (hk₀ _ hlk).ne' (hk₀ _ le_rfl).ne' hχ _,
+    four_four_red _ hχ _,
   have : 2 ^ (-2 : ℝ) * (n : ℝ) ≤ ini.Y.card,
   { refine (nat.cast_le.2 hn').trans' ((ge_floor _).trans_eq' _),
     { rw [one_le_div (zero_lt_two' ℝ)],
@@ -1572,7 +1572,7 @@ begin
     refine ⟨(end_state γ k l ini).red_A, hm₁, _⟩,
     exact (end_state γ k l ini).red_XYA.symm.subset_right (hm₀.trans (subset_union_right _ _)) },
   rwa [card_union_eq, add_le_add_iff_right],
-  { exact t_le_A_card γ (hk₀ k hlk).ne' (hk₀ l le_rfl).ne' ini },
+  { exact t_le_A_card γ k l ini },
   exact (end_state γ k l ini).hYA.symm.mono_right hm₀,
 end
 
diff --git a/src/combinatorics/simple_graph/graph_probability.lean b/src/combinatorics/simple_graph/graph_probability.lean
index 86040088a2c12..6f31dcd093bac 100644
--- a/src/combinatorics/simple_graph/graph_probability.lean
+++ b/src/combinatorics/simple_graph/graph_probability.lean
@@ -9,6 +9,7 @@ import data.finset.locally_finite
 import analysis.special_functions.explicit_stirling
 import analysis.asymptotics.asymptotics
 import data.complex.exponential_bounds
+import data.real.pi.bounds
 
 /-!
 # Asymptotic lower bounds on ramsey numbers by probabilistic arguments
@@ -34,22 +35,21 @@ begin
   simp,
 end
 
-@[simp] lemma edge_finset_bot' [decidable_eq V]
-  [fintype (edge_set (⊥ : simple_graph V))] :
+lemma edge_finset_bot' [fintype (edge_set (⊥ : simple_graph V))] :
   (⊥ : simple_graph V).edge_finset = ∅ :=
 by simp [edge_finset]
 
-@[simp] lemma edge_finset_sup' [decidable_eq V]
+lemma edge_finset_sup' [decidable_eq V]
   [fintype (edge_set G₁)] [fintype (edge_set G₂)] [fintype (edge_set (G₁ ⊔ G₂))]:
   (G₁ ⊔ G₂).edge_finset = G₁.edge_finset ∪ G₂.edge_finset :=
 by simp [edge_finset]
 
-@[simp] lemma edge_finset_inf' [decidable_eq V]
+lemma edge_finset_inf' [decidable_eq V]
   [fintype (edge_set G₁)] [fintype (edge_set G₂)] [fintype (edge_set (G₁ ⊓ G₂))] :
   (G₁ ⊓ G₂).edge_finset = G₁.edge_finset ∩ G₂.edge_finset :=
 by simp [edge_finset]
 
-@[simp] lemma edge_finset_sdiff' [decidable_eq V]
+lemma edge_finset_sdiff' [decidable_eq V]
   [fintype (edge_set G₁)] [fintype (edge_set G₂)] [fintype (edge_set (G₁ \ G₂))] :
   (G₁ \ G₂).edge_finset = G₁.edge_finset \ G₂.edge_finset :=
 by simp [edge_finset]
@@ -114,26 +114,28 @@ begin
   apply not_is_diag_of_mem_edge_set
 end
 
-variables [fintype V] {p : ℝ} {s : finset (sym2 V)}
+variables {p : ℝ} {s : finset (sym2 V)}
 
-def weighting_aux (p : ℝ) (s : finset (sym2 V)) : ℝ :=
+/-- a helper function for the weighting associated to a simple graph -/
+def weighting_aux [fintype V] (p : ℝ) (s : finset (sym2 V)) : ℝ :=
 p ^ s.card * (1 - p) ^ ((card V).choose 2 - s.card)
 
-lemma weighting_aux_pos (hp₀ : 0 < p) (hp₁ : p < 1) : 0 < weighting_aux p s :=
+lemma weighting_aux_pos [fintype V] (hp₀ : 0 < p) (hp₁ : p < 1) : 0 < weighting_aux p s :=
 mul_pos (pow_pos hp₀ _) (pow_pos (sub_pos_of_lt hp₁) _)
 
+/-- the probability of the simple graph G appearing in the G(|V|,p) model of random graphs -/
 def weighting (V : Type*) [fintype V] (p : ℝ) (G : simple_graph V) [fintype G.edge_set] :
   ℝ := weighting_aux p G.edge_finset
 
-lemma weighting_pos [fintype G.edge_set] (hp₀ : 0 < p) (hp₁ : p < 1) :
+lemma weighting_pos [fintype V] [fintype G.edge_set] (hp₀ : 0 < p) (hp₁ : p < 1) :
   0 < weighting V p G :=
 weighting_aux_pos hp₀ hp₁
 
-lemma weighting_eq [fintype G.edge_set] [fintype Gᶜ.edge_set] :
+lemma weighting_eq [fintype V] [fintype G.edge_set] [fintype Gᶜ.edge_set] :
   weighting V p G = p ^ G.edge_finset.card * (1 - p) ^ Gᶜ.edge_finset.card :=
 by rw [weighting, weighting_aux, card_compl_edge_finset_eq]
 
-lemma weighting_compl [fintype G.edge_set] [fintype Gᶜ.edge_set] :
+lemma weighting_compl [fintype V] [fintype G.edge_set] [fintype Gᶜ.edge_set] (p : ℝ) :
   weighting V (1 - p) Gᶜ = weighting V p G :=
 begin
   rw [weighting, weighting, weighting_aux, weighting_aux, sub_sub_self,
@@ -174,7 +176,8 @@ section
 
 open_locale classical
 
-lemma weighting_aux_sum_between [decidable_eq V] (H₁ H₂ : simple_graph V) (h : H₁ ≤ H₂) :
+lemma weighting_aux_sum_between [fintype V] [decidable_eq V] (H₁ H₂ : simple_graph V)
+  (h : H₁ ≤ H₂) :
   ∑ G in finset.Icc H₁ H₂, weighting V p G =
     p ^ H₁.edge_finset.card * (1 - p) ^ H₂ᶜ.edge_finset.card :=
 begin
@@ -242,7 +245,7 @@ begin
   exact union_subset hx.2 (edge_finset_subset_edge_finset.2 h),
 end
 
-lemma sum_weighting : ∑ G, weighting V p G = 1 :=
+lemma sum_weighting [fintype V] : ∑ G, weighting V p G = 1 :=
 begin
   have : Icc (⊥ : simple_graph V) ⊤ = finset.univ,
   { rw [←coe_inj, coe_Icc, set.Icc_bot_top, coe_univ] },
@@ -270,9 +273,11 @@ begin
   exact (fintype.card_of_bijective this).symm,
 end
 
+/-- is s a clique in G -/
 def clique_on (G : simple_graph V) (s : set V) : Prop :=
 spanning_coe (⊤ : simple_graph s) ≤ G
 
+/-- is s independent in G -/
 def indep_on (G : simple_graph V) (t : set V) : Prop :=
 G ≤ (spanning_coe (⊤ : simple_graph t))ᶜ
 
@@ -282,11 +287,12 @@ by rw [clique_on, indep_on, le_compl_comm]
 lemma indep_on_iff {t : set V} : indep_on G t ↔ disjoint G (spanning_coe (⊤ : simple_graph t)) :=
 by rw [indep_on, le_compl_iff_disjoint_right]
 
-instance decidable_adj_map {V' : Type*} [decidable_eq V'] {G : simple_graph V}
+instance decidable_adj_map [fintype V] {V' : Type*} [decidable_eq V'] {G : simple_graph V}
   [decidable_rel G.adj] {f : V ↪ V'} : decidable_rel (G.map f).adj :=
 λ x y, decidable_of_iff' _ (G.map_adj f _ _)
 
-lemma card_edge_set_spanning_coe_top [decidable_eq V] (s : finset V) :
+-- todo: lhs should probably have an explicit fintype instance
+lemma card_edge_set_spanning_coe_top [fintype V] [decidable_eq V] (s : finset V) :
   fintype.card (spanning_coe (⊤ : simple_graph s)).edge_set = s.card.choose 2 :=
 begin
   rw [card_edge_set_map, card_top_edge_set],
@@ -294,19 +300,20 @@ begin
   rw fintype.card_coe,
 end
 
-instance decidable_le {H : simple_graph V} [decidable_rel G.adj] [decidable_rel H.adj] :
+instance decidable_le [fintype V] {H : simple_graph V} [decidable_rel G.adj] [decidable_rel H.adj] :
   decidable (G ≤ H) :=
 fintype.decidable_forall_fintype
 
-instance decidable_pred_clique_on [decidable_eq V] [decidable_rel G.adj] :
+instance decidable_pred_clique_on [fintype V] [decidable_eq V] [decidable_rel G.adj] :
   decidable_pred (λ s : finset V, clique_on G s) :=
 λ s, simple_graph.decidable_le
 
-instance decidable_pred_indep_on [decidable_eq V] [decidable_rel G.adj] :
+instance decidable_pred_indep_on [fintype V] [decidable_eq V] [decidable_rel G.adj] :
   decidable_pred (λ s : finset V, indep_on G s) :=
 λ s, simple_graph.decidable_le
 
-lemma le.def {G H : simple_graph V} : G ≤ H ↔ ∀ ⦃x y : V⦄, G.adj x y → H.adj x y := iff.rfl
+lemma le.def {V : Type*} {G H : simple_graph V} : G ≤ H ↔ ∀ ⦃x y : V⦄, G.adj x y → H.adj x y :=
+iff.rfl
 
 lemma fin.fin_two_eq_zero_iff_ne_one {x : fin 2} : x = 0 ↔ x ≠ 1 :=
 begin
@@ -341,13 +348,18 @@ lemma indep_on_monochromatic_of (C : top_edge_labelling V (fin 2)) (m : set V) :
   indep_on (C.label_graph 1) m ↔ C.monochromatic_of m 0 :=
 by rw [←clique_on_compl, label_graph_fin_two_compl, clique_on_monochromatic_of]
 
-def number_of_cliques [decidable_eq V] (G : simple_graph V) [decidable_rel G.adj] (k : ℕ) : ℕ :=
+/-- the number of cliques of size k in the graph G -/
+def number_of_cliques [fintype V] [decidable_eq V] (G : simple_graph V) [decidable_rel G.adj]
+  (k : ℕ) : ℕ :=
 ((univ.powerset_len k).filter (λ (s : finset V), G.clique_on s)).card
 
-def number_of_indeps [decidable_eq V] (G : simple_graph V) [decidable_rel G.adj] (l : ℕ) : ℕ :=
+/-- the number of independent sets of size l in the graph G -/
+def number_of_indeps [fintype V] [decidable_eq V] (G : simple_graph V) [decidable_rel G.adj]
+  (l : ℕ) : ℕ :=
 ((univ.powerset_len l).filter (λ (s : finset V), G.indep_on s)).card
 
-lemma number_of_cliques_compl [decidable_eq V] [decidable_rel G.adj] [decidable_rel Gᶜ.adj]
+lemma number_of_cliques_compl [fintype V] [decidable_eq V] [decidable_rel G.adj]
+  [decidable_rel Gᶜ.adj]
   {k : ℕ} :
   number_of_cliques Gᶜ k = number_of_indeps G k :=
 begin
@@ -355,13 +367,17 @@ begin
   simp only [clique_on_compl],
 end
 
-def number_of_things [decidable_eq V] (G : simple_graph V) [decidable_rel G.adj] (k l : ℕ) : ℕ :=
+/-- the number of cliques of size k + the number of independent sets of size l -/
+def number_of_things [fintype V] [decidable_eq V] (G : simple_graph V) [decidable_rel G.adj]
+  (k l : ℕ) : ℕ :=
 G.number_of_cliques k + G.number_of_indeps l
 
 section
 
 open_locale classical
 
+variable [fintype V]
+
 lemma weighted_number_cliques [decidable_eq V] {k : ℕ} :
   ∑ G, weighting V p G * G.number_of_cliques k = ((card V).choose k) * p ^ k.choose 2 :=
 begin
@@ -393,7 +409,7 @@ lemma weighted_number_indeps [decidable_eq V] {k : ℕ} :
   ∑ G, weighting V p G * G.number_of_indeps k = ((card V).choose k) * (1 - p) ^ k.choose 2 :=
 begin
   simp only [←number_of_cliques_compl],
-  simp only [←@weighting_compl _ _ _ p],
+  simp only [←weighting_compl p],
   rw ←weighted_number_cliques,
   refine (sum_bij' (λ G _, Gᶜ) (λ _ _, mem_univ _) _ (λ G _, Gᶜ) (λ _ _, mem_univ _) _ _),
   { intros a ha,
@@ -419,7 +435,7 @@ by simp only [number_of_things, nat.cast_add, mul_add, sum_add_distrib, weighted
 
 end
 
-lemma basic_bound {k l : ℕ} {p : ℝ} (hp : 0 < p) (hp' : p < 1)
+lemma basic_bound [fintype V] {k l : ℕ} {p : ℝ} (hp : 0 < p) (hp' : p < 1)
   (hV : ((card V).choose k : ℝ) * p ^ k.choose 2 + (card V).choose l * (1 - p) ^ l.choose 2 < 1) :
   ∃ (G : simple_graph V),
     (∀ X : finset V, X.card = k → ¬ G.clique_on X) ∧
@@ -428,7 +444,7 @@ begin
   letI := classical.dec_eq V,
   by_contra',
   refine hV.not_le _,
-  rw [←weighted_number_things, ←@sum_weighting V _ p],
+  rw [←weighted_number_things, ←@sum_weighting V p _],
   refine sum_le_sum _,
   intros i hi,
   refine le_mul_of_one_le_right _ _,
@@ -602,11 +618,62 @@ begin
   norm_num
 end
 
+/-- An Erdos-Szekeres upper bound on Ramsey numbers, with the error term made precise -/
+lemma diagonal_ramsey_upper_bound_refined {k : ℕ} :
+  (diagonal_ramsey k : ℝ) ≤ 4 ^ (k - 1) / sqrt (real.pi * (k - 3 / 4)) :=
+begin
+  rcases k.eq_zero_or_pos with rfl | hk,
+  { rw [diagonal_ramsey_zero, nat.cast_zero, nat.zero_sub, pow_zero, one_div, inv_nonneg],
+    exact sqrt_nonneg _ },
+  refine (nat.cast_le.2 (diagonal_ramsey_le_central_binom k)).trans _,
+  refine (central_binomial_upper_bound (k - 1)).trans _,
+  have : (1 : ℝ) ≤ k,
+  { rwa [nat.one_le_cast, nat.succ_le_iff] },
+  refine div_le_div_of_le_left (by positivity) (sqrt_pos_of_pos (mul_pos pi_pos _)) _,
+  { linarith only [this] },
+  refine sqrt_le_sqrt (mul_le_mul_of_nonneg_left _ pi_pos.le),
+  rw [nat.cast_sub, nat.cast_one],
+  { linarith only },
+  rwa nat.one_le_cast at this
+end
+
+lemma diagonal_ramsey_upper_bound_simpler {k : ℕ} : (diagonal_ramsey k : ℝ) ≤ 4 ^ k / sqrt k :=
+begin
+  rcases k.eq_zero_or_pos with rfl | hk,
+  { rw [diagonal_ramsey_zero, nat.cast_zero, pow_zero, sqrt_zero, div_zero] },
+  refine diagonal_ramsey_upper_bound_refined.trans _,
+  rw [pow_sub₀ _ _ hk, ←div_eq_mul_inv, div_div],
+  swap, { positivity },
+  refine div_le_div_of_le_left (by positivity) (by positivity) _,
+  have : (4 : ℝ) ^ 1 = sqrt 16,
+  { have : (16 : ℝ) = 4 ^ 2 := by norm_num,
+    rw [pow_one, this, sqrt_sq],
+    norm_num },
+  rw [this, ←sqrt_mul],
+  swap, { norm_num1 },
+  refine sqrt_le_sqrt _,
+  suffices : (12 * real.pi) ≤ k * (16 * real.pi - 1),
+  { linarith },
+  have : 49 ≤ 16 * real.pi - 1,
+  { linarith only [pi_gt_3141592] },
+  refine (mul_le_mul_of_nonneg_left this (nat.cast_nonneg _)).trans' _,
+  have : 12 * real.pi ≤ 38 := by linarith only [pi_lt_315],
+  have : (1 : ℝ) ≤ k := nat.one_le_cast.2 hk,
+  linarith
+end
+
 section
 
 open filter
 
-lemma little_o_ramsey_bound :
+/--
+A lower bound on diagonal Ramsey numbers, as given on wikipedia. This is within a factor 2 of the
+best known lower bound.
+It says R(k, k) ≥ (1 + o(1)) * k / (e √2) * 2 ^ (k / 2)
+`diagonal_ramsey_bound_refined_again` makes the o(1) term more precise, and
+`diagonal_ramsey_lower_bound_simpler` simplifies the lower order terms for convenience.
+-/
+lemma little_o_lower_ramsey_bound :
   ∃ f : ℕ → ℝ, f =o[at_top] (λ _, 1 : _ → ℝ) ∧
     ∀ k, (1 + f k) * k / (sqrt 2 * exp 1) * (sqrt 2) ^ k ≤ diagonal_ramsey k :=
 begin
@@ -620,13 +687,6 @@ begin
     ←mul_assoc],
 end
 
--- lemma slightly_off_diagonal_lower_ramsey :
---   ∃ c : ℝ, 0 < c ∧ ∀ᶠ l : ℕ in at_top, ∀ k, l ≤ k →
---     real.exp (c * l ^ (3 / 4 : ℝ) * log k) ≤ ramsey_number ![k, ⌊(l : ℝ) ^ (3 / 4 : ℝ)⌋₊] :=
--- begin
-
--- end
-
 end
 
 end simple_graph
diff --git a/src/combinatorics/simple_graph/ramsey_small.lean b/src/combinatorics/simple_graph/ramsey_small.lean
index 8bedc0c072b36..dababef3ff318 100644
--- a/src/combinatorics/simple_graph/ramsey_small.lean
+++ b/src/combinatorics/simple_graph/ramsey_small.lean
@@ -321,6 +321,12 @@ end
 
 section
 
+/--
+A triple of vectors in F₂ ^ 4, which encodes the data of the clebsch colouring in a convenient and
+compact way.
+For our purposes, it is enough to show that the colouring this induces, `clebsch_colouring`, does
+not contain a monochromatic triangle
+-/
 def parts : fin 3 → finset (fin 4 → zmod 2) :=
 ![{(![1, 1, 0, 0]), (![0, 0, 1, 1]), (![1, 0, 0, 1]), (![1, 1, 1, 0]), (![1, 0, 0, 0])},
   {(![1, 0, 1, 0]), (![0, 1, 0, 1]), (![0, 1, 1, 0]), (![1, 1, 0, 1]), (![0, 1, 0, 0])},
@@ -344,6 +350,7 @@ lemma parts_pair_get_aux : ∀ i j : fin 4 → zmod 2, i ≠ j →
   ∃! k, k ∈ (univ : finset (fin 3)) ∧ i - j ∈ parts k :=
 λ i j hij, parts_get_aux _ (sub_ne_zero_of_ne hij)
 
+/-- given two distinct vertices in F₂ ^ 4, get the label it should have in the clebsch colouring. -/
 def parts_pair_get (i j : fin 4 → zmod 2) (hij : i ≠ j) : fin 3 :=
 finset.choose _ _ (parts_pair_get_aux i j hij)
 
@@ -367,6 +374,10 @@ end
 
 open top_edge_labelling
 
+/--
+an explicit definition of the clebsch colouring
+TODO: find the source i used for this
+-/
 def clebsch_colouring : top_edge_labelling (fin 4 → zmod 2) (fin 3) :=
 top_edge_labelling.mk parts_pair_get parts_pair_get_symm