From 2b65ea94c94a49c7bc0551dcb469115fe36049d3 Mon Sep 17 00:00:00 2001
From: Mauricio Collares <mauricio@collares.org>
Date: Sat, 21 Oct 2023 16:26:00 +0200
Subject: [PATCH 1/2] chore: fixes for new simp default (decide := false) in
 lean4#2722

---
 Std/Data/Array/Init/Lemmas.lean |  2 +-
 Std/Data/Char.lean              |  6 +++---
 Std/Data/Fin/Lemmas.lean        |  2 +-
 Std/Data/Int/DivMod.lean        | 10 +++++-----
 Std/Data/List/Count.lean        |  4 ++--
 Std/Data/List/Lemmas.lean       |  6 +++---
 Std/Data/Nat/Lemmas.lean        |  6 ++++--
 Std/Data/Rat/Lemmas.lean        |  6 +++---
 Std/Logic.lean                  |  2 +-
 9 files changed, 23 insertions(+), 21 deletions(-)

diff --git a/Std/Data/Array/Init/Lemmas.lean b/Std/Data/Array/Init/Lemmas.lean
index b7c12cd3f7..52a379deda 100644
--- a/Std/Data/Array/Init/Lemmas.lean
+++ b/Std/Data/Array/Init/Lemmas.lean
@@ -130,7 +130,7 @@ theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
 
 @[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
   simp only [push, getElem_eq_data_get, List.concat_eq_append]
-  rw [List.get_append_right] <;> simp [getElem_eq_data_get]
+  rw [List.get_append_right] <;> simp [getElem_eq_data_get, Nat.zero_lt_one]
 
 theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
     (a.push x)[i] = if h : i < a.size then a[i] else x := by
diff --git a/Std/Data/Char.lean b/Std/Data/Char.lean
index 939a5c1983..3c7a790840 100644
--- a/Std/Data/Char.lean
+++ b/Std/Data/Char.lean
@@ -12,12 +12,12 @@ private theorem csize_eq (c) :
     csize c = 1 ∨ csize c = 2 ∨ csize c = 3 ∨
     csize c = 4 := by
   simp only [csize, Char.utf8Size]
-  repeat (first | split | (solve | simp))
+  repeat (first | split | (solve | simp (config := {decide := true})))
 
 theorem csize_pos (c) : 0 < csize c := by
-  rcases csize_eq c with _|_|_|_ <;> simp_all
+  rcases csize_eq c with _|_|_|_ <;> simp_all (config := {decide := true})
 
 theorem csize_le_4 (c) : csize c ≤ 4 := by
-  rcases csize_eq c with _|_|_|_ <;> simp_all
+  rcases csize_eq c with _|_|_|_ <;> simp_all (config := {decide := true})
 
 end String
diff --git a/Std/Data/Fin/Lemmas.lean b/Std/Data/Fin/Lemmas.lean
index 89e9036c11..0f64be4266 100644
--- a/Std/Data/Fin/Lemmas.lean
+++ b/Std/Data/Fin/Lemmas.lean
@@ -645,7 +645,7 @@ theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
   exists_fin_succ.trans <| or_congr_right exists_fin_one
 
 theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by
-  simp [forall_fin_two]
+  simp only [forall_fin_two]; decide
 
 /--
 Define `motive i` by reverse induction on `i : Fin (n + 1)` via induction on the underlying `Nat`
diff --git a/Std/Data/Int/DivMod.lean b/Std/Data/Int/DivMod.lean
index 7f5640155a..ba7bfbb8ab 100644
--- a/Std/Data/Int/DivMod.lean
+++ b/Std/Data/Int/DivMod.lean
@@ -30,11 +30,11 @@ theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(div m b +
 
 @[simp] protected theorem zero_div : ∀ b : Int, div 0 b = 0
   | ofNat _ => show ofNat _ = _ by simp
-  | -[_+1] => show -ofNat _ = _ by simp
+  | -[_+1] => show -ofNat _ = _ by simp; rfl
 
 @[local simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
   | ofNat _ => show ofNat _ = _ by simp
-  | -[_+1] => show -ofNat _ = _ by simp
+  | -[_+1] => show -ofNat _ = _ by simp; rfl
 
 @[simp] theorem zero_fdiv (b : Int) : fdiv 0 b = 0 := by cases b <;> rfl
 
@@ -174,7 +174,7 @@ theorem add_mul_ediv_left (a : Int) {b : Int}
   Int.mul_comm .. ▸ Int.add_mul_ediv_right _ _ H
 
 theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
-  if h : c = 0 then by simp [h] else by
+  if h : c = 0 then by simp [h]; rfl else by
     let ⟨k, hk⟩ := H
     rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
       ← Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]
@@ -729,7 +729,7 @@ protected theorem mul_ediv_assoc' (b : Int) {a c : Int}
   rw [Int.mul_comm, Int.mul_ediv_assoc _ h, Int.mul_comm]
 
 theorem div_dvd_div : ∀ {a b c : Int}, a ∣ b → b ∣ c → b.div a ∣ c.div a
-  | a, _, _, ⟨b, rfl⟩, ⟨c, rfl⟩ => if az : a = 0 then by simp [az] else by
+  | a, _, _, ⟨b, rfl⟩, ⟨c, rfl⟩ => if az : a = 0 then by simp_arith [az] else by
     rw [Int.mul_div_cancel_left _ az, Int.mul_assoc, Int.mul_div_cancel_left _ az]
     apply Int.dvd_mul_right
 
@@ -800,7 +800,7 @@ theorem fdiv_eq_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → a.fdiv b = a / b
     rw [mul_fdiv_cancel_left _ bz, mul_ediv_cancel_left _ bz]
 
 theorem neg_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → (-a) / b = -(a / b)
-  | _, b, ⟨c, rfl⟩ => by if bz : b = 0 then simp [bz] else
+  | _, b, ⟨c, rfl⟩ => by if bz : b = 0 then simp [bz]; rfl else
     rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]
 
 theorem sub_ediv_of_dvd (a : Int) {b c : Int}
diff --git a/Std/Data/List/Count.lean b/Std/Data/List/Count.lean
index a05b86d5b5..9f35d96f62 100644
--- a/Std/Data/List/Count.lean
+++ b/Std/Data/List/Count.lean
@@ -51,11 +51,11 @@ theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a
     if h : p x then
       rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]
       · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
