Update to leanprover/lean4:v4.26.0-rc1, fixing compilation

girving · girving · commit dcfea10d0336 · 2025-11-19T22:51:42.000Z
All the tests pass again!
diff --git a/Interval/EulerMaclaurin/Bernoulli.lean b/Interval/EulerMaclaurin/Bernoulli.lean
@@ -434,7 +434,6 @@ lemma pres_eq_reflect {s : ℕ} {x y b : ℝ} :
     replace q := (q x).mp e
     have ne : x ≠ (1 + s) / 2 := by
       contrapose xh
-      simp only [ne_eq, not_not] at xh
       simp only [xh, Real.sqrt_inv, not_lt, s]
       simp only [Real.sqrt_inv, s] at xh
       rw [le_div_iff₀]
diff --git a/Interval/EulerMaclaurin/LHopital.lean b/Interval/EulerMaclaurin/LHopital.lean
@@ -59,7 +59,6 @@ theorem lhopital_field {f g : 𝕜 → 𝕜} {a f' g' : 𝕜} (df : HasDerivAt f
       _ = 2⁻¹ * ‖g'‖ * ‖y‖ := by ring
   have dg0 : g x ≠ 0 := by
     contrapose lo
-    simp only [ne_eq, not_not] at lo
     simp only [lo, norm_zero, ge_iff_le, not_le]
     bound
   calc ‖f x / g x - f' / g'‖
diff --git a/Interval/Fixed.lean b/Interval/Fixed.lean
@@ -104,8 +104,7 @@ lemma Fixed.neg_def (x : Fixed s) : -x = x.neg := rfl
 /-- The contrapose of `-nan = nan` -/
 @[simp] lemma Fixed.ne_nan_of_neg {x : Fixed s} (h : -x ≠ nan) : x ≠ nan := by
   contrapose h
-  simp only [ne_eq, not_not] at h
-  simp only [h, neg_nan, ne_eq, not_true_eq_false, not_false_eq_true]
+  simp only [h, neg_nan]
 
 /-- `Fixed` addition saturates to `nan` -/
 @[irreducible] def Fixed.add (x y : Fixed s) :=
@@ -201,15 +200,15 @@ lemma Fixed.add_comm (x y : Fixed s) : x + y = y + x := by
 lemma Fixed.ne_nan_of_add {x y : Fixed s} (h : x + y ≠ nan) : x ≠ nan ∧ y ≠ nan := by
   contrapose h; simp only [not_and_or, not_not] at h
   cases' h with h h
-  · simp only [h, nan_add, ne_eq, not_true, not_false_eq_true]
-  · simp only [h, add_nan, ne_eq, not_true, not_false_eq_true]
+  · simp only [h, nan_add]
+  · simp only [h, add_nan]
 
 /-- If `x - y ≠ nan`, neither `x` or `y` are `nan` -/
 lemma Fixed.ne_nan_of_sub {x y : Fixed s} (h : x - y ≠ nan) : x ≠ nan ∧ y ≠ nan := by
   contrapose h; simp only [not_and_or, not_not] at h
   cases' h with h h
-  · simp only [h, nan_sub, ne_eq, not_true, not_false_eq_true]
-  · simp only [h, sub_nan, ne_eq, not_true, not_false_eq_true]
+  · simp only [h, nan_sub]
+  · simp only [h, sub_nan]
 
 /-- `Fixed.val` commutes with negation, except at `nan` -/
 lemma Fixed.val_neg {x : Fixed s} (xn : x ≠ nan) : (-x).val = -x.val := by
@@ -346,7 +345,6 @@ lemma Fixed.neg_add {x y : Fixed s} : -(x + y) = -y + -x := by
     · simp only [not_lt, xym, Int64.isNeg_min, iff_true, Int64.neg_min, ite_self]
     · have xy0 : x.n + y.n ≠ 0 := by
         contrapose xyn
-        simp only [not_not] at xyn
         simp only [eq_neg_iff_add_eq_zero.mpr xyn, Int64.isNeg_neg y0 yn, ← not_le, iff_not_self,
           not_false_eq_true]
       simp only [Int64.isNeg_neg xy0 xym, ite_not, ← not_iff]
@@ -559,7 +557,7 @@ lemma Fixed.val_nan : (nan : Fixed s).val = -(2:ℝ) ^ (s + 63 : ℤ) := by
 
 /-- Positive `Fixed`s are `≠ nan` -/
 lemma Fixed.ne_nan_of_pos {x : Fixed s} (h : 0 < x.val) : x ≠ nan := by
-  contrapose h; rw [not_not] at h; simp only [not_lt, h, val_nan_neg.le]
+  contrapose h; simp only [not_lt, h, val_nan_neg.le]
 
 /-!
 ### `Fixed` multiplication, rounding up or down
@@ -1109,8 +1107,7 @@ lemma Fixed.approx_two_pow (n : Fixed 0) (up : Bool) :
 @[simp] lemma Fixed.ne_nan_of_two_pow {n : Fixed 0} {up : Bool}
     (h : (two_pow n up : Fixed s) ≠ nan) : n ≠ nan := by
   contrapose h
-  simp only [ne_eq, not_not] at h
-  simp only [h, two_pow_nan, ne_eq, not_true_eq_false, not_false_eq_true]
+  simp only [h, two_pow_nan]
 
 /-- `Fixed.approx_two_pow`, down version -/
 lemma Fixed.two_pow_le {n : Fixed 0} (h : (.two_pow n false : Fixed s) ≠ nan) :
diff --git a/Interval/Floating/Add.lean b/Interval/Floating/Add.lean
@@ -246,7 +246,7 @@ lemma add_n_norm (r : UInt128) (s : UInt64) (up : Bool) :
   rw [Nat.le_div_iff_mul_le (by positivity), ←pow_add]
   refine adjust_le_mul ?_ (UInt64.ne_zero_iff_toNat_ne_zero.mp s0)
   contrapose r0
-  simp only [ne_eq, not_not, ←UInt128.eq_zero_iff] at r0 ⊢
+  simp only [← UInt128.eq_zero_iff] at r0 ⊢
   rw [add_n]
   simp only [r0, UInt128.log2_zero, UInt128.zero_lo, UInt64.zero_shiftLeft,
     UInt128.zero_shiftRightRound, ite_self]
@@ -264,7 +264,9 @@ lemma valid_small_shift1 {n s : UInt64} (n63 : n ≠ 2^63) (n0 : n ≠ 0)
     (n_le : n.toNat ≤ 2^63)
     : Valid n.toInt64 s where
   zero_same := by
-    intro z; clear n63; contrapose n0; rw [Int64.ext_iff] at z; exact not_not.mpr z
+    intro z
+    contrapose n0
+    simpa only [Int64.ext_iff, UInt64.toUInt64_toInt64, Int64.n_zero] using z
   nan_same := by
     intro m
     rw [Int64.ext_iff, UInt64.toUInt64_toInt64, Int64.n_min] at m
diff --git a/Interval/Floating/Basic.lean b/Interval/Floating/Basic.lean
@@ -191,19 +191,18 @@ lemma val_nan : (nan : Floating).val = -(2 ^ 63) * 2 ^ (2 ^ 63 - 1) := by
 /-- If we're not nan, `x.n ≠ .min` -/
 lemma n_ne_min {x : Floating} (n : x ≠ nan) : x.n ≠ .minValue := by
   contrapose n
-  simp only [ne_eq, not_not, ext_iff, n_nan, s_nan, not_and, not_forall, exists_prop] at n ⊢
+  simp only [ext_iff, n_nan, s_nan] at n ⊢
   exact ⟨n, x.nan_same n⟩
 
 /-- If we're not zero, `x.n ≠ 0` -/
 lemma n_ne_zero {x : Floating} (n : x ≠ 0) : x.n ≠ 0 := by
   contrapose n
-  simp only [ne_eq, not_not, ext_iff, not_and, not_forall, exists_prop] at n ⊢
+  simp only [ext_iff] at n ⊢
   exact ⟨n, x.zero_same n⟩
 
 /-- If `x.s ≠ 0`, `x.n ≠ 0` -/
 lemma n_ne_zero' {x : Floating} (n : x.s ≠ 0) : x.n ≠ 0 := by
   contrapose n
-  simp only [ne_eq, not_not] at n ⊢
   simp only [x.zero_same n]
 
 /-- `x.n = 0` exactly at 0 -/
@@ -271,8 +270,8 @@ lemma val_of_nonneg {x : Floating} (x0 : 0 ≤ x.val) :
     x.val = (x.n.toUInt64.toNat : ℝ) * 2^((x.s.toNat : ℤ) - 2^63) := by
   rw [val, UInt64.toInt, Int64.coe_of_nonneg, Int.cast_natCast]
   rw [val] at x0
-  simpa only [Int64.isNeg_eq_le, decide_eq_false_iff_not, not_le, gt_iff_lt, two_zpow_pos,
-    mul_nonneg_iff_of_pos_right, Int.cast_nonneg, Int64.coe_nonneg_iff] using x0
+  simpa only [Int.reducePow, two_zpow_pos, mul_nonneg_iff_of_pos_right, Int.cast_nonneg_iff,
+    Int64.coe_nonneg_iff] using x0
 
 /-!
 ### The smallest normalized value
diff --git a/Interval/Floating/Floor.lean b/Interval/Floating/Floor.lean
@@ -43,7 +43,7 @@ namespace Floating
   rw [floor]; simp only [beq_self_eq_true, s_nan, Bool.true_or, n_nan, cond_true]
 
 @[simp] lemma ne_nan_of_floor {x : Floating} (n : x.floor ≠ nan) : x ≠ nan := by
-  contrapose n; simp only [not_not] at n; simp [n]
+  contrapose n; simp [n]
 
 lemma floor_mono {x y : Floating} (le : x ≤ y) (yn : y.floor ≠ nan) : x.floor ≤ y.floor := by
   by_cases xn : x.floor = nan
diff --git a/Interval/Floating/Mul.lean b/Interval/Floating/Mul.lean
@@ -129,7 +129,6 @@ lemma mul_norm_correct (n : UInt128) (up : Bool) (n0 : n ≠ 0) (lo : n.toNat 
         rw [Nat.one_le_iff_ne_zero]
         contrapose r_eq
         apply ne_of_lt
-        simp only [ne_eq, not_not] at r_eq
         simp only [r_eq, pow_zero, mul_one, ← UInt128.eq_iff_toNat_eq] at hz
         simp only [UInt64.lt_iff_toNat_lt, ←hz, ←hr, UInt64.toNat_2_pow_63]
         simp only [UInt128.toNat_def, mul_n_max] at lo
diff --git a/Interval/Floating/Order.lean b/Interval/Floating/Order.lean
@@ -191,7 +191,6 @@ lemma isNeg_iff' {x : Floating} : x.n < 0 ↔ x < 0 := by
   · simp only [x0, s_zero, ne_eq, not_true_eq_false] at s0
   have xm : x.n ≠ .minValue := by
     contrapose xn
-    simp only [ne_eq, not_not] at xn
     simp only [xn]
     decide
   have e : (2^62 : ℝ) = (2^62 : ℤ) := by norm_num
@@ -227,7 +226,7 @@ lemma isNeg_iff' {x : Floating} : x.n < 0 ↔ x < 0 := by
     UInt64.lt_iff_toNat_lt, UInt64.toNat_max, UInt64.toNat_2_pow_63, true_and, false_or]
     simp only [Int64.isNeg_eq_le] at xn
     contrapose n
-    simp only [not_or, not_lt, tsub_le_iff_right, not_and, not_not] at n ⊢
+    simp only [not_or, not_lt, tsub_le_iff_right, not_and] at n ⊢
     have se : x.s = .max := by
       simp only [UInt64.eq_iff_toNat_eq, UInt64.toNat_max]
       have h := x.s.toNat_le_pow_sub_one
@@ -283,7 +282,7 @@ lemma isNeg_iff' {x : Floating} : x.n < 0 ↔ x < 0 := by
   rw [val]; symm
   by_cases xn : x.n < 0
   · simp only [xn, ← not_le, mul_nonneg_iff_of_pos_right (two_zpow_pos (𝕜 := ℝ)), iff_true]
-    simpa only [Int.cast_nonneg, not_le, Int64.coe_lt_zero_iff]
+    simpa only [Int.cast_nonneg_iff, Int64.coe_nonneg_iff, not_le]
   · simp only [xn, not_lt, two_zpow_pos, mul_nonneg_iff_of_pos_right, Int.cast_nonneg,
       Int64.coe_nonneg_iff, iff_false, not_lt.mp xn]
 
@@ -412,11 +411,11 @@ instance : LinearOrder Floating where
   simpa only [val_le_val, val_zero, not_lt] using nan_lt_zero.le
 
 lemma ne_nan_of_nonneg {x : Floating} (n : 0 ≤ x.val) : x ≠ nan := by
-  contrapose n; simp only [ne_eq, not_not] at n; simp only [n, not_nan_nonneg, not_false_eq_true]
+  contrapose n; simp only [n, not_nan_nonneg, not_false_eq_true]
 
 lemma ne_nan_of_le {x y : Floating} (n : x ≠ nan) (le : x.val ≤ y.val) : y ≠ nan := by
   contrapose n
-  simp only [ne_eq, not_not, ←val_inj] at n ⊢
+  simp only [← val_inj] at n ⊢
   simp only [n] at le
   exact le_antisymm le (val_nan_le _)
 
diff --git a/Interval/Floating/Scale.lean b/Interval/Floating/Scale.lean
@@ -74,8 +74,8 @@ lemma val_scaleB {x : Floating} {t : Int64} (n : x.scaleB t ≠ nan) :
 
 /-- `scaleB` propagates `nan` -/
 @[simp] lemma ne_nan_of_scaleB {x : Floating} {t : Int64} (n : x.scaleB t ≠ nan) : x ≠ nan := by
-  contrapose n; simp only [ne_eq, not_not] at n
-  simp only [n, nan_scaleB, ne_eq, not_true_eq_false, not_false_eq_true]
+  contrapose n
+  simp only [n, nan_scaleB]
 
 /-!
 ### Dividing by two
diff --git a/Interval/Int64.lean b/Interval/Int64.lean
@@ -363,7 +363,7 @@ lemma Int64.toInt_ofInt' {n : ℤ} (h : |n| < 2^63) : ((n : Int64) : ℤ) = n :=
     · simp [n0]
     have d : ¬((2 * a : ℕ) : ℤ) ∣ n := by
       contrapose h
-      simp only [Decidable.not_not, not_lt, Int.natCast_dvd, Int.natAbs_natCast] at h ⊢
+      simp only [not_lt, Int.natCast_dvd, Int.natAbs_natCast] at h ⊢
       linarith [Nat.le_of_dvd (Nat.pos_iff_ne_zero.mpr n0) h]
     have lt : n < 2 * a := by omega
     simp only [Int.neg_emod, d, ite_false, Int.ofNat_mod_ofNat]
@@ -927,7 +927,6 @@ lemma Int64.abs_shiftRightRound_le (x : Int64) (s : UInt64) (up : Bool) :
 lemma Int64.shiftRightRound_ne_min {x : Int64} (n : x ≠ minValue) (s : UInt64) (up : Bool) :
     x.shiftRightRound s up ≠ minValue := by
   contrapose n
-  simp only [ne_eq, Decidable.not_not] at n ⊢
   have h := abs_shiftRightRound_le x s up
   simp only [n, coe_min', _root_.abs_neg, abs_pow, abs_two, le_abs] at h
   rcases h with h | h
diff --git a/Interval/Interval/Basic.lean b/Interval/Interval/Basic.lean
@@ -152,16 +152,12 @@ instance : ApproxOne Interval ℝ where approx_one := by simp only [approx_one]
 /-- If we're not `nan`, our components are not `nan` -/
 @[simp] lemma lo_ne_nan {x : Interval} (n : x ≠ nan) : x.lo ≠ nan := by
   contrapose n
-  simp only [ne_eq, not_not] at n
-  simp only [ne_eq, ext_iff, n, lo_nan, x.norm.mp n, hi_nan, and_self, not_true_eq_false,
-    not_false_eq_true]
+  simp only [ext_iff, n, lo_nan, x.norm.mp n, hi_nan, and_self]
 
 /-- If we're not `nan`, our components are not `nan` -/
 @[simp] lemma hi_ne_nan {x : Interval} (n : x ≠ nan) : x.hi ≠ nan := by
   contrapose n
-  simp only [ne_eq, not_not] at n
-  simp only [ne_eq, ext_iff, n, lo_nan, x.norm.mpr n, hi_nan, and_self, not_true_eq_false,
-    not_false_eq_true]
+  simp only [ext_iff, n, lo_nan, x.norm.mpr n, hi_nan, and_self]
 
 -- We're not nan if lo or hi aren't nan -/
 lemma ne_nan_of_lo {x : Interval} (n : x.lo ≠ nan) : x ≠ nan := ne_of_apply_ne lo n
@@ -541,10 +537,10 @@ lemma sub_def : x - y = mix (x.lo.sub y.hi false) (x.hi.sub y.lo true) (by
   simp only [HSub.hSub, Sub.sub, lo_nan, Floating.nan_sub, hi_nan, mix_nan]
 lemma ne_nan_of_add {x y : Interval} (n : x + y ≠ nan) : x ≠ nan ∧ y ≠ nan := by
   contrapose n; simp only [ne_eq, not_and_or, not_not] at n
-  rcases n with n | n; repeat simp only [n, nan_add, add_nan, not_not]
+  rcases n with n | n; repeat simp only [n, nan_add, add_nan]
 lemma ne_nan_of_sub {x y : Interval} (n : x - y ≠ nan) : x ≠ nan ∧ y ≠ nan := by
   contrapose n; simp only [ne_eq, not_and_or, not_not] at n
-  rcases n with n | n; repeat simp only [n, nan_sub, sub_nan, not_not]
+  rcases n with n | n; repeat simp only [n, nan_sub, sub_nan]
 
 /-- `add` respects `approx` -/
 instance : ApproxAdd Interval ℝ where
@@ -797,8 +793,8 @@ lemma abs_pos_of_not_zero_mem {x : Interval} (z : ¬approx x (0 : ℝ)) : 0 < x.
   by_cases n : x = nan
   · simp only [n, approx_nan, not_true_eq_false] at z
   apply abs_pos n
-  · contrapose z; simp only [ne_eq, not_not, ←Floating.val_eq_zero] at z
-    simp only [← z, not_not, lo_mem]
+  · contrapose z; simp only [← Floating.val_eq_zero] at z
+    simp only [← z, lo_mem]
   · simp only [approx, lo_eq_nan, n, false_or, not_and, not_le] at z
     by_cases l0 : x.lo.val < 0
     · simpa only [l0, l0.le, true_iff, true_implies] using z
@@ -873,7 +869,7 @@ lemma valid_error {e : Floating} (e0 : ¬e.n.isNeg) : Valid (-e) e where
 
 /-- `error` propagates `nan` -/
 lemma ne_nan_of_error {e : Floating} (n : error e ≠ nan) : e ≠ nan := by
-  contrapose n; simp only [ne_eq, not_not] at n; simp only [n, ne_eq, not_not, error_nan]
+  contrapose n; simp only [n, error_nan]
 
 /-- `grow` propagates `nan` -/
 @[simp] lemma grow_nan {x : Interval} : x.grow nan = nan := by
diff --git a/Interval/Interval/Division.lean b/Interval/Interval/Division.lean
@@ -236,7 +236,7 @@ lemma inv_def (x : Interval) : x⁻¹ = inv x := rfl
     approx (x.inv_pos l0) x'⁻¹ := by
   rw [inv_pos]
   have xn : x ≠ nan := by
-    contrapose l0; simp only [ne_eq, not_not] at l0
+    contrapose l0
     simp only [l0, lo_nan, not_lt, Floating.val_nan_lt_zero.le]
   simp only [approx, lo_eq_nan, xn, false_or] at ax
   have x0 := lt_of_lt_of_le l0 ax.1
diff --git a/Interval/Interval/Scale.lean b/Interval/Interval/Scale.lean
@@ -30,8 +30,8 @@ variable {x : Interval} {x' : ℝ}
 
 /-- `scaleB` propagates `nan` -/
 lemma ne_nan_of_scaleB {t : Int64} (n : x.scaleB t ≠ nan) : x ≠ nan := by
-  contrapose n; simp only [ne_eq, not_not] at n
-  simp only [n, nan_scaleB, ne_eq, not_true_eq_false, not_false_eq_true]
+  contrapose n
+  simp only [n, nan_scaleB]
 
 /-- `scaleB'` propagates `nan` -/
 @[simp] lemma nan_scaleB' {t : Fixed 0} : (nan : Interval).scaleB' t = nan := by
@@ -46,7 +46,7 @@ lemma ne_nan_of_scaleB' {t : Fixed 0} (n : x.scaleB' t ≠ nan) :
     x ≠ nan ∧ t ≠ nan := by
   contrapose n; simp only [ne_eq, not_not, not_and_or] at n
   rcases n with n | n
-  all_goals simp only [n, nan_scaleB', scaleB'_nan, ne_eq, not_true_eq_false, not_false_eq_true]
+  all_goals simp only [n, nan_scaleB', scaleB'_nan]
 
 /-- `scaleB` is conservative -/
 @[approx] lemma mem_approx_scaleB {t : Int64} (xm : approx x x') :
diff --git a/Interval/Misc/Int.lean b/Interval/Misc/Int.lean
@@ -12,7 +12,7 @@ import Interval.Misc.Nat
 /-- `abs` and `zpow` commute -/
 lemma abs_zpow {x : ℝ} {n : ℤ} : |x ^ n| = |x| ^ n := by
   induction' n using Int.rec with n n
-  · simp only [Int.ofNat_eq_coe, zpow_natCast, abs_pow]
+  · simp only [Int.ofNat_eq_natCast, zpow_natCast, abs_pow]
   · simp [zpow_negSucc, abs_inv, abs_pow]
 
 /-- `Int` division, rounding up or down -/
@@ -142,7 +142,7 @@ lemma Int.neg_ediv_neg {a b : ℤ} (b0 : 0 < b) (ab : ¬b ∣ a) : -(-a / b) = a
   have yb : y < b := by
     rw [← hy]
     convert emod_lt a b0.ne'
-    rw [Int.cast_natAbs, abs_of_pos b0, cast_id]
+    rw [Nat.cast_natAbs, abs_of_pos b0, cast_id]
   have e0 : -(b * x + y) = -y + (-x) * b := by ring
   have e1 : (b * x + y) = y + (x) * b := by ring
   rw [e0, e1]
@@ -295,7 +295,7 @@ lemma Int.abs_def {n : ℤ} : |n| = if n < 0 then -n else n := by
 lemma Int.natAbs_def {n : ℤ} : n.natAbs = if n < 0 then (-n).toNat else n.toNat := by
   simp only [natAbs]
   induction' n using Int.rec with n
-  · simp only [ofNat_eq_coe, toNat_neg_natCast, toNat_natCast]
+  · simp only [ofNat_eq_natCast, toNat_neg_natCast, toNat_natCast]
     split_ifs
     all_goals omega
   · simp only [Nat.succ_eq_add_one, negSucc_eq, neg_add_rev, reduceNeg, add_neg_lt_iff_lt_add,
diff --git a/Interval/Misc/Nat.lean b/Interval/Misc/Nat.lean
@@ -142,7 +142,7 @@ lemma Nat.bodd_two_pow {k : ℕ} : bodd (2^k) = decide (k = 0) := by
     simp only
     trans 2^n
     · apply Nat.pred_lt; apply pow_ne_zero; norm_num
-    · apply pow_lt_pow_right₀; norm_num; exact lt.base n
+    · apply pow_lt_pow_right₀; norm_num; exact lt_add_one n
 
 lemma Nat.land_eq_mod {n k : ℕ} : n &&& (2^k-1) = n % 2^k := by
   revert n
diff --git a/Interval/UInt128.lean b/Interval/UInt128.lean
@@ -219,8 +219,8 @@ lemma UInt128.toNat_succ' (x : UInt128) :
 
 lemma UInt128.coe_succ {x : UInt128} (h : (x:ℝ) ≠ (2:ℝ)^128-1) : (x.succ : ℝ) = x+1 := by
   rw [toReal, toReal, toNat_succ, Nat.cast_add_one]
-  contrapose h; simp only [ne_eq, not_not] at h
-  simp only [toReal, h, ne_eq, not_not]
+  contrapose h
+  simp only [toReal, h]
   norm_num
 
 /-!
@@ -261,7 +261,7 @@ lemma UInt128.toNat_neg (x : UInt128) : (-x).toNat = if x = 0 then 0 else 2^128
     · simp only [toNat_complement]
       omega
     · contrapose x0
-      simp only [toNat_complement, ne_eq, not_not, eq_iff_toNat_eq, toNat_zero] at x0 ⊢
+      simp only [toNat_complement, eq_iff_toNat_eq, toNat_zero] at x0 ⊢
       omega
 
 /-- `ofInt` commutes with `-` -/
@@ -585,7 +585,7 @@ lemma tb_false {x : UInt64} {i : ℕ} (il : 64 ≤ i) : Nat.testBit x.toNat i =
   replace x0 : 0 < x.toNat := by
     simpa only [ne_eq, UInt128.eq_iff_toNat_eq, UInt128.toNat_zero, ← Nat.pos_iff_ne_zero] using x0
   replace h : 2^128 ≤ 2^t := Nat.pow_le_pow_right (by norm_num) h
-  exact not_le.mpr (lt_of_lt_of_le (by norm_num) (Nat.mul_le_mul (Nat.succ_le.mpr x0) h))
+  exact not_le.mpr (lt_of_lt_of_le (by norm_num) (Nat.mul_le_mul (Nat.succ_le_iff.mpr x0) h))
 @[local simp] lemma a4 {t i : ℕ} (hi : i < 64) (ht : 64 ≤ t) : ¬t ≤ i := by omega
 @[local simp] lemma a5 {t i : ℕ} (hi : i < 64) (ti : t < 64) : i - t < 64 - t := by omega
 
@@ -761,7 +761,7 @@ lemma UInt128.toInt_shiftRightRound (x : UInt128) (s : UInt64) (up : Bool) :
   · simp only [not_le] at h1
     simp only [h3.1, Nat.mod_eq_of_lt h1, true_and] at h3 h4
     contrapose h3; clear h3
-    simp only [d1 h4, pow_zero, Nat.div_one, mul_one, not_not] at h4 ⊢
+    simp only [d1 h4, pow_zero, Nat.div_one, mul_one] at h4 ⊢
     rw [h4]; decide
   · simp only [not_le] at h1; clear h4
     simp only [h3.1, Nat.mod_eq_of_lt h1, true_and, Int.rdiv, Nat.cast_pow, Nat.cast_ofNat,
diff --git a/Interval/UInt64.lean b/Interval/UInt64.lean
@@ -164,7 +164,7 @@ lemma UInt64.toNat_sub'' {x y : UInt64} (h : y ≤ x) : (x - y).toNat = x.toNat
 lemma UInt64.toNat_add_one {m : UInt64} (h : m.toNat ≠ 2^64-1) : (m + 1).toNat = m.toNat + 1 := by
   rw [UInt64.toNat_add, toNat_one, Nat.mod_eq_of_lt]
   contrapose h; simp only [not_lt] at h
-  simp only [ne_eq, Nat.reducePow, Nat.add_one_sub_one, Decidable.not_not]
+  simp only [Nat.reducePow, Nat.add_one_sub_one]
   exact _root_.le_antisymm (UInt64.le_size_sub_one _) (Nat.sub_le_of_le_add h)
 
 /-- Adding 1 is usually adding one `toNat` -/
diff --git a/lake-manifest.json b/lake-manifest.json
diff --git a/lean-toolchain b/lean-toolchain
