From 525e1760bc7dbe0467e1612479fab9f328b14a78 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 8 May 2024 02:50:22 -0700
Subject: [PATCH] Update to Lean 4.7.0

No statements have changed.

Within the proofs, the main change is that `simp` no longer has `decide := true` as a default.
Some other theorems were renamed upstream.

PiperOrigin-RevId: 631717078
Change-Id: I1c59a179f69d16081eaa8dce1c90847876a58c89
---
 Comp/Basic.lean     |   4 +-
 Debate/Cost.lean    |   9 ++--
 Debate/Details.lean |  44 ++++++++---------
 Misc/Finset.lean    |   6 +--
 Misc/If.lean        |   6 +--
 Prob/Arith.lean     |  11 +++--
 Prob/Basics.lean    |   2 +-
 Prob/Bernoulli.lean |  13 ++---
 Prob/Chernoff.lean  |  16 +++---
 Prob/Cond.lean      |  16 +++---
 Prob/Defs.lean      |   2 +-
 Prob/Estimate.lean  |   6 +--
 Prob/Pmf.lean       |   2 +-
 lake-manifest.json  | 118 +++++++++++++++++++++++++-------------------
 lakefile.lean       |   2 +-
 lean-toolchain      |   2 +-
 16 files changed, 136 insertions(+), 123 deletions(-)

diff --git a/Comp/Basic.lean b/Comp/Basic.lean
index a56bb3d..6bb689b 100644
--- a/Comp/Basic.lean
+++ b/Comp/Basic.lean
@@ -101,7 +101,7 @@ lemma cost_of_not_mem (f : Comp s α) (o : I → Oracle) {i : I} (is : i ∉ s)
   · simp only [cost_sample, h, exp_const]
   · simp only [cost_query', h0, h1, ite_self, exp_const, add_zero]
     by_cases ij : i = j
-    · simp only [ij] at is; simp only [js] at is
+    · simp only [ij] at is; simp (config := {decide := true}) only [js] at is
     · simp only [ij, if_false]
 
 /-- Expanding `query'.run` -/
@@ -307,7 +307,7 @@ macro "not_mem" : tactic =>
 
 /-- Show `s ⊆ t` via `simp` -/
 macro "subset" : tactic =>
-  `(tactic| simp only [Set.mem_singleton_iff, Set.singleton_subset_iff, Set.mem_insert_iff,
+  `(tactic| simp (config := {decide := true}) only [Set.mem_singleton_iff, Set.singleton_subset_iff, Set.mem_insert_iff,
     or_false])
 
 /-- Show a cost is zero via `i : I` not being in `s` -/
diff --git a/Debate/Cost.lean b/Debate/Cost.lean
index 517abda..a973f81 100644
--- a/Debate/Cost.lean
+++ b/Debate/Cost.lean
@@ -7,9 +7,6 @@ import Debate.Protocol
 See `Correct.lean` for the summary.
 -/
 
--- Work around https://github.com/leanprover/lean4/issues/2220
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- See issue lean4#2220
-
 open Classical
 open Prob
 open Option (some none)
@@ -158,10 +155,10 @@ lemma post_stepsV (alice : Alice) (bob : Bob) (vera : Vera) :
         postV, bind_assoc, step]
       apply congr_arg₂ _ rfl ?_; ext p; apply congr_arg₂ _ rfl ?_; ext b
       induction b
-      · simp only [ite_false, Comp.allow_all_pure, pure_bind]
-      · simp only [ite_true]
+      · simp only [ite_false, Comp.allow_all_pure, pure_bind, postV]
+      · simp only [ite_cond_eq_true]
         rw [Comp.allow_all, Comp.allow, bind_assoc]