-      · simp only [h]
+      · simp only [h, not_true_eq_false, decide_False, not_false_eq_true]
     else
       rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]
       · rfl
-      · simp only [h]
+      · simp only [h, not_false_eq_true, decide_True]
 
 theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by
   induction l with
diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index c6c54c750b..18153b8e7d 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -1963,8 +1963,8 @@ theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l := drop
 theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n)
   | [], _, _ => by simp
   | x :: xs, hl, h => by
-    cases m <;> cases n <;> simp only [disjoint_cons_left, mem_cons, disjoint_cons_right,
-      drop, true_or, eq_self_iff_true, not_true, false_and, not_mem_nil, disjoint_nil_left, take]
+    cases m <;> cases n <;> simp only [disjoint_cons_left, drop, not_mem_nil, disjoint_nil_left,
+      take, not_false_eq_true, and_self]
     · case succ.zero => cases h
     · cases hl with | cons h₀ h₁ =>
       refine ⟨fun h => h₀ _ (mem_of_mem_drop h) rfl, ?_⟩
@@ -2117,7 +2117,7 @@ theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by
   simp only [range_eq_range', range'_sublist_right]
 
 theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n := by
-  simp only [range_eq_range', range'_subset_right]
+  simp only [range_eq_range', range'_subset_right, lt_succ_self]
 
 @[simp]
 theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n := by
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index a1a0ac1617..d5bcb7a0dc 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -700,7 +700,7 @@ theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
   | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
 
 theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
-  match n % 2, @Nat.mod_lt n 2 (by simp) with
+  match n % 2, @Nat.mod_lt n 2 (by decide) with
   | 0, _ => .inl rfl
   | 1, _ => .inr rfl
 
