From 8b8de124e373953390973164d57a5ea26c4c4f2d Mon Sep 17 00:00:00 2001
From: Bhavik Mehta <bhavikmehta8@gmail.com>
Date: Thu, 28 Sep 2023 19:50:52 +0100
Subject: [PATCH] hmm.

---
 .../simple_graph/exponential_ramsey/section5.lean        | 8 ++++----
 .../simple_graph/exponential_ramsey/section6.lean        | 9 ++++-----
 .../simple_graph/exponential_ramsey/section9.lean        | 4 ++--
 3 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section5.lean b/src/combinatorics/simple_graph/exponential_ramsey/section5.lean
index 082ba46ac31e3..eddc847d562f4 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section5.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section5.lean
@@ -29,7 +29,7 @@ namespace simple_graph
 
 open_locale exponential_ramsey
 
-open filter finset nat
+open filter finset
 
 lemma top_adjuster {α : Type*} [semilattice_sup α] [nonempty α] {p : α → Prop}
   (h : ∀ᶠ k : α in at_top, p k) :
@@ -134,7 +134,7 @@ begin
   rw [rpow_def_of_pos, ←mul_assoc, ←mul_assoc, mul_comm, ←rpow_def_of_pos hk₀'],
   swap,
   { positivity },
-  have : real.log 2 * (4 / 5 * 2) ≤ log (1 + ε) * (4 / 5) * (2 / ε),
+  have : log 2 * (4 / 5 * 2) ≤ log (1 + ε) * (4 / 5) * (2 / ε),
   { rw [mul_div_assoc' _ _ ε, le_div_iff' hε, ←mul_assoc, mul_assoc (real.log _)],
     refine mul_le_mul_of_nonneg_right (mul_log_two_le_log_one_add hε.le hε₁) _,
     norm_num1 },
@@ -686,13 +686,13 @@ begin
   rw [degree_regularisation_applied hi, book_config.degree_regularisation_step_X, mem_filter] at hx,
   rw [degree_steps, mem_filter, mem_range] at hi,
   change (1 - (k : ℝ) ^ (- 1 / 8 : ℝ)) * C.p * C.Y.card ≤ (red_neighbors χ x ∩ C.Y).card,
-  change x ∈ C.X ∧ (C.p - _ * α_function k (C.height k ini.p)) * (C.Y.card : ℝ) ≤
+  change x ∈ C.X ∧ (C.p - _ * α_function k (height k ini.p C.p)) * (C.Y.card : ℝ) ≤
     (red_neighbors χ x ∩ C.Y).card at hx,
   have : 1 / (k : ℝ) < C.p := one_div_k_lt_p_of_lt_final_step hi.1,
   refine hx.2.trans' (mul_le_mul_of_nonneg_right _ (nat.cast_nonneg _)),
   rw [one_sub_mul, sub_le_sub_iff_left],
   cases le_total C.p (q_function k ini.p 0) with h' h',
-  { rw [book_config.height, five_seven_extra, α_one, mul_div_assoc', ←rpow_add' (nat.cast_nonneg _),
+  { rw [five_seven_extra, α_one, mul_div_assoc', ←rpow_add' (nat.cast_nonneg _),
       div_eq_mul_one_div],
     { refine (mul_le_mul_of_nonneg_left this.le (rpow_nonneg_of_nonneg (nat.cast_nonneg _)
         _)).trans_eq _,
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section6.lean b/src/combinatorics/simple_graph/exponential_ramsey/section6.lean
index 2e29001ce92dd..b373139816dec 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section6.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section6.lean
@@ -12,7 +12,7 @@ namespace simple_graph
 
 open_locale big_operators exponential_ramsey
 
-open filter finset nat real
+open filter finset real
 
 variables {V : Type*} [decidable_eq V] [fintype V] {χ : top_edge_labelling V (fin 2)}
 variables {k l : ℕ} {ini : book_config χ} {i : ℕ}
@@ -108,7 +108,7 @@ begin
   rw [degree_regularisation_applied hi, book_config.degree_regularisation_step_X,
     book_config.degree_regularisation_step_Y],
   set C := algorithm μ k l ini i,
-  set α := α_function k (C.height k ini.p),
+  set α := α_function k (height k ini.p C.p),
   rw col_density_eq_average,
   have : C.X.filter (λ x, (C.p - k ^ (1 / 8 : ℝ) * α) * C.Y.card ≤
     ((col_neighbors χ 0 x ∩ C.Y).card)) = C.X.filter (λ x, C.p - k ^ (1 / 8 : ℝ) * α ≤
@@ -153,7 +153,7 @@ begin
   rw [col_density_eq_average],
   let C := algorithm μ k l ini i,
   let C' := algorithm μ k l ini (i + 1),
-  have : ∀ x ∈ (C'.big_blue_step μ).X, C.p - k ^ (1 / 8 : ℝ) * α_function k (C.height k ini.p) ≤
+  have : ∀ x ∈ (C'.big_blue_step μ).X, C.p - k ^ (1 / 8 : ℝ) * α_function k (height k ini.p C.p) ≤
     (red_neighbors χ x ∩ C.Y).card / C.Y.card,
   { intros x hx,
     have : x ∈ (algorithm μ k l ini (i + 1)).X := book_config.get_book_snd_subset hx,
@@ -167,7 +167,6 @@ begin
   refine (div_le_div_of_le _ (card_nsmul_le_sum _ _ _ this)).trans' _,
   { exact nat.cast_nonneg _ },
   rw [book_config.big_blue_step_X, nsmul_eq_mul, mul_div_cancel_left],
-  { refl },
   rw [nat.cast_ne_zero, ←pos_iff_ne_zero, card_pos],
   refine book_config.get_book_snd_nonempty hμ₀ _,
   exact X_nonempty h,
@@ -320,7 +319,7 @@ end
 lemma convex_thing_aux {x : ℝ} (hε : 0 ≤ x) (hx' : x ≤ 2 / 7) :
   exp (-(7 * log 2 / 4 * x)) ≤ 1 - 7 / 2 * (1 - 1 / sqrt 2) * x :=
 begin
-  have h' : 0 < log 2 := log_pos (by norm_num),
+  have h' : (0 : ℝ) < log 2 := log_pos (by norm_num),
   let a := - log 2 / 2,
   have : - log 2 / 2 ≠ 0,
   { norm_num },
diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section9.lean b/src/combinatorics/simple_graph/exponential_ramsey/section9.lean
index c1e6899ec2ede..47af65d247490 100644
--- a/src/combinatorics/simple_graph/exponential_ramsey/section9.lean
+++ b/src/combinatorics/simple_graph/exponential_ramsey/section9.lean
@@ -629,10 +629,10 @@ lemma strict_convex_on.const_mul {c : ℝ} {s : set ℝ} {f : ℝ → ℝ} (hf :
   hc).trans_eq (by simp only [smul_eq_mul]; ring_nf)⟩
 
 lemma convex_on_inv : convex_on ℝ (set.Ioi (0 : ℝ)) (λ x, x⁻¹) :=
-convex_on.congr (convex_on_zpow (-1)) (by simp)
+convex_on.congr' (convex_on_zpow (-1)) (by simp)
 
 lemma convex_on_one_div : convex_on ℝ (set.Ioi (0 : ℝ)) (λ x, 1 / x) :=
-convex_on.congr (convex_on_zpow (-1)) (by simp)
+convex_on.congr' (convex_on_zpow (-1)) (by simp)
 
 lemma quadratic_is_concave {a b c : ℝ} (ha : 0 < a) :
   strict_convex_on ℝ set.univ (λ x, a * x ^ 2 + b * x + c) :=