diff --git a/src/analysis/calculus/iterated_deriv_mathlib.lean b/src/analysis/calculus/iterated_deriv_mathlib.lean
new file mode 100644
index 0000000000000..4e615e0c94869
--- /dev/null
+++ b/src/analysis/calculus/iterated_deriv_mathlib.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+import analysis.calculus.iterated_deriv
+
+/-!
+# One-dimensional iterated derivatives
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
+We define the `n`-th derivative of a function `f : 𝕜 → F` as a function
+`iterated_deriv n f : 𝕜 → F`, as well as a version on domains `iterated_deriv_within n f s : 𝕜 → F`,
+and prove their basic properties.
+
+## Main definitions and results
+
+Let `𝕜` be a nontrivially normed field, and `F` a normed vector space over `𝕜`. Let `f : 𝕜 → F`.
+
+* `iterated_deriv n f` is the `n`-th derivative of `f`, seen as a function from `𝕜` to `F`.
+  It is defined as the `n`-th Fréchet derivative (which is a multilinear map) applied to the
+  vector `(1, ..., 1)`, to take advantage of all the existing framework, but we show that it
+  coincides with the naive iterative definition.
+* `iterated_deriv_eq_iterate` states that the `n`-th derivative of `f` is obtained by starting
+  from `f` and differentiating it `n` times.
+* `iterated_deriv_within n f s` is the `n`-th derivative of `f` within the domain `s`. It only
+  behaves well when `s` has the unique derivative property.
+* `iterated_deriv_within_eq_iterate` states that the `n`-th derivative of `f` in the domain `s` is
+  obtained by starting from `f` and differentiating it `n` times within `s`. This only holds when
+  `s` has the unique derivative property.
+
+## Implementation details
+
+The results are deduced from the corresponding results for the more general (multilinear) iterated
+Fréchet derivative. For this, we write `iterated_deriv n f` as the composition of
+`iterated_fderiv 𝕜 n f` and a continuous linear equiv. As continuous linear equivs respect
+differentiability and commute with differentiation, this makes it possible to prove readily that
+the derivative of the `n`-th derivative is the `n+1`-th derivative in `iterated_deriv_within_succ`,
+by translating the corresponding result `iterated_fderiv_within_succ_apply_left` for the
+iterated Fréchet derivative.
+-/
+
+noncomputable theory
+open_locale classical topology big_operators
+open filter asymptotics set
+
+
+variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
+variables {F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
+variables {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
+
+-- lemma iterated_deriv_within_univ {n : ℕ} {f : 𝕜 → F} {n : ℕ} :
+--   iterated_deriv_within n f univ = iterated_deriv n f :=
+
+lemma iterated_fderiv_within_nhds {u : set E} {x : E} {f : E → F} {n : ℕ} (hu : u ∈ 𝓝 x) :
+  iterated_fderiv_within 𝕜 n f u x = iterated_fderiv 𝕜 n f x :=
+by rw [←iterated_fderiv_within_univ, ←univ_inter u, iterated_fderiv_within_inter hu]
+
+lemma iterated_deriv_within_of_is_open {s : set 𝕜} {f : 𝕜 → F} (n : ℕ) (hs : is_open s) :
+  eq_on (iterated_deriv_within n f s) (iterated_deriv n f) s :=
+λ x hx, by rw [iterated_deriv_within, iterated_deriv, iterated_fderiv_within_of_is_open _ hs hx]
+
+lemma iterated_deriv_within_nhds {u : set 𝕜} {x : 𝕜} {f : 𝕜 → F} {n : ℕ} (hu : u ∈ 𝓝 x) :
+  iterated_deriv_within n f u x = iterated_deriv n f x :=
+by rw [iterated_deriv_within, iterated_deriv, iterated_fderiv_within_nhds hu]
diff --git a/src/analysis/calculus/taylor_mathlib.lean b/src/analysis/calculus/taylor_mathlib.lean
new file mode 100644
index 0000000000000..4b12c86dabc34
--- /dev/null
+++ b/src/analysis/calculus/taylor_mathlib.lean
@@ -0,0 +1,229 @@
+import analysis.calculus.taylor
+import analysis.calculus.cont_diff
+import data.set.intervals.unordered_interval
+
+open set
+
+open_locale nat
+
+section
+
+variables {α : Type*} [lattice α]
+
+def uIoo (x y : α) : set α := Ioo (x ⊓ y) (x ⊔ y)
+
+lemma uIoo_of_le {x y : α} (h : x ≤ y) : uIoo x y = Ioo x y :=
+by rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
+
+lemma uIoo_of_ge {x y : α} (h : y ≤ x) : uIoo x y = Ioo y x :=
+by rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]
+
+lemma uIoo_comm (x y : α) : uIoo x y = uIoo y x := by rw [uIoo, uIoo, inf_comm, sup_comm]
+
+lemma uIoo_subset_Ioo {a₁ a₂ b₁ b₂ : α} (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) :
+  uIoo a₁ b₁ ⊆ Ioo a₂ b₂ :=
+Ioo_subset_Ioo (le_inf ha.1 hb.1) (sup_le ha.2 hb.2)
+
+end
+
+lemma taylor_mean_remainder_unordered {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ ≠ x)
+  (hf : cont_diff_on ℝ n f (uIcc x₀ x))
+  (hf' : differentiable_on ℝ (iterated_deriv_within n f (uIcc x₀ x)) (uIoo x₀ x))
+  (gcont : continuous_on g (uIcc x₀ x))
+  (gdiff : ∀ (x_1 : ℝ), x_1 ∈ uIoo x₀ x → has_deriv_at g (g' x_1) x_1)
+  (g'_ne : ∀ (x_1 : ℝ), x_1 ∈ uIoo x₀ x → g' x_1 ≠ 0) :
+  ∃ (x' : ℝ) (hx' : x' ∈ uIoo x₀ x), f x - taylor_within_eval f n (uIcc x₀ x) x₀ x =
+  ((x - x')^n /n! * (g x - g x₀) / g' x') •
+    (iterated_deriv_within (n+1) f (uIcc x₀ x) x') :=
+begin
+  rcases ne.lt_or_lt hx with hx₀ | hx₀,
+  { rw [uIcc_of_le hx₀.le] at hf hf' gcont ⊢,
+    rw [uIoo_of_le hx₀.le] at g'_ne gdiff hf' ⊢,
+    exact taylor_mean_remainder hx₀ hf hf' gcont gdiff g'_ne },
+  rw [uIcc_of_ge hx₀.le] at hf hf' gcont ⊢,
+  rw [uIoo_of_ge hx₀.le] at g'_ne gdiff hf' ⊢,
+  rcases exists_ratio_has_deriv_at_eq_ratio_slope (λ t, taylor_within_eval f n (Icc x x₀) t x)
+    (λ t, ((n! : ℝ)⁻¹ * (x - t)^n) • (iterated_deriv_within (n+1) f (Icc x x₀) t)) hx₀
+    (continuous_on_taylor_within_eval (unique_diff_on_Icc hx₀) hf)
+    (λ _ hy, taylor_within_eval_has_deriv_at_Ioo x hx₀ hy hf hf')
+    g g' gcont gdiff with ⟨y, hy, h⟩,
+  use [y, hy],
+  -- The rest is simplifications and trivial calculations
+  simp only [taylor_within_eval_self] at h,
+  rw [mul_comm, ←div_left_inj' (g'_ne y hy), mul_div_cancel _ (g'_ne y hy)] at h,
+  rw [←neg_sub, ←h],
+  field_simp [g'_ne y hy, n.factorial_ne_zero],
+  ring,
+end
+
+lemma taylor_mean_remainder_lagrange_unordered {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ ≠ x)
+  (hf : cont_diff_on ℝ n f (uIcc x₀ x))
+  (hf' : differentiable_on ℝ (iterated_deriv_within n f (uIcc x₀ x)) (uIoo x₀ x)) :
+  ∃ (x' : ℝ) (hx' : x' ∈ uIoo x₀ x), f x - taylor_within_eval f n (uIcc x₀ x) x₀ x =
+  (iterated_deriv_within (n+1) f (uIcc x₀ x) x') * (x - x₀)^(n+1) /(n+1)! :=
+begin
+  have gcont : continuous_on (λ (t : ℝ), (x - t) ^ (n + 1)) (uIcc x₀ x) :=
+  by { refine continuous.continuous_on _, continuity },
+  have xy_ne : ∀ (y : ℝ), y ∈ uIoo x₀ x → (x - y)^n ≠ 0 :=
+  begin
+    intros y hy,
+    refine pow_ne_zero _ _,
+    rw [sub_ne_zero],
+    cases le_total x₀ x,
+    { rw [uIoo_of_le h] at hy,
+      exact hy.2.ne' },
+    { rw [uIoo_of_ge h] at hy,
+      exact hy.1.ne }
+  end,
+  have hg' : ∀ (y : ℝ), y ∈ uIoo x₀ x → -(↑n + 1) * (x - y) ^ n ≠ 0 :=
+  λ y hy, mul_ne_zero (neg_ne_zero.mpr (nat.cast_add_one_ne_zero n)) (xy_ne y hy),
+  -- We apply the general theorem with g(t) = (x - t)^(n+1)
+  rcases taylor_mean_remainder_unordered hx hf hf' gcont (λ y _, monomial_has_deriv_aux y x _) hg'
+    with ⟨y, hy, h⟩,
+  use [y, hy],
+  simp only [sub_self, zero_pow', ne.def, nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h,
+  rw [h, neg_div, ←div_neg, neg_mul, neg_neg],
+  field_simp [n.cast_add_one_ne_zero, n.factorial_ne_zero, xy_ne y hy],
+  ring,
+end
+
+-- x' should be in uIoo x₀ x
+lemma taylor_mean_remainder_central_aux {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x₀ x a b : ℝ} {n : ℕ}
+  (hab : a < b) (hx : x ∈ Icc a b) (hx₀ : x₀ ∈ Icc a b)
+  (hf : cont_diff_on ℝ n f (Icc a b))
+  (hf' : differentiable_on ℝ (iterated_deriv_within n f (Icc a b)) (Ioo a b))
+  (gcont : continuous_on g (Icc a b))
+  (gdiff : ∀ (y : ℝ), y ∈ Ioo a b → has_deriv_at g (g' y) y) :
+  ∃ (x' : ℝ) (hx' : x' ∈ Ioo a b), x' ≠ x ∧ (f x - taylor_within_eval f n (Icc a b) x₀ x) * g' x' =
+  ((x - x')^n / n! * (g x - g x₀)) • (iterated_deriv_within (n+1) f (Icc a b) x') :=
+begin
+  rcases eq_or_ne x₀ x with rfl | hx',
+  { simp only [sub_self, taylor_within_eval_self, mul_zero, zero_div, zero_smul, eq_self_iff_true,
+      exists_prop, and_true, zero_mul],
+    obtain ⟨x', hx'⟩ := ((Ioo_infinite hab).diff (set.finite_singleton x₀)).nonempty,
+    exact ⟨x', by simpa using hx'⟩ },
+  rcases ne.lt_or_lt hx' with hx' | hx',
+  { have h₁ : Icc x₀ x ⊆ Icc a b := Icc_subset_Icc hx₀.1 hx.2,
+    have h₂ : Ioo x₀ x ⊆ Ioo a b := Ioo_subset_Ioo hx₀.1 hx.2,
+    obtain ⟨y, hy, h⟩ := exists_ratio_has_deriv_at_eq_ratio_slope
+      (λ t, taylor_within_eval f n (Icc a b) t x)
+      (λ t, ((n! : ℝ)⁻¹ * (x - t)^n) • (iterated_deriv_within (n+1) f (Icc a b) t)) hx'
+      ((continuous_on_taylor_within_eval (unique_diff_on_Icc hab) hf).mono h₁)
+      (λ _ hy, taylor_within_eval_has_deriv_at_Ioo _ hab (h₂ hy) hf hf') g g'
+      (gcont.mono h₁) (λ y hy, gdiff y (h₂ hy)),
+    refine ⟨y, h₂ hy, hy.2.ne, _⟩,
+    -- The rest is simplifications and trivial calculations
+    simp only [taylor_within_eval_self] at h,
+    field_simp [←h, n.factorial_ne_zero],
+    ring },
+  { have h₁ : Icc x x₀ ⊆ Icc a b := Icc_subset_Icc hx.1 hx₀.2,
+    have h₂ : Ioo x x₀ ⊆ Ioo a b := Ioo_subset_Ioo hx.1 hx₀.2,
+    obtain ⟨y, hy, h⟩ := exists_ratio_has_deriv_at_eq_ratio_slope
+      (λ t, taylor_within_eval f n (Icc a b) t x)
+      (λ t, ((n! : ℝ)⁻¹ * (x - t)^n) • (iterated_deriv_within (n+1) f (Icc a b) t)) hx'
+      ((continuous_on_taylor_within_eval (unique_diff_on_Icc hab) hf).mono h₁)
+      (λ _ hy, taylor_within_eval_has_deriv_at_Ioo _ hab (h₂ hy) hf hf') g g'
+      (gcont.mono h₁) (λ y hy, gdiff y (h₂ hy)),
+    refine ⟨y, h₂ hy, hy.1.ne', _⟩,
+    -- The rest is simplifications and trivial calculations
+    simp only [taylor_within_eval_self] at h,
+    rw [←neg_sub, neg_mul, ←h],
+    field_simp [n.factorial_ne_zero],
+    ring },
+end
+
+lemma taylor_mean_remainder_central {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x₀ x a b : ℝ} {n : ℕ} (hab : a < b)
+  (hx : x ∈ Icc a b) (hx₀ : x₀ ∈ Icc a b)
+  (hf : cont_diff_on ℝ n f (Icc a b))
+  (hf' : differentiable_on ℝ (iterated_deriv_within n f (Icc a b)) (Ioo a b))
+  (gcont : continuous_on g (Icc a b))
+  (gdiff : ∀ (y : ℝ), y ∈ Ioo a b → has_deriv_at g (g' y) y)
+  (g'_ne : ∀ (y : ℝ), y ∈ Ioo a b → g' y ≠ 0) :
+  ∃ (x' : ℝ) (hx' : x' ∈ Ioo a b), f x - taylor_within_eval f n (Icc a b) x₀ x =
+  ((x - x')^n / n! * (g x - g x₀) / g' x') •
+    (iterated_deriv_within (n+1) f (Icc a b) x') :=
+begin
+  obtain ⟨y, hy, hyx, h⟩ := taylor_mean_remainder_central_aux hab hx hx₀ hf hf' gcont gdiff,
+  refine ⟨y, hy, _⟩,
+  rw [smul_eq_mul] at h,
+  rw [smul_eq_mul, div_mul_eq_mul_div, ←h, mul_div_cancel],
+  exact g'_ne _ hy,
+end
+
+lemma taylor_mean_remainder_lagrange_central {f : ℝ → ℝ} {x x₀ a b : ℝ} {n : ℕ} (hab : a < b)
+  (hx : x ∈ Icc a b) (hx₀ : x₀ ∈ Icc a b)
+  (hf : cont_diff_on ℝ n f (Icc a b))
+  (hf' : differentiable_on ℝ (iterated_deriv_within n f (Icc a b)) (Ioo a b)) :
+  ∃ (x' : ℝ) (hx' : x' ∈ Ioo a b), f x - taylor_within_eval f n (Icc a b) x₀ x =
+  (iterated_deriv_within (n+1) f (Icc a b) x') * (x - x₀)^(n+1) / (n+1)! :=
+begin
+  have gcont : continuous_on (λ (t : ℝ), (x - t) ^ (n + 1)) (Icc a b) :=
+  by { refine continuous.continuous_on _, continuity },
+  rcases taylor_mean_remainder_central_aux hab hx hx₀ hf hf' gcont
+    (λ y _, monomial_has_deriv_aux y x _) with ⟨y, hy, hy', h⟩,
+  have hy_ne : x - y ≠ 0 := sub_ne_zero_of_ne hy'.symm,
+  use [y, hy],
+  dsimp at h,
+  rw [←eq_div_iff] at h,
+  swap,
+  { exact mul_ne_zero (neg_ne_zero.2 (by positivity)) (by positivity) },
+  simp only [h, sub_self, zero_pow' _ (nat.succ_ne_zero n), zero_sub, mul_neg, neg_mul,
+    nat.factorial_succ, nat.cast_add_one, neg_div_neg_eq, nat.cast_mul] with field_simps,
+  rw [mul_left_comm, ←mul_assoc, ←div_div, div_eq_iff (pow_ne_zero _ hy_ne), div_mul_eq_mul_div],
+  congr' 1,
+  ring_nf
+end
+
+lemma taylor_mean_remainder_cauchy_central {f : ℝ → ℝ} {x x₀ a b : ℝ} {n : ℕ} (hab : a < b)
+  (hx : x ∈ Icc a b) (hx₀ : x₀ ∈ Icc a b)
+  (hf : cont_diff_on ℝ n f (Icc a b))
+  (hf' : differentiable_on ℝ (iterated_deriv_within n f (Icc a b)) (Ioo a b)) :
+  ∃ (x' : ℝ) (hx' : x' ∈ Ioo a b), f x - taylor_within_eval f n (Icc a b) x₀ x =
+  (iterated_deriv_within (n+1) f (Icc a b) x') * (x - x')^n /n! * (x - x₀) :=
+begin
+  -- We apply the general theorem with g = id
+  rcases taylor_mean_remainder_central hab hx hx₀ hf hf' continuous_on_id
+    (λ _ _, has_deriv_at_id _) (λ _ _, by simp) with ⟨y, hy, h⟩,
+  refine ⟨y, hy, _⟩,
+  rw h,
+  field_simp [n.factorial_ne_zero],
+  ring,
+end
+
+lemma taylor_mean_remainder_bound_central {f : ℝ → ℝ} {a b C x x₀ : ℝ} {n : ℕ}
+  (hab : a ≤ b) (hf : cont_diff_on ℝ (n+1) f (Icc a b)) (hx : x ∈ Icc a b) (hx₀ : x₀ ∈ Icc a b)
+  (hC : ∀ y ∈ Ioo a b, ‖iterated_deriv_within (n + 1) f (Icc a b) y‖ ≤ C) :
+  ‖f x - taylor_within_eval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / (n + 1)! :=
+begin
+  rcases eq_or_lt_of_le hab with rfl | hab,
+  { simp only [Icc_self, mem_singleton_iff] at hx hx₀,
+    substs hx₀ hx,
+    rw [taylor_within_eval_self, sub_self, sub_self, abs_zero, zero_pow nat.succ_pos', mul_zero,
+      zero_div, norm_zero] },
+  have : differentiable_on ℝ (iterated_deriv_within n f (Icc a b)) (Ioo a b),
+  { refine (hf.differentiable_on_iterated_deriv_within _ (unique_diff_on_Icc hab)).mono
+      Ioo_subset_Icc_self,
+    rw [←nat.cast_add_one, nat.cast_lt],
+    exact nat.lt_succ_self _ },
+  obtain ⟨x', hx', h⟩ := taylor_mean_remainder_lagrange_central hab hx hx₀ hf.of_succ this,
+  rw [h, norm_div, norm_mul, real.norm_coe_nat, real.norm_eq_abs ((x - x₀) ^ _), ←abs_pow],
+  refine div_le_div_of_le (nat.cast_nonneg _) _,
+  exact mul_le_mul_of_nonneg_right (hC _ hx') (abs_nonneg _),
+end
+
+lemma exists_taylor_mean_remainder_bound_central {f : ℝ → ℝ} {a b x₀ : ℝ} {n : ℕ}
+  (hab : a ≤ b) (hf : cont_diff_on ℝ (n+1) f (Icc a b)) (hx₀ : x₀ ∈ Icc a b) :
+  ∃ C, ∀ x ∈ Icc a b, ‖f x - taylor_within_eval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) :=
+begin
+  rcases eq_or_lt_of_le hab with rfl | h,
+  { refine ⟨0, λ x hx, _⟩,
+    rw [Icc_self, mem_singleton_iff] at hx hx₀,
+    rw [hx₀, hx, taylor_within_eval_self, sub_self, zero_mul, norm_zero] },
+  let C := Sup ((λ y, ‖iterated_deriv_within (n + 1) f (Icc a b) y‖) '' Icc a b),
+  refine ⟨C / (n + 1)!, λ x hx, _⟩,
+  rw [div_mul_eq_mul_div],
+  refine taylor_mean_remainder_bound_central hab hf hx hx₀ _,
+  intros y hy,
+  refine continuous_on.le_Sup_image_Icc _ (Ioo_subset_Icc_self hy),
+  exact (hf.continuous_on_iterated_deriv_within le_rfl (unique_diff_on_Icc h)).norm,
+end
diff --git a/src/combinatorics/simple_graph/basic_mathlib.lean b/src/combinatorics/simple_graph/basic_mathlib.lean
index 0315d5b756b58..d50d2099f094f 100644
--- a/src/combinatorics/simple_graph/basic_mathlib.lean
+++ b/src/combinatorics/simple_graph/basic_mathlib.lean
@@ -143,4 +143,10 @@ by { rw [←disjoint_coe, coe_neighbor_finset, coe_neighbor_finset], exact neigh
 
 end
 
+lemma degree_eq_zero_iff {v : V} [fintype (G.neighbor_set v)] : G.degree v = 0 ↔ ∀ w, ¬ G.adj v w :=
+by rw [←not_exists, ←degree_pos_iff_exists_adj, not_lt, le_zero_iff]
+
+lemma comap_comap {V W X : Type*} {G : simple_graph V} {f : W → V} {g : X → W} :
+  (G.comap f).comap g = G.comap (f ∘ g) := rfl
+
 end simple_graph
diff --git a/src/combinatorics/simple_graph/clique_mathlib.lean b/src/combinatorics/simple_graph/clique_mathlib.lean
new file mode 100644
index 0000000000000..8ea785769f00f
--- /dev/null
+++ b/src/combinatorics/simple_graph/clique_mathlib.lean
@@ -0,0 +1,19 @@
+import combinatorics.simple_graph.basic_mathlib
+import combinatorics.simple_graph.clique
+
+namespace simple_graph
+
+variables {V W : Type*} {G : simple_graph V} {H : simple_graph W} {n : ℕ}
+
+lemma not_clique_free_iff' (n : ℕ) :
+  ¬ G.clique_free n ↔ nonempty ((⊤ : simple_graph (fin n)) →g G) :=
+by rw [not_clique_free_iff, (simple_graph.top_hom_graph_equiv).nonempty_congr]
+
+lemma clique_free_iff' {n : ℕ} :
+  G.clique_free n ↔ is_empty ((⊤ : simple_graph (fin n)) →g G) :=
+by rw [← not_iff_not, not_clique_free_iff', not_is_empty_iff]
+
+lemma clique_free.hom (f : G →g H) : H.clique_free n → G.clique_free n :=
+λ h, clique_free_iff'.2 ⟨λ x, (clique_free_iff'.1 h).elim' (f.comp x)⟩
+
+end simple_graph
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/basic.lean b/src/combinatorics/simple_graph/exponential_ramsey/basic.lean
index 2a21ce47f897a..05e32575eaae7 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/basic.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/basic.lean
@@ -63,96 +63,6 @@ def col_neighbors [fintype V] [decidable_eq V] [decidable_eq K] (χ : top_edge_l
   (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
 
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/main_results.lean b/src/combinatorics/simple_graph/exponential_ramsey/main_results.lean
new file mode 100644
index 0000000000000..36bf2c4c3bd72
--- /dev/null
+++ b/src/combinatorics/simple_graph/exponential_ramsey/main_results.lean
@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2023 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
+import combinatorics.simple_graph.exponential_ramsey.section12
+
+/-!
+# Summary of main results
+
+In this file we demonstrate the main result of this formalisation, using the proofs which are
+given fully in other files. The purpose of this file is to show the form in which the definitions
+and theorem look.
+-/
+
+namespace main_results
+
+open simple_graph
+open simple_graph.top_edge_labelling
+
+-- This lemma characterises our definition of Ramsey numbers.
+-- Since `fin k` denotes the numbers `{0, ..., k - 1}`, we can think of a function `fin k → ℕ`
+-- as being a vector in `ℕ^k`, ie `n = (n₀, n₁, ..., nₖ₋₁)`. Then our definition of `R(n)` satisfies
+-- `R(n) ≤ N` if and only if, for any labelling `C` of the edges of the complete graph on
+-- `{0, ..., N - 1}`, there is a finite subset `m` of this graph's vertices, and a label `i` such
+-- that `|m| ≥ nᵢ`, and all edges of `m` are labelled `i`.
+lemma ramsey_number_le_iff {k N : ℕ} (n : fin k → ℕ) :
+  ramsey_number n ≤ N ↔
+    ∀ (C : (complete_graph (fin N)).edge_set → fin k),
+      ∃ m : finset (fin N), ∃ i : fin k, monochromatic_of C m i ∧ n i ≤ m.card :=
+ramsey_number_le_iff_fin
+
+-- We've got a definition of Ramsey numbers, let's first make sure it satisfies some of
+-- the obvious properties.
+example : ∀ k, ramsey_number ![2, k] = k := by simp
+example : ∀ k l, ramsey_number ![k, l] = ramsey_number ![l, k] := ramsey_number_pair_swap
+
+-- It also satisfies the inductive bound by Erdős-Szekeres
+lemma ramsey_number_inductive_bound : ∀ k l, k ≥ 2 → l ≥ 2 →
+    ramsey_number ![k, l] ≤ ramsey_number ![k - 1, l] + ramsey_number ![k, l - 1] :=
+λ _ _, ramsey_number_two_colour_bound_aux
+
+-- And we can use this bound to get the standard upper bound in terms of the binomial coefficient,
+-- which is written `n.choose k` in Lean.
+lemma ramsey_number_binomial_bound :
+  ∀ k l, ramsey_number ![k, l] ≤ (k + l - 2).choose (k - 1) :=
+ramsey_number_le_choose
+
+lemma ramsey_number_power_bound : ∀ k, ramsey_number ![k, k] ≤ 4 ^ k :=
+λ _, diagonal_ramsey_le_four_pow
+
+-- We can also verify some small values:
+example : ramsey_number ![3, 3] = 6 := ramsey_number_three_three
+example : ramsey_number ![3, 4] = 9 := ramsey_number_three_four
+example : ramsey_number ![4, 4] = 18 := ramsey_number_four_four
+-- The `![]` notation means the input to the `ramsey_number` function is a vector, and indeed gives
+-- values for more than two colours too
+example : ramsey_number ![3, 3, 3] = 17 := ramsey_number_three_three_three
+
+-- We also have Erdős' lower bound on Ramsey numbers
+lemma ramsey_number_lower_bound : ∀ k, 2 ≤ k → real.sqrt 2 ^ k ≤ ramsey_number ![k, k] :=
+  λ _, diagonal_ramsey_lower_bound_simpler
+
+-- Everything up to this point has been known results, which were needed for the formalisation,
+-- served as a useful warm up to the main result, and hopefully demonstrate the correctness
+-- of the definition of Ramsey numbers.
+
+-- Finally, the titutar statement, giving an exponential improvement to the upper bound on Ramsey
+-- numbers.
+theorem exponential_ramsey_improvement : ∃ ε > 0, ∀ k, (ramsey_number ![k, k] : ℝ) ≤ (4 - ε) ^ k :=
+global_bound
+
+end main_results
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section11.lean b/src/combinatorics/simple_graph/exponential_ramsey/section11.lean
index e5e1c98ad9fdf..1fda25fe5465f 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section11.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section11.lean
@@ -509,9 +509,8 @@ lemma comp_right_density_apply {V K K' : Type*} [fintype V] [decidable_eq V] [de
   [decidable_eq K'] (k : K) {χ : top_edge_labelling V K} (f : K → K') (hf : function.injective f) :
   (χ.comp_right f).density (f k) = χ.density k :=
 begin
-  rw [top_edge_labelling.density],
-  simp only [comp_right_label_graph_apply _ hf],
-  refl
+  rw [top_edge_labelling.density, top_edge_labelling.density, rat.cast_inj],
+  exact density_congr _ _ (comp_right_label_graph_apply _ hf),
 end
 
 lemma density_sum {V : Type*} [fintype V] [decidable_eq V] (hV : 2 ≤ fintype.card V)
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section9.lean b/src/combinatorics/simple_graph/exponential_ramsey/section9.lean
index 479aab21e202d..1c2d34b48d6d8 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section9.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section9.lean
@@ -1019,16 +1019,26 @@ end
 
 section
 
-variables {V : Type*} [fintype V] [decidable_eq V]
+variables {V : Type*}
 open fintype
 
 section
 
 /-- The density of a simple graph. -/
-def density (G : simple_graph V) [decidable_rel G.adj] : ℚ :=
+def density [fintype V] (G : simple_graph V) [fintype G.edge_set] : ℚ :=
 G.edge_finset.card / (card V).choose 2
 
-lemma edge_finset_eq_filter (G : simple_graph V) [decidable_rel G.adj] :
+lemma density_congr [fintype V] (G₁ G₂ : simple_graph V) [fintype G₁.edge_set] [fintype G₂.edge_set]
+  (h : G₁ = G₂) : G₁.density = G₂.density :=
+begin
+  rw [density, density, edge_finset_card, edge_finset_card],
+  congr' 2,
+  refine card_congr' _,
+  rw h
+end
+
+lemma edge_finset_eq_filter
+  [fintype (sym2 V)] (G : simple_graph V) [fintype G.edge_set] [decidable_rel G.adj] :
   G.edge_finset = univ.filter (∈ sym2.from_rel G.symm) :=
 begin
   rw [←finset.coe_inj, coe_edge_finset, coe_filter, coe_univ, set.sep_univ],
@@ -1039,7 +1049,8 @@ lemma univ_image_quotient_mk {α : Type*} (s : finset α) [decidable_eq α] :
   s.off_diag.image quotient.mk = s.sym2.filter (λ a, ¬ a.is_diag) :=
 (sym2.filter_image_quotient_mk_not_is_diag _).symm
 
-lemma edge_finset_eq_filter_filter (G : simple_graph V) [decidable_rel G.adj] :
+lemma edge_finset_eq_filter_filter [decidable_eq V] [fintype (sym2 V)] (G : simple_graph V)
+  [fintype G.edge_set] [decidable_rel G.adj] :
   G.edge_finset = (univ.filter (λ a : sym2 V, ¬ a.is_diag)).filter (∈ sym2.from_rel G.symm) :=
 begin
   rw [edge_finset_eq_filter, filter_filter],
@@ -1051,7 +1062,8 @@ begin
   exact h.ne,
 end
 
-lemma edge_finset_eq_filter' (G : simple_graph V) [decidable_rel G.adj] :
+lemma edge_finset_eq_filter' [fintype V] [decidable_eq V] (G : simple_graph V) [fintype G.edge_set]
+  [decidable_rel G.adj] :
   G.edge_finset = (univ.off_diag.image quotient.mk).filter (∈ sym2.from_rel G.symm) :=
 by rw [edge_finset_eq_filter_filter, ←sym2_univ, ←univ_image_quotient_mk]
 
@@ -1092,7 +1104,8 @@ begin
   simp [h.1, h.2.2, ne.symm h.2.1],
 end
 
-lemma density_eq_average (G : simple_graph V) [decidable_rel G.adj] :
+lemma density_eq_average [fintype V] [decidable_eq V] (G : simple_graph V) [fintype G.edge_set]
+  [decidable_rel G.adj] :
   G.density =
     (card V * (card V - 1))⁻¹ * ∑ x : V, ∑ y in univ.erase x, if G.adj x y then 1 else 0 :=
 begin
@@ -1102,16 +1115,18 @@ begin
   refl
 end
 
-lemma density_eq_average' (G : simple_graph V) [decidable_rel G.adj] :
-  G.density =
-    (card V * (card V - 1))⁻¹ * ∑ x y : V, if G.adj x y then 1 else 0 :=
+lemma density_eq_average' [fintype V] (G : simple_graph V) [fintype G.edge_set]
+  [decidable_rel G.adj] :
+  G.density = (card V * (card V - 1))⁻¹ * ∑ x y : V, if G.adj x y then 1 else 0 :=
 begin
+  classical,
   rw [density_eq_average],
   congr' 2 with x : 1,
   simp
 end
 
-lemma density_eq_average_neighbors (G : simple_graph V) [decidable_rel G.adj] :
+lemma density_eq_average_neighbors [fintype V] (G : simple_graph V) [fintype G.edge_set]
+  [decidable_rel G.adj] :
   G.density = (card V * (card V - 1))⁻¹ * ∑ x : V, (G.neighbor_finset x).card :=
 begin
   rw [density_eq_average'],
@@ -1119,7 +1134,8 @@ begin
   simp [neighbor_finset_eq_filter],
 end
 
-lemma density_compl (G : simple_graph V) [decidable_rel G.adj] (h : 2 ≤ card V) :
+lemma density_compl [fintype V] (G : simple_graph V) [fintype G.edge_set] [fintype Gᶜ.edge_set]
+  (h : 2 ≤ card V) :
   Gᶜ.density = 1 - G.density :=
 begin
   rw [simple_graph.density, card_compl_edge_finset_eq, nat.cast_sub edge_finset_card_le,
@@ -1230,7 +1246,10 @@ begin
   { linarith }
 end
 
-lemma density_eq_average_partition (G : simple_graph V) [decidable_rel G.adj] (n : ℕ)
+variables [fintype V]
+
+lemma density_eq_average_partition [decidable_eq V]
+  (G : simple_graph V) [decidable_rel G.adj] [fintype G.edge_set] (n : ℕ)
   (hn₀ : 0 < n) (hn : n < card V) :
   G.density = ((card V).choose n)⁻¹ * ∑ U in powerset_len n univ, G.edge_density U Uᶜ :=
 begin
@@ -1259,8 +1278,9 @@ begin
   rw [choose_helper hn],
 end
 
-lemma exists_density_edge_density (G : simple_graph V) [decidable_rel G.adj] (n : ℕ)
-  (hn₀ : 0 < n) (hn : n < card V) :
+lemma exists_density_edge_density [decidable_eq V] (G : simple_graph V) [decidable_rel G.adj]
+  [fintype G.edge_set]
+  (n : ℕ) (hn₀ : 0 < n) (hn : n < card V) :
   ∃ U : finset V, U.card = n ∧ G.density ≤ G.edge_density U Uᶜ :=
 begin
   suffices : ∃ U ∈ powerset_len n (univ : finset V), G.density ≤ G.edge_density U Uᶜ,
@@ -1275,10 +1295,12 @@ begin
 end
 
 lemma exists_equibipartition_edge_density (G : simple_graph V) [decidable_rel G.adj]
+  [fintype G.edge_set]
   (hn : 2 ≤ card V) :
   ∃ X Y : finset V, disjoint X Y ∧ ⌊(card V / 2 : ℝ)⌋₊ ≤ X.card ∧ ⌊(card V / 2 : ℝ)⌋₊ ≤ Y.card
     ∧ G.density ≤ G.edge_density X Y :=
 begin
+  classical,
   rw [←nat.cast_two, nat.floor_div_eq_div],
   have h₁ : 0 < card V / 2 := nat.div_pos hn two_pos,
   have h₂ : card V / 2 < card V := nat.div_lt_self (pos_of_gt hn) one_lt_two,
@@ -1291,7 +1313,8 @@ end
 end
 
 /--  The density of a label in the edge labelling. -/
-def top_edge_labelling.density {K : Type*} [decidable_eq K] (χ : top_edge_labelling V K) (k : K) :
+def top_edge_labelling.density [fintype V] {K : Type*} [decidable_eq K] (χ : top_edge_labelling V K)
+  (k : K) [fintype (χ.label_graph k).edge_set] :
   ℝ := density (χ.label_graph k)
 
 lemma exists_equibipartition_col_density {n : ℕ}
@@ -1306,12 +1329,16 @@ begin
   all_goals { simp }
 end
 
-lemma density_zero_one (χ : top_edge_labelling V (fin 2)) (h : 2 ≤ card V) :
+lemma density_zero_one [fintype V] (χ : top_edge_labelling V (fin 2))
+  [fintype (χ.label_graph 0).edge_set] [fintype (χ.label_graph 1).edge_set]
+  (h : 2 ≤ card V) :
   χ.density 0 = 1 - χ.density 1 :=
 begin
+  classical,
   rw [top_edge_labelling.density, top_edge_labelling.density, ←rat.cast_one, ←rat.cast_sub,
-    rat.cast_inj, ←density_compl _ h],
-  simp only [←to_edge_labelling_label_graph_compl, label_graph_to_edge_labelling χ],
+    rat.cast_inj, ←density_compl (χ.label_graph 1) h],
+  refine density_congr _ _ _,
+  rw [←to_edge_labelling_label_graph_compl, label_graph_to_edge_labelling],
 end
 
 end
diff --git a/src/combinatorics/simple_graph/ramsey.lean b/src/combinatorics/simple_graph/ramsey.lean
index 970c689397a39..07fc2f7c039ba 100644
--- a/src/combinatorics/simple_graph/ramsey.lean
+++ b/src/combinatorics/simple_graph/ramsey.lean
@@ -13,8 +13,6 @@ import data.fin.vec_notation
 import data.finite.card
 import data.finset.pairwise
 import data.sym.card
-import field_theory.finite.basic
-import number_theory.legendre_symbol.quadratic_char.gauss_sum
 import tactic.fin_cases
 
 import combinatorics.simple_graph.ramsey_prereq
@@ -238,46 +236,48 @@ instance [decidable_eq K] [decidable_eq V] (C : top_edge_labelling V K)
   (m : finset V) (c : K) : decidable (C.monochromatic_of m c) :=
 decidable_of_iff' _ C.monochromatic_of_iff_pairwise
 
+namespace top_edge_labelling
+
 variables {m : set V} {c : K}
 
-@[simp] lemma top_edge_labelling.monochromatic_of_empty : C.monochromatic_of ∅ c.
+@[simp] lemma monochromatic_of_empty : C.monochromatic_of ∅ c.
 
-@[simp] lemma top_edge_labelling.monochromatic_of_singleton {x : V} : C.monochromatic_of {x} c :=
+@[simp] lemma monochromatic_of_singleton {x : V} : C.monochromatic_of {x} c :=
 by simp [top_edge_labelling.monochromatic_of]
 
-lemma top_edge_labelling.monochromatic_finset_singleton {x : V} :
+lemma monochromatic_finset_singleton {x : V} :
   C.monochromatic_of ({x} : finset V) c :=
 by simp [top_edge_labelling.monochromatic_of]
 
-lemma top_edge_labelling.monochromatic_subsingleton (hm : set.subsingleton m) :
+lemma monochromatic_subsingleton (hm : m.subsingleton) :
   C.monochromatic_of m c :=
 λ x hx y hy h, by cases h (hm hx hy)
 
-lemma top_edge_labelling.monochromatic_subsingleton_colours [subsingleton K] :
+lemma monochromatic_subsingleton_colours [subsingleton K] :
   C.monochromatic_of m c :=
 λ x hx y hy h, subsingleton.elim _ _
 
-lemma top_edge_labelling.monochromatic_of.comp_right (e : K → K') (h : C.monochromatic_of m c) :
+lemma monochromatic_of.comp_right (e : K → K') (h : C.monochromatic_of m c) :
   (C.comp_right e).monochromatic_of m (e c) :=
 λ x hx y hy h', by rw [top_edge_labelling.comp_right_get, h hx hy h']
 
-lemma top_edge_labelling.monochromatic_of_injective (e : K → K') (he : function.injective e) :
+lemma monochromatic_of_injective (e : K → K') (he : function.injective e) :
   (C.comp_right e).monochromatic_of m (e c) ↔ C.monochromatic_of m c :=
 forall₅_congr (λ x hx y hy h', by simp [he.eq_iff])
 
-lemma top_edge_labelling.monochromatic_of.subset {m' : set V} (h' : m' ⊆ m)
+lemma monochromatic_of.subset {m' : set V} (h' : m' ⊆ m)
   (h : C.monochromatic_of m c) : C.monochromatic_of m' c :=
 λ x hx y hy h'', h (h' hx) (h' hy) h''
 
-lemma top_edge_labelling.monochromatic_of.image {C : top_edge_labelling V' K} {f : V ↪ V'}
+lemma monochromatic_of.image {C : top_edge_labelling V' K} {f : V ↪ V'}
   (h : (C.pullback f).monochromatic_of m c) : C.monochromatic_of (f '' m) c :=
 by simpa [top_edge_labelling.monochromatic_of]
 
-lemma top_edge_labelling.monochromatic_of.map {C : top_edge_labelling V' K} {f : V ↪ V'}
+lemma monochromatic_of.map {C : top_edge_labelling V' K} {f : V ↪ V'}
   {m : finset V} (h : (C.pullback f).monochromatic_of m c) : C.monochromatic_of (m.map f) c :=
-by simpa [top_edge_labelling.monochromatic_of]
+by { rw [coe_map], exact h.image }
 
-lemma top_edge_labelling.monochromatic_of_insert {x : V} (hx : x ∉ m) :
+lemma monochromatic_of_insert {x : V} (hx : x ∉ m) :
   C.monochromatic_of (insert x m) c ↔
     C.monochromatic_of m c ∧ ∀ y ∈ m, C.get x y (H.ne_of_not_mem hx).symm = c :=
 begin
@@ -293,6 +293,88 @@ begin
   exact h₂ y hy,
 end
 
+/-- The predicate `χ.monochromatic_between X Y k` says every edge between `X` and `Y` is labelled
+`k` by the labelling `χ`. -/
+def monochromatic_between (C : top_edge_labelling V K) (X Y : finset V) (k : K) : Prop :=
+∀ ⦃x⦄, x ∈ X → ∀ ⦃y⦄, y ∈ Y → x ≠ y → C.get x y = k
+
+instance [decidable_eq V] [decidable_eq K] {X Y : finset V} {k : K} :
+  decidable (monochromatic_between C X Y k) :=
+finset.decidable_dforall_finset
+
+@[simp] lemma monochromatic_between_empty_left {Y : finset V} {k : K} :
+  C.monochromatic_between ∅ Y k :=
+by simp [monochromatic_between]
+
+@[simp] lemma monochromatic_between_empty_right {X : finset V} {k : K} :
+  C.monochromatic_between X ∅ k :=
+by simp [monochromatic_between]
+
+lemma monochromatic_between_singleton_left {x : V} {Y : finset V} {k : K} :
+  C.monochromatic_between {x} Y k ↔ ∀ ⦃y⦄, y ∈ Y → x ≠ y → C.get x y = k :=
+by simp [monochromatic_between]
+
+lemma monochromatic_between_singleton_right {y : V} {X : finset V} {k : K} :
+  C.monochromatic_between X {y} k ↔ ∀ ⦃x⦄, x ∈ X → x ≠ y → C.get x y = k :=
+by simp [monochromatic_between]
+
+lemma monochromatic_between_union_left [decidable_eq V] {X Y Z : finset V} {k : K} :
+  C.monochromatic_between (X ∪ Y) Z k ↔
+    C.monochromatic_between X Z k ∧ C.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} :
+  C.monochromatic_between X (Y ∪ Z) k ↔
+    C.monochromatic_between X Y k ∧ C.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} :
+  C.monochromatic_between X X k ↔ C.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) :
+  C.monochromatic_between X Y k ↔
+    ∀ ⦃x⦄, x ∈ X → ∀ ⦃y⦄, y ∈ Y → C.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 : C.monochromatic_between Y Z k) (hXY : X ⊆ Y) :
+  C.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 : C.monochromatic_between X Z k) (hXY : Y ⊆ Z) :
+  C.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 : C.monochromatic_between W X k) (hYW : Y ⊆ W) (hZX : Z ⊆ X) :
+  C.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 : C.monochromatic_between X Y k) :
+  C.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} :
+  C.monochromatic_between Y X k ↔ C.monochromatic_between X Y k :=
+⟨monochromatic_between.symm, monochromatic_between.symm⟩
+
+lemma monochromatic_of_union {X Y : finset V} {k : K} :
+  C.monochromatic_of (X ∪ Y) k ↔
+    C.monochromatic_of X k ∧ C.monochromatic_of Y k ∧ C.monochromatic_between X Y k :=
+begin
+  have : C.monochromatic_between X Y k ∧ C.monochromatic_between Y X k ↔
+    C.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
+
 open top_edge_labelling
 
 -- TODO (BM): I think the `∃` part of this should be its own def...
@@ -604,13 +686,6 @@ begin
   exact ⟨_, ramsey_fin_induct _ _ hN⟩,
 end
 
-lemma sum_tsub {α β : Type*} [add_comm_monoid β] [partial_order β] [has_exists_add_of_le β]
-  [covariant_class β β (+) (≤)] [contravariant_class β β (+) (≤)] [has_sub β] [has_ordered_sub β]
-  (s : finset α) {f g : α → β} (hfg : ∀ x ∈ s, g x ≤ f x) :
-  ∑ x in s, (f x - g x) = ∑ x in s, f x - ∑ x in s, g x :=
-eq_tsub_of_add_eq $ by rw [←finset.sum_add_distrib];
-  exact finset.sum_congr rfl (λ x hx, tsub_add_cancel_of_le $ hfg _ hx)
-
 -- hn can be weakened but it's just a nontriviality assumption
 lemma ramsey_fin_induct' [decidable_eq K] [fintype K] (n : K → ℕ) (N : K → ℕ)
   (hn : ∀ k, 2 ≤ n k) (hN : ∀ k, is_ramsey_valid (fin (N k)) (function.update n k (n k - 1))) :
@@ -637,49 +712,6 @@ end
 
 open matrix (vec_cons)
 
-lemma function.update_head {α : Type*} {i : ℕ} {x y : α} {t : fin i → α} :
-  function.update (vec_cons x t) 0 y = vec_cons y t :=
-begin
-  rw [function.funext_iff, fin.forall_fin_succ],
-  refine ⟨rfl, λ j, _⟩,
-  rw function.update_noteq,
-  { simp only [vec_cons, fin.cons_succ] },
-  exact fin.succ_ne_zero j
-end
-
-lemma function.update_one {α : Type*} {i : ℕ} {x y z : α} {t : fin i → α} :
-  function.update (vec_cons x (vec_cons y t)) 1 z = vec_cons x (vec_cons z t) :=
-begin
-  simp only [function.funext_iff, fin.forall_fin_succ],
-  refine ⟨rfl, rfl, λ j, _⟩,
-  rw function.update_noteq,
-  { simp only [vec_cons, fin.cons_succ] },
-  exact (fin.succ_injective _).ne (fin.succ_ne_zero _),
-end
-
-lemma function.update_two {α : Type*} {i : ℕ} {w x y z : α} {t : fin i → α} :
-  function.update (vec_cons w (vec_cons x (vec_cons y t))) 2 z =
-    vec_cons w (vec_cons x (vec_cons z t)) :=
-begin
-  simp only [function.funext_iff, fin.forall_fin_succ],
-  refine ⟨rfl, rfl, rfl, λ j, _⟩,
-  rw function.update_noteq,
-  { simp only [vec_cons, fin.cons_succ] },
-  exact (fin.succ_injective _).ne ((fin.succ_injective _).ne (fin.succ_ne_zero _))
-end
-
-lemma function.swap_cons {α : Type*} {i : ℕ} {x y : α} {t : fin i → α} :
-  vec_cons x (vec_cons y t) ∘ equiv.swap 0 1 = vec_cons y (vec_cons x t) :=
-begin
-  rw [function.funext_iff],
-  simp only [fin.forall_fin_succ],
-  refine ⟨rfl, rfl, λ j, _⟩,
-  simp only [vec_cons, fin.cons_succ, function.comp_apply],
-  rw [equiv.swap_apply_of_ne_of_ne, fin.cons_succ, fin.cons_succ],
-  { exact fin.succ_ne_zero _ },
-  exact (fin.succ_injective _).ne (fin.succ_ne_zero _)
-end
-
 theorem ramsey_fin_induct_two {i j Ni Nj : ℕ} (hi : 2 ≤ i) (hj : 2 ≤ j)
   (hi' : is_ramsey_valid (fin Ni) ![i - 1, j])
   (hj' : is_ramsey_valid (fin Nj) ![i, j - 1]) :
@@ -691,7 +723,7 @@ begin
   { rwa this at h },
   { rw fin.forall_fin_two,
     exact ⟨hi, hj⟩ },
-  { rw [fin.forall_fin_two, function.update_head, function.update_one],
+  { rw [fin.forall_fin_two, function.update_head, function.update_cons_one],
     exact ⟨hi', hj'⟩ },
 end
 
@@ -750,7 +782,7 @@ begin
     rw [add_add_add_comm, ←add_assoc, e] at this,
     simpa only [add_le_iff_nonpos_right, le_zero_iff, nat.one_ne_zero] using this },
   refine ramsey_fin_induct_aux ![Ni, Nj] m x _ (by simp) _ _,
-  { rw [fin.forall_fin_two, function.update_head, function.update_one],
+  { rw [fin.forall_fin_two, function.update_head, function.update_cons_one],
     exact ⟨hi', hj'⟩ },
   { rwa fin.exists_fin_two },
   { rw [fin.forall_fin_two],
@@ -772,7 +804,7 @@ begin
   { rw [fin.forall_fin_succ, fin.forall_fin_two],
     exact ⟨hi, hj, hk⟩ },
   { rw [fin.forall_fin_succ, fin.forall_fin_two, function.update_head, fin.succ_zero_eq_one',
-      fin.succ_one_eq_two', function.update_one, function.update_two],
+      fin.succ_one_eq_two', function.update_cons_one, function.update_cons_two],
     exact ⟨hi', hj', hk'⟩ }
 end
 
diff --git a/src/combinatorics/simple_graph/ramsey_prereq.lean b/src/combinatorics/simple_graph/ramsey_prereq.lean
index bf609dc183f36..9520a2c75faf8 100644
--- a/src/combinatorics/simple_graph/ramsey_prereq.lean
+++ b/src/combinatorics/simple_graph/ramsey_prereq.lean
@@ -11,6 +11,7 @@ import data.nat.choose.basic_mathlib
 import data.nat.choose.central_mathlib
 import data.nat.choose.sum_mathlib
 import data.nat.factorial.basic_mathlib
+import data.fin.vec_notation_mathlib
 
 /-!
 # Misc prereqs and collect imports
diff --git a/src/combinatorics/simple_graph/ramsey_small.lean b/src/combinatorics/simple_graph/ramsey_small.lean
index dababef3ff318..2c564150a78a4 100644
--- a/src/combinatorics/simple_graph/ramsey_small.lean
+++ b/src/combinatorics/simple_graph/ramsey_small.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import combinatorics.simple_graph.ramsey
+import number_theory.legendre_symbol.quadratic_char.gauss_sum
+import number_theory.legendre_symbol.quadratic_char.basic_mathlib
 
 /-!
 # Constructions to prove lower bounds on some small Ramsey numbers
@@ -18,15 +20,11 @@ section paley
 
 variables {F : Type*} [field F] [fintype F]
 
-lemma symmetric_is_square (hF : card F % 4 ≠ 3) :
-  symmetric (λ x y : F, is_square (x - y)) :=
-λ _ _ h, by simpa using h.mul (finite_field.is_square_neg_one_iff.2 hF)
-
 /--
 If `F` is a finite field with `|F| = 3 mod 4`, the Paley graph on `F` has an edge `x ~ y` if
 `x - y` is a (non-zero) quadratic residue.
-The definition should only be used if `card F % 4 ≠ 3`. If this condition fails, the graph is `⊤`,
-but it is still defined for convenience.
+The definition should only be used if `card F % 4 ≠ 3`. If this condition fails, the graph should
+be directed, but we define it here to just be `⊤` for convenience.
 -/
 def {u} paley_graph (F : Type*) [field F] [fintype F] : simple_graph F :=
 { adj := λ x y, x ≠ y ∧ (is_square (x - y) ∨ card F % 4 = 3),
@@ -83,7 +81,7 @@ def rescale (x : F) (hx : is_square x) (hx' : x ≠ 0) :
   end }
 
 /--
-The graph isomorphism witnessing that the Paley graph is self complementary: rescalingby a
+The graph isomorphism witnessing that the Paley graph is self complementary: rescaling by a
 non-square.
 -/
 @[simps]
@@ -111,6 +109,13 @@ def paley_labelling (F : Type*) [field F] [fintype F] [decidable_eq F] :
   top_edge_labelling F (fin 2) := to_edge_labelling (paley_graph F)
 
 -- smaller `k` don't need the paley construction
+/--
+If |F| is 1 mod 4, and the paley labelling contans a monochromatic subset of size k + 2, then `F`
+contains a subset of size k not containing 0 or 1, all of whose elements are squares and one more
+than squares; and all pairwise differences are square.
+For small `k` and `|F|`, this reduction is enough to brute-force check that such a configuration
+can be avoided.
+-/
 lemma no_paley_mono_set [decidable_eq F] {k : ℕ} (hF : card F % 4 = 1)
   (h : ∃ (m : finset F) c, (paley_labelling F).monochromatic_of m c ∧ k + 2 = m.card) :
   ∃ (m : finset F), m.card = k ∧ (0 : F) ∉ m ∧ (1 : F) ∉ m ∧
@@ -184,45 +189,6 @@ begin
   exact is_square_sub_of_paley_graph_adj card_not_three_mod_four (f.map_rel_iff.2 (ne.symm h)),
 end
 
--- #lint
-
-lemma card_non_zero_square_non_square {F : Type*} [fintype F] [field F] [decidable_eq F]
-  (hF : ring_char F ≠ 2) :
-  (univ.filter (λ x : F, x ≠ 0 ∧ is_square x)).card = card F / 2 ∧
-  (univ.filter (λ x : F, ¬ is_square x)).card = card F / 2 :=
-begin
-  have : (univ.filter (λ x : F, ¬ is_square x)) = (univ.filter (λ x : F, x ≠ 0 ∧ ¬ is_square x)),
-  { refine filter_congr _,
-    simp [not_imp_not] {contextual := tt} },
-  rw this,
-  have cf := quadratic_char_sum_zero hF,
-  simp only [quadratic_char_apply, quadratic_char_fun] at cf,
-  rw [sum_ite, sum_const_zero, zero_add, sum_ite, sum_const, sum_const, nsmul_eq_mul, nsmul_eq_mul,
-    mul_neg, mul_one, mul_one, add_neg_eq_zero, nat.cast_inj, filter_filter, filter_filter] at cf,
-  rw [←cf, and_self],
-  have : (univ.filter (λ x : F, x ≠ 0 ∧ is_square x)) ∪
-    (univ.filter (λ x : F, x ≠ 0 ∧ ¬ is_square x)) ∪ {0} = univ,
-  { simp only [←filter_or, ←and_or_distrib_left, em, and_true, filter_ne'],
-    rw [union_comm, ←insert_eq, insert_erase],
-    exact mem_univ _ },
-  have h' := congr_arg finset.card this,
-  rw [card_disjoint_union, card_disjoint_union, card_singleton, card_univ, ←cf, ←two_mul,
-    ←bit0_eq_two_mul, ←bit1] at h',
-  { rw [←h', nat.bit1_div_two] },
-  { rw finset.disjoint_left,
-    simp {contextual := tt} },
-  { simp },
-end
-
-lemma card_square (F : Type*) [fintype F] [field F] (hF : ring_char F ≠ 2) :
-  ((univ : finset F).filter is_square).card = card F / 2 + 1 :=
-begin
-  rw [←(card_non_zero_square_non_square hF).1],
-  simp only [and_comm, ←filter_filter, filter_ne'],
-  rw card_erase_add_one,
-  simp
-end
-
 lemma paley_five_bound : ¬ is_ramsey_valid (zmod 5) ![3, 3] :=
 begin
   haveI : fact (nat.prime 5) := ⟨by norm_num⟩,
@@ -244,6 +210,7 @@ lemma paley_seventeen_helper :
   ∀ (a : zmod 17), a ≠ 0 → a ≠ 1 → is_square a → is_square (a - 1) → a = 2 ∨ a = 9 ∨ a = 16 :=
 by dec_trivial
 
+-- No pair from {2, 9, 16} has difference a square.
 lemma paley_seventeen_bound : ¬ is_ramsey_valid (zmod 17) ![4, 4] :=
 begin
   haveI : fact (nat.prime 17) := ⟨by norm_num⟩,
@@ -275,14 +242,16 @@ end
 
 end paley
 
-lemma diagonal_ramsey_three : diagonal_ramsey 3 = 6 :=
+lemma ramsey_number_three_three : ramsey_number ![3, 3] = 6 :=
 begin
   refine le_antisymm _ _,
   { exact (ramsey_number_two_colour_bound 3 3 (by norm_num)).trans_eq (by simp) },
-  rw [←not_lt, nat.lt_succ_iff, ←zmod.card 5, diagonal_ramsey.def, ramsey_number_le_iff],
+  rw [←not_lt, nat.lt_succ_iff, ←zmod.card 5, ramsey_number_le_iff],
   exact paley_five_bound
 end
 
+lemma diagonal_ramsey_three : diagonal_ramsey 3 = 6 := ramsey_number_three_three
+
 lemma ramsey_number_three_four_upper : ramsey_number ![3, 4] ≤ 9 :=
 begin
   refine (ramsey_number_two_colour_bound_even 4 6 _ _ _ _ _ _).trans_eq _,
@@ -295,17 +264,19 @@ begin
   { norm_num },
 end
 
-lemma diagonal_ramsey_four : diagonal_ramsey 4 = 18 :=
+lemma ramsey_number_four_four : ramsey_number ![4, 4] = 18 :=
 begin
   refine le_antisymm _ _,
   { refine (ramsey_number_two_colour_bound 4 4 (by norm_num)).trans _,
     simp only [nat.succ_sub_succ_eq_sub, tsub_zero],
     rw ramsey_number_pair_swap 4,
     linarith [ramsey_number_three_four_upper] },
-  rw [←not_lt, nat.lt_succ_iff, ←zmod.card 17, diagonal_ramsey.def, ramsey_number_le_iff],
+  rw [←not_lt, nat.lt_succ_iff, ←zmod.card 17, ramsey_number_le_iff],
   exact paley_seventeen_bound
 end
 
+lemma diagonal_ramsey_four : diagonal_ramsey 4 = 18 := ramsey_number_four_four
+
 lemma ramsey_number_three_four : ramsey_number ![3, 4] = 9 :=
 begin
   refine eq_of_le_of_not_lt ramsey_number_three_four_upper _,
@@ -376,7 +347,7 @@ open top_edge_labelling
 
 /--
 an explicit definition of the clebsch colouring
-TODO: find the source i used for this
+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
diff --git a/src/data/fin/vec_notation_mathlib.lean b/src/data/fin/vec_notation_mathlib.lean
new file mode 100644
index 0000000000000..b806215d83e4f
--- /dev/null
+++ b/src/data/fin/vec_notation_mathlib.lean
@@ -0,0 +1,50 @@
+import data.fin.vec_notation
+
+namespace function
+open matrix (vec_cons)
+open fin
+
+lemma update_head {α : Type*} {i : ℕ} {x y : α} {t : fin i → α} :
+  update (vec_cons x t) 0 y = vec_cons y t :=
+begin
+  rw [funext_iff, fin.forall_fin_succ],
+  refine ⟨rfl, λ j, _⟩,
+  rw update_noteq,
+  { simp only [vec_cons, fin.cons_succ] },
+  exact succ_ne_zero j
+end
+
+lemma update_cons_one {α : Type*} {i : ℕ} {x y z : α} {t : fin i → α} :
+  update (vec_cons x (vec_cons y t)) 1 z = vec_cons x (vec_cons z t) :=
+begin
+  simp only [funext_iff, forall_fin_succ],
+  refine ⟨rfl, rfl, λ j, _⟩,
+  rw update_noteq,
+  { simp only [vec_cons, cons_succ] },
+  exact (succ_injective _).ne (fin.succ_ne_zero _),
+end
+
+lemma update_cons_two {α : Type*} {i : ℕ} {w x y z : α} {t : fin i → α} :
+  update (vec_cons w (vec_cons x (vec_cons y t))) 2 z =
+    vec_cons w (vec_cons x (vec_cons z t)) :=
+begin
+  simp only [funext_iff, forall_fin_succ],
+  refine ⟨rfl, rfl, rfl, λ j, _⟩,
+  rw update_noteq,
+  { simp only [vec_cons, cons_succ] },
+  exact (succ_injective _).ne ((succ_injective _).ne (succ_ne_zero _))
+end
+
+lemma swap_cons {α : Type*} {i : ℕ} {x y : α} {t : fin i → α} :
+  vec_cons x (vec_cons y t) ∘ equiv.swap 0 1 = vec_cons y (vec_cons x t) :=
+begin
+  rw [funext_iff],
+  simp only [forall_fin_succ],
+  refine ⟨rfl, rfl, λ j, _⟩,
+  simp only [vec_cons, cons_succ, comp_apply],
+  rw [equiv.swap_apply_of_ne_of_ne, cons_succ, cons_succ],
+  { exact succ_ne_zero _ },
+  exact (succ_injective _).ne (succ_ne_zero _)
+end
+
+end function
diff --git a/src/number_theory/legendre_symbol/quadratic_char/basic_mathlib.lean b/src/number_theory/legendre_symbol/quadratic_char/basic_mathlib.lean
new file mode 100644
index 0000000000000..7b88075087999
--- /dev/null
+++ b/src/number_theory/legendre_symbol/quadratic_char/basic_mathlib.lean
@@ -0,0 +1,47 @@
+import data.fintype.parity
+import number_theory.legendre_symbol.quadratic_char.basic
+
+open fintype (card)
+open finset
+
+variables {F : Type*} [fintype F] [field F]
+
+lemma symmetric_is_square (hF : card F % 4 ≠ 3) :
+  symmetric (λ x y : F, is_square (x - y)) :=
+λ _ _ h, by simpa using h.mul (finite_field.is_square_neg_one_iff.2 hF)
+
+lemma card_non_zero_square_non_square [decidable_eq F] (hF : ring_char F ≠ 2) :
+  (univ.filter (λ x : F, x ≠ 0 ∧ is_square x)).card = card F / 2 ∧
+  (univ.filter (λ x : F, ¬ is_square x)).card = card F / 2 :=
+begin
+  have : (univ.filter (λ x : F, ¬ is_square x)) = (univ.filter (λ x : F, x ≠ 0 ∧ ¬ is_square x)),
+  { refine filter_congr _,
+    simp [not_imp_not] {contextual := tt} },
+  rw this,
+  have cf := quadratic_char_sum_zero hF,
+  simp only [quadratic_char_apply, quadratic_char_fun] at cf,
+  rw [sum_ite, sum_const_zero, zero_add, sum_ite, sum_const, sum_const, nsmul_eq_mul, nsmul_eq_mul,
+    mul_neg, mul_one, mul_one, add_neg_eq_zero, nat.cast_inj, filter_filter, filter_filter] at cf,
+  rw [←cf, and_self],
+  have : (univ.filter (λ x : F, x ≠ 0 ∧ is_square x)) ∪
+    (univ.filter (λ x : F, x ≠ 0 ∧ ¬ is_square x)) ∪ {0} = univ,
+  { simp only [←filter_or, ←and_or_distrib_left, em, and_true, filter_ne'],
+    rw [union_comm, ←insert_eq, insert_erase],
+    exact mem_univ _ },
+  have h' := congr_arg finset.card this,
+  rw [card_disjoint_union, card_disjoint_union, card_singleton, card_univ, ←cf, ←two_mul,
+    ←bit0_eq_two_mul, ←bit1] at h',
+  { rw [←h', nat.bit1_div_two] },
+  { rw finset.disjoint_left,
+    simp {contextual := tt} },
+  { simp },
+end
+
+lemma card_square (F : Type*) [fintype F] [field F] [decidable_eq F] (hF : ring_char F ≠ 2) :
+  ((univ : finset F).filter is_square).card = card F / 2 + 1 :=
+begin
+  rw [←(card_non_zero_square_non_square hF).1],
+  simp only [and_comm, ←filter_filter, filter_ne'],
+  rw card_erase_add_one,
+  simp
+end