@@ -845,7 +845,9 @@ theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
   | k+1 =>
     rw [log2]; split
     · have n0 : 0 < n / 2 := (Nat.le_div_iff_mul_le (by decide)).2 ‹_›
-      simp [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0), le_div_iff_mul_le, Nat.pow_succ]
+      simp only [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0), le_div_iff_mul_le,
+        Nat.pow_succ]
+      exact Nat.le_div_iff_mul_le (by decide)
     · simp only [le_zero_eq, succ_ne_zero, false_iff]
       refine mt (Nat.le_trans ?_) ‹_›
       exact Nat.pow_le_pow_of_le_right (Nat.succ_pos 1) (Nat.le_add_left 1 k)
diff --git a/Std/Data/Rat/Lemmas.lean b/Std/Data/Rat/Lemmas.lean
index 15c620f09b..aa76a05872 100644
--- a/Std/Data/Rat/Lemmas.lean
+++ b/Std/Data/Rat/Lemmas.lean
@@ -126,7 +126,7 @@ theorem mk_eq_divInt (num den nz c) : ⟨num, den, nz, c⟩ = num /. (den : Nat)
 
 theorem divInt_self (a : Rat) : a.num /. a.den = a := by rw [divInt_ofNat, mkRat_self]
 
-@[simp] theorem zero_divInt (n) : 0 /. n = 0 := by cases n <;> simp [divInt]
+@[simp] theorem zero_divInt (n) : 0 /. n = 0 := by cases n <;> simp [divInt]; rfl
 
 @[simp] theorem divInt_zero (n) : n /. 0 = 0 := mkRat_zero n
 
@@ -215,7 +215,7 @@ theorem neg_normalize (n d z) : -normalize n d z = normalize (-n) d z := by
   simp [normalize, maybeNormalize_eq]; ext <;> simp [Int.neg_div]
 
 theorem neg_mkRat (n d) : -mkRat n d = mkRat (-n) d := by
-  if z : d = 0 then simp [z] else simp [← normalize_eq_mkRat z, neg_normalize]
+  if z : d = 0 then simp [z]; rfl else simp [← normalize_eq_mkRat z, neg_normalize]
 
 theorem neg_divInt (n d) : -(n /. d) = -n /. d := by
   rcases Int.eq_nat_or_neg d with ⟨_, rfl | rfl⟩ <;> simp [divInt_neg', neg_mkRat]
@@ -300,7 +300,7 @@ theorem inv_def (a : Rat) : a.inv = a.den /. a.num := by
 
 @[simp] protected theorem inv_zero : (0 : Rat).inv = 0 := by
   unfold Rat.inv
-  simp
+  rfl
 
 @[simp] theorem inv_divInt (n d : Int) : (n /. d).inv = d /. n := by
   if z : d = 0 then simp [z] else
diff --git a/Std/Logic.lean b/Std/Logic.lean
index db0c1c9796..98b6eaae94 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -77,7 +77,7 @@ theorem not_iff_false_intro (h : a) : ¬a ↔ False := iff_false_intro (not_not_
 theorem iff_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ↔ b) ↔ (c ↔ d) :=
   ⟨fun h => h₁.symm.trans <| h.trans h₂, fun h => h₁.trans <| h.trans h₂.symm⟩
 
-@[simp] theorem not_true : (¬True) ↔ False := iff_false_intro (not_not_intro ⟨⟩)
+theorem not_true : (¬True) ↔ False := iff_false_intro (not_not_intro ⟨⟩)
 
 theorem not_false_iff : (¬False) ↔ True := iff_true_intro not_false
 

From 6f724a0557dc82150f2d12bdaf72dea91b3bdac8 Mon Sep 17 00:00:00 2001
From: Mauricio Collares <mauricio@collares.org>
Date: Tue, 31 Oct 2023 07:57:27 +0100
Subject: [PATCH 2/2] use leanprover/lean4-pr-releases:pr-release-2722
 toolchain

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index e8560170ab..0167242997 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4-pr-releases:pr-release-2722