-        simp only [Comp.allow, pure_bind, Comp.sample'_bind]
+        simp only [Comp.allow, pure_bind, Comp.sample'_bind, postV]
 
 /-- Vera makes few queries, regardless of Alice and Bob -/
 theorem vera_debate_cost (o : Oracle) (alice : Alice) (bob : Bob) (t : ℕ):
diff --git a/Debate/Details.lean b/Debate/Details.lean
index 5fea613..97bbc7b 100644
--- a/Debate/Details.lean
+++ b/Debate/Details.lean
@@ -56,14 +56,14 @@ lemma alice_pr_le (e0 : 0 < e) (q0 : 0 < q) (y : Vector Bool n) :
 lemma le_alice_pr (o : Oracle) (i : OracleId) (e0 : 0 < e) (q0 : 0 < q) (y : Vector Bool n) :
     1 - q ≤ ((alice' e q i _ y).prob' o).pr (λ p ↦ |p - (o _ y).prob true| ≤ e) := by
   trans ((alice' e q i _ y).prob' o).pr (λ p ↦ |p - (o _ y).prob true| < e)
-  · rw [pr_neg']; simp only [not_lt]; linarith [alice_pr_le e0 q0 y]
+  · rw [pr_neg']; simp only [not_lt]; linarith [alice_pr_le (i := i) (o := o) e0 q0 y]
   · apply pr_mono; intro _ _ h; exact le_of_lt h
 
 /-- Honest Bob usually accepts if Alice is off by ≤ c -/
 lemma bob_complete (o : Oracle) (i : OracleId) (cs : c < s) (q0 : 0 < q) {y : Vector Bool n}
     (good : |p - (o _ y).prob true| ≤ c) :
     ((bob' c s q i _ y p).prob' o).prob false ≤ q := by
-  simp only [bob', prob_bind, prob_pure, Bool.false_eq_decide_iff, not_lt, Comp.prob',
+  simp only [bob', prob_bind, prob_pure, false_eq_decide_iff, not_lt, Comp.prob',
     Comp.prob_bind, Comp.prob_pure]
   rw [←pr]
   refine' le_trans (pr_mono _) (alice_pr_le (by linarith) q0 y)
@@ -78,7 +78,7 @@ lemma bob_complete (o : Oracle) (i : OracleId) (cs : c < s) (q0 : 0 < q) {y : Ve
 lemma bob_sound (o : Oracle) (i : OracleId) (cs : c < s) (q0 : 0 < q) {y : Vector Bool n}
     (bad : |p - (o _ y).prob true| ≥ s) :
     ((bob' c s q i _ y p).prob' o).prob true ≤ q := by
-  simp only [bob', prob_bind, prob_pure, Bool.true_eq_decide_iff, not_lt, Comp.prob',
+  simp only [bob', prob_bind, prob_pure, true_eq_decide_iff, not_lt, Comp.prob',
     Comp.prob_bind, Comp.prob_pure]
   rw [←pr]
   refine' le_trans (pr_mono _) (alice_pr_le (by linarith) q0 y)
@@ -293,7 +293,7 @@ lemma alices_close (o : Oracle) (e0 : 0 < e) (q0 : 0 < q) (q1 : q ≤ 1) :
     (1 - q)^n ≤ (alices o (alice e q) n).pr (fun (p,y) ↦ close p (o.probs y) e) := by
   induction' n with n h
   · simp only [Nat.zero_eq, pow_zero, alices, close_nil, pr_pure, if_true, le_refl]
-  · simp only [pow_succ', alices, Oracle.probs, pr_bind, pr_pure, Vector.tail_cons, close_cons, ite_and_one_zero,
+  · simp only [pow_succ, alices, Oracle.probs, pr_bind, pr_pure, Vector.tail_cons, close_cons, ite_and_one_zero,
       exp_const_mul, exp_const, exp_mul_const]
     apply le_exp_of_cut (fun (p,y) ↦ close p (o.probs y) e) ((1 - q)^n) (1 - q)
     · apply h
@@ -328,7 +328,7 @@ lemma alices_success (o : Oracle) (L : o.lipschitz t k) (e0 : 0 < e) (q0 : 0 < q
           by_cases c : close p (o.probs y) e
           · simp only [c, if_true, mul_one, snaps_prob _ c]
           · simp only [c, if_false, mul_zero]
-        simp only [pr_neg, ae]; linarith [alices_close o e0 q0 q1]
+        simp only [pr_neg, ae]; linarith [alices_close (n := t + 1) o e0 q0 q1]
 
 /-- If Alice is correct and Bob rejects, the probability of false is low -/
 lemma evil_bobs_lies' (o : Oracle) (eve : Bob) (cs : c < s) (v0 : 0 < v)
@@ -336,26 +336,26 @@ lemma evil_bobs_lies' (o : Oracle) (eve : Bob) (cs : c < s) (v0 : 0 < v)
     (bobs o eve (vera c s v) p y).cond (λ r ↦ r = some false) (λ r ↦ r.isSome) ≤ v := by
   have v0' := le_of_lt v0
   induction' n with n h
-  · simp only [bobs, cond_pure, if_false, v0']
+  · simp (config := {decide := true}) only [bobs, cond_pure, if_false, v0']
   · simp only [close_succ, Vector.eq_cons_iff] at py
     apply le_trans (cond_bind_le_of_cut (λ r ↦ r.isSome)); apply max_le
     · refine' le_trans (cond_bind_le_first (λ r ↦ r = some false)
         (λ r ↦ r.isSome) (λ r ↦ r = some false) (λ r ↦ r.isSome) _ _) _;
       · intro r s pr ps r0 s0 _; match r with
-        | none => simp only at r0 | some false => rfl
-        | some true => simp only [s0, prob_pure, ite_false, ne_eq, not_true] at ps
+        | none => simp (config := {decide := true}) only at r0 | some false => rfl
+        | some true => simp (config := {decide := true}) only [s0, prob_pure, ite_false, ne_eq, not_true] at ps
       · intro r s pr ps ri; match r with
-        | none => simp only at ri
+        | none => simp (config := {decide := true}) only at ri
         | some r => simp only [prob_pure, ite_one_zero_ne_zero] at ps; simp only [ps, Option.isSome]
       · exact h py.2
     · refine' cond_bind_le_second (λ r ↦ r = some false) (λ r ↦ r.isSome)
         (λ r : Option Bool ↦ ¬r.isSome) v0' _
       intro r pr ri; match r with
-      | some _ => simp only [Option.isSome] at ri
+      | some _ => simp (config := {decide := true}) only [Option.isSome] at ri
       | none =>
           simp only; apply cond_bind_le_of_forall_le v0'
           intro b _; match b with
-          | true => simp only [if_true, bind_const, cond_pure, if_false, v0']
+          | true => simp (config := {decide := true}) only [if_true, bind_const, cond_pure, if_false, v0']
           | false =>
             simp only [if_false]; rw [cond_eq_pr]
             · refine' le_trans _ (bob_complete o VeraId cs v0 py.1)
@@ -374,13 +374,13 @@ lemma evil_bobs_lies (o : Oracle) (eve : Bob) (cs : c < s) (v0 : 0 < v)
   rw [pr_eq_cond_add_cond (λ r : Option Bool ↦ r.isSome)]
   have b1 : (bobs o eve (vera c s v) p y).cond (λ r ↦ extract ((p,y),r) = false) (λ r ↦ ¬r.isSome) = 0 := by
     apply cond_eq_zero; intro r _ ri
-    simp only [Option.not_isSome_iff_eq_none] at ri; simp only [ri, extract, yt]
+    simp only [Option.not_isSome_iff_eq_none] at ri; simp (config := {decide := true}) only [ri, extract, yt]
   simp only [b1, zero_mul, add_zero]
   refine' le_trans (mul_le_of_le_one_right cond_nonneg pr_le_one) _
   refine' le_trans (le_of_eq _) (evil_bobs_lies' o eve cs v0 py)
   apply cond_congr; intro r _ ri; match r with
   | some r => simp only [extract, Option.some_inj]
-  | none => simp only at ri
+  | none => simp (config := {decide := true}) only at ri
 
 /-- Alice wins the debate with good probability -/
 theorem completeness' (o : Oracle) (L : o.lipschitz t k) (eve : Bob)
@@ -436,7 +436,7 @@ def vera_score (v : ℝ) : Option Bool → ℝ
 
 /-- Option Bool's univ-/
 lemma option_bool_univ : (Finset.univ : Finset (Option Bool)) = {some true, some false, none} := by
-  simp only
+  simp (config := {decide := true}) only
 
 /-- If Honest Bob rejects, Vera usually complains.  The error probability is higher if Bob
     does complain, though, so we use an expectation over vera_score. -/
@@ -446,7 +446,7 @@ lemma bobs_safe (o : Oracle) (cs : c < s) (sb : s < b) (q0 : 0 < q) (v0 : 0 < v)
   induction' n with n h
   · simp only [Nat.zero_eq, pow_zero, mul_one, bobs, vera_score, exp_pure, le_refl]
   · simp only [bobs, exp_bind]; specialize h p.tail y.tail
-    simp only [Nat.succ_sub_one, vera_score, @exp_fintype (Option Bool), option_bool_univ, Finset.mem_singleton,
+    simp (config := {decide := true}) only [Nat.succ_sub_one, vera_score, @exp_fintype (Option Bool), option_bool_univ, Finset.mem_singleton,
       Finset.mem_insert, not_false_eq_true, Finset.sum_insert, mul_zero, Finset.sum_singleton, mul_one, zero_add,
       prob_pure, ite_false, zero_mul, add_zero, ite_true, one_mul, prob_bind, ←exp_add] at h ⊢
     generalize hbs : bobs o (bob s b q) (vera c s v) p.tail y.tail = bs
@@ -454,7 +454,7 @@ lemma bobs_safe (o : Oracle) (cs : c < s) (sb : s < b) (q0 : 0 < q) (v0 : 0 < v)
     generalize hbn : (bob s b q n y.tail p.head).prob' o = bn
     trans (bs.prob (some false) + bs.prob none * (1 - v)) * (1 - q)
     · refine le_trans ?_ (mul_le_mul_of_nonneg_right h (by linarith))
-      rw [mul_assoc, ←pow_succ']
+      rw [mul_assoc, ←pow_succ]
     · simp only [add_mul]; apply add_le_add
       · exact mul_le_of_le_one_right (prob_nonneg _) (by linarith)
       · rw [mul_assoc]; refine mul_le_mul_of_nonneg_left ?_ (prob_nonneg _)
@@ -485,20 +485,20 @@ lemma bobs_catches (o : Oracle) (cs : c < s) (sb : s < b) (q0 : 0 < q) (v0 : 0 <
     {p : Vector ℝ n} {y : Vector Bool n} (pb : ¬close p (o.probs y) b) :
     (1 - v) * (1 - q) ^ n ≤ (bobs o (bob s b q) (vera c s v) p y).pr (λ r ↦ r = some false) := by
   induction' n with n h
-  · simp only [Vector.eq_nil, close_nil] at pb
+  · simp (config := {decide := true}) only [Vector.eq_nil, close_nil] at pb
   · by_cases pbn : close p.tail (o.probs y.tail) b
     · have safe := bobs_safe o cs sb q0 v0 v1 qv p.tail y.tail
-      simp only [bobs, Nat.succ_sub_one, pr_bind, @exp_fintype (Option Bool), option_bool_univ,
+      simp (config := {decide := true}) only [bobs, Nat.succ_sub_one, pr_bind, @exp_fintype (Option Bool), option_bool_univ,
         Finset.mem_singleton, Finset.mem_insert, not_false_eq_true, Finset.sum_insert, pr_pure, ite_false,
         mul_zero, ite_true, mul_one, Finset.sum_singleton, zero_add, ge_iff_le, vera_score] at safe ⊢
       generalize hbs : bobs o (bob s b q) (vera c s v) p.tail y.tail = bs; simp only [hbs] at safe
       trans (bs.prob (some false) + bs.prob none * (1 - v)) * (1 - q)
       · refine le_trans ?_ (mul_le_mul_of_nonneg_right safe (by linarith))
-        rw [mul_assoc, ←pow_succ']
+        rw [mul_assoc, ←pow_succ]
       · simp only [add_mul]; apply add_le_add
         · exact mul_le_of_le_one_right (prob_nonneg _) (by linarith)
         · rw [mul_assoc]; refine mul_le_mul_of_nonneg_left ?_ (prob_nonneg _)
-          simp only [close_succ, not_and_or, pbn, Oracle.probs, Vector.tail_cons, Vector.head_cons,
+          simp (config := {decide := true}) only [close_succ, not_and_or, pbn, Oracle.probs, Vector.tail_cons, Vector.head_cons,
             or_false, Nat.succ_sub_one, not_le] at pb
           rw [mul_comm]; refine le_exp_of_cut (fun x ↦ x = false) (1-q) (1-v) ?_ ?_ ?_ (by linarith)
           · have bs := bob_sound o BobId sb q0 (le_of_lt pb)
@@ -512,7 +512,7 @@ lemma bobs_catches (o : Oracle) (cs : c < s) (sb : s < b) (q0 : 0 < q) (v0 : 0 <
           · intro _ _ t; simp only [Bool.not_eq_false] at t; simp only [t, if_true, if_false, exp_const, le_refl]
     · specialize h pbn
       refine le_trans ?_ (le_pr_bind_of_cut _ (1-q) h ?_ (by linarith))
-      · rw [mul_assoc, pow_succ']
+      · rw [mul_assoc, pow_succ]
       · intro _ _ f; simp only [f, pr_pure, if_true]; linarith
 
 /-- Bob wins the debate with probability ≥ 8/15 -/
@@ -531,7 +531,7 @@ theorem soundness' (o : Oracle) (L : o.lipschitz t k) (eve : Alice)
     · simp only at h; simp only [pr]
       have safe := bobs_safe o cs sb q0 v0 v1 qv p y
       generalize hbs : bobs o (bob s b q) (vera c s v) p y = bs; simp only [hbs] at safe
-      simp only [extract, h, @exp_fintype (Option Bool), option_bool_univ, Finset.mem_singleton,
+      simp (config := {decide := true}) only [extract, h, @exp_fintype (Option Bool), option_bool_univ, Finset.mem_singleton,
         Finset.mem_insert, mul_ite, mul_one, mul_zero, not_false_eq_true, Finset.sum_insert, ite_false,
         ite_true, Finset.sum_singleton, zero_add, ge_iff_le, vera_score] at safe ⊢
       exact le_trans safe (add_le_add_left (mul_le_of_le_one_right (prob_nonneg _) (by linarith)) _)
diff --git a/Misc/Finset.lean b/Misc/Finset.lean
index ec50dbe..4ef7c91 100644
--- a/Misc/Finset.lean
+++ b/Misc/Finset.lean
@@ -1,7 +1,7 @@
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Real.ENNReal
+import Mathlib.Data.ENNReal.Basic
 import Mathlib.Topology.Algebra.InfiniteSum.Basic
 import Mathlib.Topology.Instances.ENNReal
 
@@ -47,8 +47,8 @@ lemma Finset.sum_le_sum_of_map {s : Finset α} {t : Finset β} {u : α → ℝ}
   rw [e]; clear e
   refine' le_trans _ (le_add_of_nonneg_right _)
   · rw [Finset.sum_image]
-    · apply Finset.sum_le_sum; intro x m; simp only [mem_filter] at m; exact le _ m.2
-    · intro x m y n; simp only [mem_filter] at m n; apply inj _ _ m.2 n.2
+    · apply Finset.sum_le_sum; intro x m; simp only [mem_filter, s'] at m; exact le _ m.2
+    · intro x m y n; simp only [mem_filter, s'] at m n; apply inj _ _ m.2 n.2
   · apply Finset.sum_nonneg; intro y m; simp only [mem_sdiff, not_exists, not_and] at m; exact v0 _ m.1
 
 /-- `ENNReal.ofReal` commutes with `Finset.sum` for nonnegative maps -/
diff --git a/Misc/If.lean b/Misc/If.lean
index 9c4b7ee..dfb5dff 100644
--- a/Misc/If.lean
+++ b/Misc/If.lean
@@ -13,7 +13,7 @@ lemma ite_le_ite_iff (x y : Prop) {dx : Decidable x} {dy : Decidable y} :
 lemma ite_one_zero_congr (x y : Prop) {dx : Decidable x} {dy : Decidable y} :
     @ite _ x dx (1:ℝ) 0 = @ite _ y dy (1:ℝ) 0 ↔ (x ↔ y) := by
   by_cases h : x
-  repeat { by_cases l : y; repeat simp only [h, l, if_true, if_false, one_ne_zero, zero_ne_one] }
+  repeat { by_cases l : y; repeat simp [h, l] }
 
 lemma ite_one_zero_ne_zero (x : Prop) {dx : Decidable x} : @ite _ x dx (1:ℝ) 0 ≠ 0 ↔ x := by
   by_cases h : x; repeat { simp only [h, if_true, if_false]; norm_num }
@@ -21,8 +21,8 @@ lemma ite_one_zero_ne_zero (x : Prop) {dx : Decidable x} : @ite _ x dx (1:ℝ) 0
 lemma ite_and_one_zero (x y : Prop) {d : Decidable (x ∧ y)} :
     @ite _ (x ∧ y) d (1:ℝ) 0 =
       (@ite _ x (Classical.dec _) (1:ℝ) 0) * (@ite _ y (Classical.dec _) 1 0) := by
-  by_cases h : x
-  repeat { by_cases l : y; repeat simp only [h, l, if_true, if_false, one_mul, zero_mul] }
+  rw [ite_zero_mul_ite_zero, one_mul]
+  congr
 
 lemma ite_one_zero_nonneg {x : Prop} {d : Decidable x} : 0 ≤ @ite _ x d (1:ℝ) 0 := by
   split_ifs; repeat norm_num
diff --git a/Prob/Arith.lean b/Prob/Arith.lean
index ca0c863..ae0373b 100644
--- a/Prob/Arith.lean
+++ b/Prob/Arith.lean
@@ -37,6 +37,7 @@ instance : AddCommMonoid (Prob ℝ) where
   zero_add x := by simp only [add_eq, zero_eq, pure_bind, zero_add, bind_pure]
   add_zero x := by simp only [add_eq, zero_eq, pure_bind, add_zero, bind_pure]
   add_comm x y := by simp only [add_eq]; rw [bind_comm_of_eq]; ext x y; rw [add_comm]
+  nsmul := nsmulRec
 
 /-- • distributes over + -/
 instance : DistribMulAction ℝ (Prob ℝ) where
@@ -96,12 +97,14 @@ lemma le_exp_of_forall_le {f : Prob α} {u : α → ℝ} {b : ℝ} (h : ∀ x, f
 -- Mean is linear
 lemma mean_smul (s : ℝ) (f : Prob ℝ) : (s • f).mean = s * f.mean := by
   simp only [mean, smul_eq, exp_bind, exp_pure, id, exp_const_mul s f (λ x ↦ x)]
+  rfl
 lemma mean_add (f g : Prob ℝ) : (f + g).mean = f.mean + g.mean := by
   simp only [mean, add_eq, exp_bind, exp_pure, id, λ x ↦ exp_add g (λ _ ↦ x) (λ y ↦ y), exp_const, exp_add]
+  rfl
 
 /-- Mean is multiplicative -/
 lemma mean_mul (f g : Prob ℝ) : (f * g).mean = f.mean * g.mean := by
-  simp only [mean, mul_eq, exp_bind, exp_pure, id, ←exp_mul_const]; simp only [←exp_const_mul]
+  simp only [mean, mul_eq, exp_bind, exp_pure, id, ←exp_mul_const]; simp only [←exp_const_mul]; rfl
 
 -- f.pr is between 0 and 1
 lemma pr_nonneg {f : Prob α} {p : α → Prop} : 0 ≤ f.pr p := by
@@ -166,7 +169,7 @@ lemma pr_eq_zero {f : Prob α} {p : α → Prop} : f.pr p = 0 ↔ ∀ x, f.prob
   · intro h; contrapose h; simp only [not_forall] at h ⊢; apply ne_of_gt
     rcases h with ⟨x,px,h⟩; rw [not_not] at h; rw [←pr_false]; apply pr_lt_pr
     · simp only [ne_eq, IsEmpty.forall_iff, implies_true]
-    · simp only [true_and]; use x, px, h
+    · simp only [not_false_iff, true_and]; use x, px, h
   · intro h; rw [←pr_false]; apply pr_congr; simp only [iff_false]; exact h
 
 /-- `pr ≠ 0` if there is some nonzero prob -/
@@ -186,7 +189,7 @@ lemma pr_eq_one {f : Prob α} {p : α → Prop} : f.pr p = 1 ↔ ∀ x, f.prob x
 lemma pr_neg {f : Prob α} {p : α → Prop} : f.pr (λ x ↦ ¬p x) = 1 - f.pr p := by
   rw [eq_sub_iff_add_eq, ←pr_true]; simp only [pr, ←exp_add]; apply exp_congr;
   intro x _; simp only [if_true]; by_cases h : p x
-  repeat simp only [h, if_false, if_true, zero_add, add_zero]
+  repeat simp (config := {decide := true}) only [h, if_false, if_true, zero_add, add_zero]
 lemma pr_neg' {f : Prob α} {p : α → Prop} : f.pr p = 1 - f.pr (λ x ↦ ¬p x) := by
   simp only [pr_neg, sub_sub_cancel]
 
@@ -205,7 +208,7 @@ lemma pr_or_le {f : Prob α} (p q : α → Prop) : f.pr (λ x ↦ p x ∨ q x) 
 lemma pr_eq_add_of_cut {f : Prob α} {p : α → Prop} (q : α → Prop) :
     f.pr p = f.pr (fun x ↦ p x ∧ q x) + f.pr (fun x ↦ p x ∧ ¬q x) := by
   simp only [pr, ←exp_add]; apply exp_congr; intro x _; by_cases px : p x;
-  repeat { by_cases qx : q x; repeat simp only [px, qx, if_true, if_false, add_zero, zero_add] }
+  repeat { by_cases qx : q x; repeat simp (config := {decide := true}) only [px, qx, if_true, if_false, add_zero, zero_add] }
 
 /-- Markov's inequality -/
 lemma markov' (f : Prob α) (g : α → ℝ) (f0 : ∀ x, f.prob x ≠ 0 → 0 ≤ g x) {a : ℝ} (a0 : 0 < a) :
diff --git a/Prob/Basics.lean b/Prob/Basics.lean
index feafd70..fac74e5 100644
--- a/Prob/Basics.lean
+++ b/Prob/Basics.lean
@@ -154,7 +154,7 @@ lemma bool_prob_false_of_true {f : Prob Bool} : f.prob false = 1 - f.prob true :
   apply eq_sub_of_add_eq; rw [add_comm]; exact f.bool_total
 lemma bool_prob_true_of_false {f : Prob Bool} : f.prob true = 1 - f.prob false := eq_sub_of_add_eq f.bool_total
 lemma not_bool_prob {f : Prob Bool} {x : Bool} : (not <$> f).prob x = f.prob (not x) := by
-  rw [←Bool.not_not x, map_prob_of_inj, Bool.not_not]; rw [Bool.injective_iff]; simp only
+  rw [←Bool.not_not x, map_prob_of_inj, Bool.not_not]; rw [Bool.injective_iff]; decide
 
 /-- Bound a prob bind in terms of an intermediate event -/
 lemma le_prob_bind_of_cut {f : Prob α} {g : α → Prob β} (x : α) {y : β} :
diff --git a/Prob/Bernoulli.lean b/Prob/Bernoulli.lean
index e82c915..7b76155 100644
--- a/Prob/Bernoulli.lean
+++ b/Prob/Bernoulli.lean
@@ -1,4 +1,5 @@
 import Prob.Arith
+import Mathlib.Data.Finsupp.Notation
 
 /-!
 Bernoulli distributions
@@ -19,18 +20,18 @@ def bernoulli (p' : ℝ) : Prob Bool := by
     prob_nonneg := by
       intro x; induction x
       · simp only [ge_iff_le, min_le_iff, le_min_iff, zero_le_one, true_and, Finsupp.coe_update,
-          Function.update_same, sub_nonneg, max_le_iff, le_refl, true_or, and_self]
-      · simp only [ge_iff_le, min_le_iff, le_min_iff, zero_le_one, true_and, Finsupp.coe_update, ne_eq,
-          Function.update_noteq, Finsupp.single_eq_same, le_max_iff, le_refl, true_or]
+          Function.update_same, sub_nonneg, max_le_iff, le_refl, true_or, and_self, p]
+      · simp (config := {decide := true}) only [ge_iff_le, min_le_iff, le_min_iff, zero_le_one, true_and, Finsupp.coe_update, ne_eq,
+          Function.update_noteq, Finsupp.single_eq_same, le_max_iff, le_refl, true_or, p]
     total := by
-      simp only [Finsupp.sum_fintype, Fintype.sum_bool, ge_iff_le, min_le_iff, le_min_iff, zero_le_one,
+      simp (config := {decide := true}) only [Finsupp.sum_fintype, Fintype.sum_bool, ge_iff_le, min_le_iff, le_min_iff, zero_le_one,
         true_and, Finsupp.coe_update, ne_eq, Function.update_noteq, Finsupp.single_eq_same,
-        Function.update_same, add_sub_cancel'_right]
+        Function.update_same, add_sub_cancel]
   }
 
 -- If p is arbitrary, the probabilities are clamped
 lemma bernoulli_prob_true' (p : ℝ) : (bernoulli p).prob true = max 0 (min 1 p) := by
-  simp only [prob, bernoulli, ge_iff_le, min_le_iff, le_min_iff, zero_le_one, true_and, Finsupp.coe_update,
+  simp (config := {decide := true}) only [prob, bernoulli, ge_iff_le, min_le_iff, le_min_iff, zero_le_one, true_and, Finsupp.coe_update,
     ne_eq, Function.update_noteq, Finsupp.single_eq_same]
 lemma bernoulli_prob_false' (p : ℝ) : (bernoulli p).prob false = 1 - max 0 (min 1 p) := by
   simp only [bool_prob_false_of_true, bernoulli_prob_true']
diff --git a/Prob/Chernoff.lean b/Prob/Chernoff.lean
index 7060562..0d2af15 100644
--- a/Prob/Chernoff.lean
+++ b/Prob/Chernoff.lean
@@ -1,8 +1,9 @@
-import Mathlib.Analysis.Calculus.ContDiffDef
+import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 import Mathlib.Analysis.Calculus.TangentCone
 import Mathlib.Analysis.Calculus.Taylor
+import Mathlib.Analysis.Calculus.Deriv.Inv
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Data.Set.Intervals.Basic
 import Prob.Arith
@@ -17,15 +18,10 @@ We prove Hoeffding's inequality just for the Bernoulli case
 2. https://en.m.wikipedia.org/wiki/Hoeffding%27s_lemma
 -/
 
--- Work around https://github.com/leanprover/lean4/issues/2220
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- See issue lean4#2220
-
 open Prob
 open Real (log)
 open Set
 
-lemma Real.exp_nonneg {x : ℝ} : 0 ≤ exp x := le_of_lt (Real.exp_pos _)
-
 lemma exp_bernoulli_exp {p : ℝ} (m : p ∈ Icc 0 1) (t : ℝ) :
     (bernoulli p).exp (λ x ↦ (t * bif x then 1 else 0).exp) = 1 - p + p * t.exp := by
   simp only [exp_bernoulli _ m, cond_false, mul_zero, Real.exp_zero, mul_one, cond_true]
@@ -98,13 +94,13 @@ lemma hoeffdings_lemma {p : ℝ} (m : p ∈ Icc 0 1) {t : ℝ} (t0 : 0 ≤ t) :
   simp only [exp_bernoulli_exp m]
   have p1 : 0 ≤ 1-p := by linarith [m.2]
   by_cases tz : t = 0
-  · simp only [tz, Real.exp_zero, mul_one, sub_add_cancel, zero_mul, ne_eq, zero_div, add_zero, le_refl, zero_pow]
+  · simp (config := {decide := true}) only [tz, Real.exp_zero, mul_one, sub_add_cancel, zero_mul, ne_eq, zero_div, add_zero, le_refl, zero_pow]
   replace t0 := (Ne.symm tz).lt_of_le t0; clear tz
   rw [←Real.exp_log (L_pos m), Real.exp_le_exp]
   rcases L_taylor m t0 with ⟨a,_,h⟩
   simp only [L] at h; rw [h]; clear h; norm_num
   generalize hb : p * a.exp = b
-  have b0 : 0 ≤ b := by rw [←hb]; exact mul_nonneg m.1 Real.exp_nonneg
+  have b0 : 0 ≤ b := by rw [←hb]; exact mul_nonneg m.1 (Real.exp_nonneg _)
   have amgm : (1-p:) * b / (1 - p + b)^2 ≤ 1/4 := mul_div_sq_sum_le p1 b0
   simp only [mul_comm b _, ←mul_div _ _ (2 : ℝ)] at amgm ⊢
   apply le_trans (add_le_add_right (mul_le_mul_of_nonneg_right amgm _) _)
@@ -127,7 +123,7 @@ lemma exp_count (f : Prob Bool) (n : ℕ) (t : ℝ) :
     have i : ∀ x : Bool, ↑(bif x then (1 : ℕ) else (0 : ℕ)) = (bif x then (1 : ℝ) else (0 : ℝ)) := by
       intro x; induction x; repeat simp only [cond_false, cond_true, Nat.cast_one, Nat.cast_zero]
     simp only [count, Nat.cast_succ, add_mul, one_mul, Real.exp_add, exp_bind, exp_pure, Nat.cast_add,
-      exp_const_mul, exp_mul_const, h, hz, mul_comm _ z.exp, i, pow_succ, mul_ite, mul_add, mul_one,
+      exp_const_mul, exp_mul_const, h, hz, mul_comm _ z.exp, i, pow_succ', mul_ite, mul_add, mul_one,
       mul_zero]
 
 /-- Weak Chernoff's theorem for the Bernoulli case -/
@@ -148,7 +144,7 @@ lemma chernoff_count_le (f : Prob Bool) (n : ℕ) {t : ℝ} (t0 : 0 ≤ t) :
     generalize hz : f.exp (λ x ↦ (s * bif x then 1 else 0).exp) = z; simp only [hz] at le ⊢
     have z0 : 0 ≤ z := by rw [←hz]; apply exp_nonneg; intro x _; apply Real.exp_nonneg
     rw [div_le_iff (Real.exp_pos _), ←Real.exp_add]
-    apply le_trans (pow_le_pow_of_le_left z0 le n); clear le z0 hz z
+    apply le_trans (pow_le_pow_left z0 le n); clear le z0 hz z
     simp only [hp, ←Real.rpow_nat_cast, ←Real.exp_mul]
     simp only [Real.rpow_nat_cast, Real.exp_le_exp, mul_comm _ (n:ℝ), mul_add, mul_div, ←add_assoc, ←mul_assoc]
     simp only [add_comm _ (s*t), ←add_assoc]; simp only [neg_mul, add_right_neg, zero_add]
diff --git a/Prob/Cond.lean b/Prob/Cond.lean
index cf847d8..6c82206 100644
--- a/Prob/Cond.lean
+++ b/Prob/Cond.lean
@@ -25,7 +25,7 @@ lemma cond_eq_cexp : f.cond p q = f.cexp (λ x ↦ if p x then 1 else 0) q := by
 
 /-- cexp is monotonic -/
 lemma cexp_mono {u v : α → ℝ} (uv : ∀ x, f.prob x ≠ 0 → q x → u x ≤ v x) : f.cexp u q ≤ f.cexp v q := by
-  simp only [cexp]; refine' div_le_div_of_le_of_nonneg (exp_mono _) pr_nonneg
+  simp only [cexp]; refine' div_le_div_of_nonneg_right (exp_mono _) pr_nonneg
   intro x m; by_cases qx : q x
   repeat simp only [qx, if_true, if_false, uv x m, le_refl]
 
@@ -99,12 +99,12 @@ lemma cond_bind_le_of_forall_le {f : Prob α} {g : α → Prob β} {p q : β →
 lemma exp_eq_cexp_add_cexp (q : α → Prop) : f.exp u = f.cexp u q * f.pr q + f.cexp u (λ x ↦ ¬q x) * (1 - f.pr q) := by
   by_cases q0 : f.pr q = 0
   · simp only [cexp, q0, div_zero, sub_zero, mul_zero, zero_add, pr_neg, div_one, mul_one]
-    simp only [pr_eq_zero] at q0; apply exp_congr; intro x m; simp only [q0 x m, if_true, and_true]
+    simp only [pr_eq_zero] at q0; apply exp_congr; intro x m; simp (config := {decide := true}) only [q0 x m, if_true, and_true]
   by_cases q1 : f.pr q = 1
   · simp only [cexp, q1, div_one, mul_one, sub_self, mul_zero, add_zero]
     simp only [pr_eq_one] at q1; apply exp_congr; intro x m; simp only [q1 x m, if_true, and_true]
   replace q1 : 1 - f.pr q ≠ 0 := by rw [sub_ne_zero]; exact Ne.symm q1
-  simp only [cexp, pr_neg, div_mul_cancel _ q0, div_mul_cancel _ q1]
+  simp only [cexp, pr_neg, div_mul_cancel₀ _ q0, div_mul_cancel₀ _ q1]
   simp only [pr, ←exp_add]; apply exp_congr; intro x _
   by_cases qx : q x; repeat { simp only [qx, if_true, if_false]; norm_num }
 
@@ -165,11 +165,11 @@ lemma bayes' (f : Prob α) (a b : α → Prop) : f.cond a b * f.pr b = f.cond b
   · have ab0 : f.pr (λ x ↦ b x ∧ a x) = 0 := by
       apply le_antisymm _ pr_nonneg; rw [←b0]; apply pr_mono; intro x _; exact And.left
     simp only [b0, ab0, div_zero, mul_zero, zero_div, zero_mul]
-  simp only [div_mul_cancel _ a0, div_mul_cancel _ b0, and_comm]
+  simp only [div_mul_cancel₀ _ a0, div_mul_cancel₀ _ b0, and_comm]
 
 /-- Bayes' theorem, ratio version -/
 theorem bayes (f : Prob α) (a b : α → Prop) (b0 : f.pr b ≠ 0) : f.cond a b = f.cond b a * f.pr a / f.pr b := by
-  rw [←bayes', mul_div_cancel _ b0]
+  rw [←bayes', mul_div_cancel_right₀ _ b0]
 
 /-- Pure cexps are simple -/
 lemma cexp_pure {x : α} : (pure x : Prob α).cexp u q = if q x then u x else 0 := by
@@ -192,7 +192,7 @@ lemma cexp_sum {s : Finset β} {u : β → α → ℝ} :
   · simp only [Finset.sum_empty, cexp_zero]
   · simp only [Finset.sum_insert m, cexp_add, h]
 lemma cexp_const_mul {s : ℝ} : f.cexp (λ x ↦ s * u x) q = s * f.cexp u q := by
-  simp only [cexp, ite_mul_zero_right, exp_const_mul, mul_div]
+  simp only [cexp, ← mul_ite_zero, exp_const_mul, mul_div]
 
 /-- cond depends only on the conditional supp -/
 lemma cond_congr {p q r : α → Prop} (pq : ∀ x, f.prob x ≠ 0 → r x → (p x ↔ q x)) : f.cond p r = f.cond q r := by
@@ -221,9 +221,9 @@ lemma cexp_eq_cexp_add_cexp (r : α → Prop) :
     intro x m; simp only [q0 x m, false_and, not_false_eq_true]
   rw [cexp, exp_eq_cexp_add_cexp r, add_div, mul_div_right_comm, mul_div_right_comm]; apply congr_arg₂
   · simp only [cexp_if, mul_div_right_comm, mul_assoc, bayes' f q r]
-    rw [mul_comm _ (f.pr q), ←mul_assoc, div_mul_cancel _ q0]
+    rw [mul_comm _ (f.pr q), ←mul_assoc, div_mul_cancel₀ _ q0]
   · simp only [cexp_if, mul_div_right_comm, mul_assoc, ←pr_neg, bayes' f q (λ x ↦ ¬r x)]
-    rw [mul_comm _ (f.pr q), ←mul_assoc, ←cond_neg q0, div_mul_cancel _ q0]
+    rw [mul_comm _ (f.pr q), ←mul_assoc, ←cond_neg q0, div_mul_cancel₀ _ q0]
 
 /-- Weighted averages are ≤ max -/
 lemma average_le_max {p x y : ℝ} (m : p ∈ Icc 0 1) : x*p + y*(1-p) ≤ max x y := by
diff --git a/Prob/Defs.lean b/Prob/Defs.lean
index acf264e..15448c1 100644
--- a/Prob/Defs.lean
+++ b/Prob/Defs.lean
@@ -86,7 +86,7 @@ instance : Monad Prob where
   bind := λ f g ↦ by
     set prob := f.prob.sum (λ x p ↦ p • (g x).prob)
     have nonneg : ∀ x, 0 ≤ prob x := by
-      intro _; simp only [Finsupp.sum_apply]; apply Finset.sum_nonneg
+      intro _; simp only [Finsupp.sum_apply, prob]; apply Finset.sum_nonneg
       intro _ _; exact mul_nonneg f.prob_nonneg (g _).prob_nonneg
     have total : prob.sum (λ _ p ↦ p) = 1 := by
       rw [Finsupp.sum_sum_index]
diff --git a/Prob/Estimate.lean b/Prob/Estimate.lean
index 97fe0a5..013a322 100644
--- a/Prob/Estimate.lean
+++ b/Prob/Estimate.lean
@@ -27,7 +27,7 @@ def count (f : m Bool) : ℕ → m ℕ
 lemma count_le (f : Prob Bool) {n k : ℕ} : n < k → (count f n).prob k = 0 := by
   induction' n with n lo generalizing k
   · intro h; simp only [count, prob_pure, Nat.le_zero] at h ⊢
-    by_cases k0 : k = 0; simp only [k0] at h; simp only [k0, ite_false]
+    by_cases k0 : k = 0; simp (config := {decide := true}) only [k0] at h; simp only [k0, ite_false]
   · intro h; simp only [count, prob_bind, prob_pure] at h ⊢
     apply Finset.sum_eq_zero; intro x _; rw [mul_eq_zero]; right
     apply Finset.sum_eq_zero; intro l m; induction x
@@ -38,7 +38,7 @@ lemma count_le (f : Prob Bool) {n k : ℕ} : n < k → (count f n).prob k = 0 :=
       contrapose m; simp only [not_not]; apply lo
       by_cases kl : k = 1 + l
       · rw [kl, add_comm 1 _, Nat.succ_lt_succ_iff] at h; exact h
-      · simp only [kl, if_false] at m
+      · simp (config := {decide := true}) only [kl, if_false] at m
 lemma count_le' (f : Prob Bool) {n k : ℕ} : (count f n).prob k ≠ 0 → k ≤ n := by
   intro h; contrapose h; simp only [not_le, not_not] at h ⊢; exact count_le _ h
 
@@ -68,4 +68,4 @@ lemma count_not (f : Prob Bool) (n : ℕ) : (count (not <$> f) n) = (λ x ↦ n
 /-- estimate.mean = f.prob true -/
 lemma mean_estimate (f : Prob Bool) {n : ℕ} (n0 : n ≠ 0) : (estimate f n).mean = f.prob true := by
   simp only [mean, estimate, exp_map, id, exp_div, mean_count, Function.comp]
-  rw [mul_div_cancel_left]; rw [Nat.cast_ne_zero]; exact n0
+  rw [mul_div_cancel_left₀]; rw [Nat.cast_ne_zero]; exact n0
diff --git a/Prob/Pmf.lean b/Prob/Pmf.lean
index c22730b..d721de3 100644
--- a/Prob/Pmf.lean
+++ b/Prob/Pmf.lean
@@ -91,7 +91,7 @@ theorem Prob.toProb_toPmf (f : Prob α) : f.toPmf.toProb f.toPmf_support_finite
 /-- `PMF → Prob → PMF` is the identity on finitely-supported `PMF`s. -/
 theorem PMF.toPmf_toProb (f : PMF α) (hf : f.support.Finite) : (f.toProb hf).toPmf = f := by
   ext
-  simp only [Prob.toPmf_coe, prob_toProb, ne_eq, ENNReal.ofReal_toReal_eq_iff, apply_ne_top]
+  simp (config := {decide := true}) only [Prob.toPmf_coe, prob_toProb, ne_eq, ENNReal.ofReal_toReal_eq_iff, apply_ne_top, not_false]
 
 /-- This enables the use of the `lift p to Prob α` tactic when `p : PMF α`, which creates a
 new goal of `p.support.Finite`. -/
diff --git a/lake-manifest.json b/lake-manifest.json
index 9439007..8d863b0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,52 +1,68 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib4",
-    "subDir?": null,
-    "rev": "3ce43c18f614b76e161f911b75a3e1ef641620ff",
-    "opts": {},
-    "name": "mathlib",
-    "inputRev?": null,
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "727fa6aa1113c376ea1873812d1ab5c17a24f1d2",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/quote4",
-    "subDir?": null,
-    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
-    "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/aesop",
-    "subDir?": null,
-    "rev": "b601328752091a1cfcaebdd6b6b7c30dc5ffd946",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/lean4-cli",
-    "subDir?": null,
-    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
-    "opts": {},
-    "name": "Cli",
-    "inputRev?": "nightly",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/ProofWidgets4",
-    "subDir?": null,
-    "rev": "27715d1daf32b9657dc38cd52172d77b19bde4ba",
-    "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.18",
-    "inherited": true}}],
- "name": "debate"}
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.30",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "rev": "a45ae63747140c1b2cbad9d46f518015c047047a",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "debate",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 176590e..15a09a6 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,7 +13,7 @@ def moreLeanArgs := moreServerArgs
 
 package debate
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
 
 @[default_target]
 lean_lib Debate where
diff --git a/lean-toolchain b/lean-toolchain
index 183a307..9ad3040 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc4
+leanprover/lean4:v4.7.0