[Merged by Bors] - chore: adaptations for nightly-2025-02-09

Archive/Imo/Imo2024Q3.lean

@@ -58,7 +58,7 @@ lemma N_lt_of_M_le_apply {a : ℕ → ℕ} {N i : ℕ} (h : M a N ≤ a i) : N <
   exact Nat.not_succ_le_self _ (h.trans (Finset.le_sup (Finset.mem_range_succ_iff.2 hi)))
 
 lemma ne_zero_of_M_le_apply {a : ℕ → ℕ} {N i : ℕ} (h : M a N ≤ a i) : i ≠ 0 :=
-  Nat.not_eq_zero_of_lt (N_lt_of_M_le_apply h)
+  Nat.ne_zero_of_lt (N_lt_of_M_le_apply h)
 
 lemma apply_lt_of_M_le_apply {a : ℕ → ℕ} {N i j : ℕ} (hi : M a N ≤ a i) (hj : j ≤ N) :
     a j < a i :=

Mathlib/Algebra/Order/Kleene.lean

@@ -139,7 +139,7 @@ lemma natCast_eq_one {n : ℕ} (nezero : n ≠ 0) : (n : α) = 1 := by
   | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]
 
 lemma ofNat_eq_one {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : α) = 1 :=
-  natCast_eq_one <| Nat.not_eq_zero_of_lt Nat.AtLeastTwo.prop
+  natCast_eq_one <| Nat.ne_zero_of_lt Nat.AtLeastTwo.prop
 
 theorem nsmul_eq_self : ∀ {n : ℕ} (_ : n ≠ 0) (a : α), n • a = a
   | 0, h => (h rfl).elim

Mathlib/Data/Nat/Choose/Central.lean

@@ -80,7 +80,7 @@ theorem four_pow_lt_mul_centralBinom (n : ℕ) (n_big : 4 ≤ n) : 4 ^ n < n * c
   rcases lt_trichotomy n 4 with (hn | rfl | hn)
   · clear IH; exact False.elim ((not_lt.2 n_big) hn)
   · norm_num [centralBinom, choose]
-  obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.not_eq_zero_of_lt hn)
+  obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.ne_zero_of_lt hn)
   calc
     4 ^ (n + 1) < 4 * (n * centralBinom n) := lt_of_eq_of_lt pow_succ' <|
       (mul_lt_mul_left <| zero_lt_four' ℕ).mpr (IH n n.lt_succ_self (Nat.le_of_lt_succ hn))

Mathlib/Data/Nat/Digits.lean

@@ -414,7 +414,7 @@ theorem digits_base_pow_mul {b k m : ℕ} (hb : 1 < b) (hm : 0 < m) :
     have hmb : 0 < m * b := lt_mul_of_lt_of_one_lt' hm hb
     let h1 := digits_def' hb hmb
     have h2 : m = m * b / b :=
-      Nat.eq_div_of_mul_eq_left (not_eq_zero_of_lt hb) rfl
+      Nat.eq_div_of_mul_eq_left (ne_zero_of_lt hb) rfl
     simp only [mul_mod_left, ← h2] at h1
     rw [List.replicate_succ', List.append_assoc, List.singleton_append, ← h1, ← ih hmb]
     ring_nf

Mathlib/Data/Nat/MaxPowDiv.lean

@@ -103,7 +103,7 @@ theorem le_of_dvd {p n pow : ℕ} (hp : 1 < p) (hn : 0 < n) (h : p ^ pow ∣ n)
     apply Nat.pos_of_ne_zero
     intro h'
     rw [h',mul_zero] at hc
-    exact not_eq_zero_of_lt hn hc
+    omega
   simp [hc, base_pow_mul hp this]
 
 end maxPowDiv

Mathlib/Data/Nat/Prime/Defs.lean

@@ -88,7 +88,7 @@ theorem prime_def {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, m ∣ p → m = 1 
   simp only [Nat.isUnit_iff]
   apply Or.imp_right _ (h.2 a _)
   · rintro rfl
-    rw [← mul_right_inj' (not_eq_zero_of_lt h1), ← hab, mul_one]
+    rw [← mul_right_inj' (Nat.ne_zero_of_lt h1), ← hab, mul_one]
   · rw [hab]
     exact dvd_mul_right _ _
 

Mathlib/FieldTheory/Differential/Basic.lean

@@ -114,7 +114,7 @@ noncomputable instance (p : F[X]) [Fact (Irreducible p)] [Fact p.Monic] :
       · intro nh
         simp [natDegree_eq_zero_of_derivative_eq_zero nh] at this
       apply natDegree_derivative_lt
-      exact Nat.not_eq_zero_of_lt this)
+      exact Nat.ne_zero_of_lt this)
 
 instance (p : F[X]) [Fact (Irreducible p)] [Fact p.Monic] :
     DifferentialAlgebra F (AdjoinRoot p) where
@@ -175,7 +175,7 @@ noncomputable def uniqueDifferentialAlgebraFiniteDimensional [FiniteDimensional
     · intro nh
       simp [natDegree_eq_zero_of_derivative_eq_zero nh] at this
     apply natDegree_derivative_lt
-    exact Nat.not_eq_zero_of_lt this
+    exact Nat.ne_zero_of_lt this
 
 noncomputable instance (B : IntermediateField F K) [FiniteDimensional F B] : Differential B :=
   differentialFiniteDimensional F B

Mathlib/FieldTheory/KummerPolynomial.lean

@@ -28,7 +28,7 @@ lemma root_X_pow_sub_C_pow (n : ℕ) (a : K) :
 
 lemma root_X_pow_sub_C_ne_zero {n : ℕ} (hn : 1 < n) (a : K) :
     (AdjoinRoot.root (X ^ n - C a)) ≠ 0 :=
-  mk_ne_zero_of_natDegree_lt (monic_X_pow_sub_C _ (Nat.not_eq_zero_of_lt hn))
+  mk_ne_zero_of_natDegree_lt (monic_X_pow_sub_C _ (Nat.ne_zero_of_lt hn))
     X_ne_zero <| by rwa [natDegree_X_pow_sub_C, natDegree_X]
 
 lemma root_X_pow_sub_C_ne_zero' {n : ℕ} {a : K} (hn : 0 < n) (ha : a ≠ 0) :

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -228,7 +228,7 @@ alias addOrderOf_generator_eq_natCard := addOrderOf_eq_card_of_forall_mem_zmulti
 @[to_additive]
 theorem exists_pow_ne_one_of_isCyclic [G_cyclic : IsCyclic G]
     {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Nat.card G) : ∃ a : G, a ^ k ≠ 1 := by
-  have : Finite G := Nat.finite_of_card_ne_zero (Nat.not_eq_zero_of_lt k_lt_card_G)
+  have : Finite G := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt k_lt_card_G)
   rcases G_cyclic with ⟨a, ha⟩
   use a
   contrapose! k_lt_card_G

Mathlib/NumberTheory/Ostrowski.lean

@@ -324,7 +324,7 @@ lemma one_lt_of_not_bounded (notbdd : ¬ ∀ n : ℕ, f n ≤ 1) {n₀ : ℕ} (h
     _ = n₀ * (Nat.log n₀ m + 1) := by
       rw [List.mapIdx_eq_zipIdx_map, List.eq_replicate_of_mem (a := (n₀ : ℝ)) (l := L.zipIdx.map _),
         List.sum_replicate, List.length_map, List.length_zipIdx, nsmul_eq_mul, mul_comm,
-        Nat.digits_len n₀ m hn₀ (not_eq_zero_of_lt hm), Nat.cast_add_one]
+        Nat.digits_len n₀ m hn₀ (ne_zero_of_lt hm), Nat.cast_add_one]
       simp +contextual
     _ ≤ n₀ * (logb n₀ m + 1) := by gcongr; exact natLog_le_logb ..
   -- For h_ineq2 we need to exclude the case n = 0.
@@ -376,7 +376,7 @@ private lemma param_upperbound {k : ℕ} (hk : k ≠ 0) :
     _ = m * ((Nat.digits m n).mapIdx fun i _ ↦ f m ^ i).sum := list_mul_sum (m.digits n) (f m) m
     _ = m * ((f m ^ (d + 1) - 1) / (f m - 1)) := by
       rw [list_geom _ (ne_of_gt (one_lt_of_not_bounded notbdd hm)),
-        ← Nat.digits_len m n hm (not_eq_zero_of_lt hn)]
+        ← Nat.digits_len m n hm (ne_zero_of_lt hn)]
     _ ≤ m * ((f m ^ (d + 1)) / (f m - 1)) := by
       gcongr
       · linarith only [one_lt_of_not_bounded notbdd hm]
@@ -406,7 +406,7 @@ lemma le_pow_log : f n ≤ f m ^ logb m n := by
     nth_rw 2 [← one_mul (f ↑m ^ logb ↑m ↑n)]
     exact (tendsto_const_rpow_inv (expr_pos hm notbdd)).mul_const _
   exact le_of_tendsto_of_tendsto (tendsto_const_nhds (x:= f ↑n)) this <|
-    eventually_atTop.mpr ⟨2, fun b hb ↦ param_upperbound hm hn notbdd (not_eq_zero_of_lt hb)⟩
+    eventually_atTop.mpr ⟨2, fun b hb ↦ param_upperbound hm hn notbdd (ne_zero_of_lt hb)⟩
 
 include hm hn notbdd in
 /-- Given `m, n ≥ 2` and `f m = m ^ s`, `f n = n ^ t` for `s, t > 0`, we have `t ≤ s`. -/
@@ -440,8 +440,8 @@ theorem equiv_real_of_unbounded : f ≈ real := by
     have : (logb (↑m) (f ↑m))⁻¹ ≠ 0 := by
       simp only [ne_eq, inv_eq_zero, logb_eq_zero, Nat.cast_eq_zero, Nat.cast_eq_one, map_eq_zero,
         not_or]
-      exact ⟨not_eq_zero_of_lt oneltm, oneltm.ne', by norm_cast,
-        not_eq_zero_of_lt oneltm, ne_of_not_le hm, by linarith only [apply_nonneg f ↑m]⟩
+      exact ⟨ne_zero_of_lt oneltm, oneltm.ne', by norm_cast,
+        ne_zero_of_lt oneltm, ne_of_not_le hm, by linarith only [apply_nonneg f ↑m]⟩
     simp [hs, this]
   · simp
   · simp only [real_eq_abs, abs_cast, Rat.cast_natCast]
@@ -452,7 +452,7 @@ theorem equiv_real_of_unbounded : f ≈ real := by
       rw [rpow_logb (mod_cast zero_lt_of_lt oneltm) (mod_cast oneltm.ne') (by linarith only [hm])]
     have hfn : f n = n ^ logb n (f n) := by
       rw [rpow_logb (mod_cast zero_lt_of_lt h) (mod_cast h.ne')
-        (by apply map_pos_of_ne_zero; exact_mod_cast not_eq_zero_of_lt h)]
+        (by apply map_pos_of_ne_zero; exact_mod_cast ne_zero_of_lt h)]
     rwa [← hs, eq_of_eq_pow oneltm h notbdd hfm hfn]
 
 end Archimedean

Mathlib/NumberTheory/SmoothNumbers.lean

@@ -357,7 +357,7 @@ lemma smoothNumbers_succ {N : ℕ} (hN : ¬ N.Prime) : N.succ.smoothNumbers = N.
 
 /-- All `m`, `0 < m < n` are `n`-smooth numbers -/
 lemma mem_smoothNumbers_of_lt {m n : ℕ} (hm : 0 < m) (hmn : m < n) : m ∈ n.smoothNumbers :=
-  smoothNumbers_eq_factoredNumbers _ ▸ ⟨not_eq_zero_of_lt hm,
+  smoothNumbers_eq_factoredNumbers _ ▸ ⟨ne_zero_of_lt hm,
   fun _ h => Finset.mem_range.mpr <| lt_of_le_of_lt (le_of_mem_primeFactorsList h) hmn⟩
 
 /-- The non-zero non-`N`-smooth numbers are `≥ N`. -/

Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean

@@ -106,7 +106,7 @@ lemma accumulate_invAccumulate {n m} (hmn : m ≤ n) {s : Fin m → ℕ} (hs : A
     rw [accumulate_rec (him.trans_le hmn) hi, ih hi, invAccumulate, dif_pos him, dif_pos hi]
     simp only
     exact Nat.sub_add_cancel (hs i.le_succ)
-  · have := (Nat.sub_one_add_one <| Nat.not_eq_zero_of_lt hm).symm
+  · have := (Nat.sub_one_add_one <| Nat.ne_zero_of_lt hm).symm
     rw [accumulate_last (hm.trans_le hmn) this, invAccumulate, dif_pos hm, dif_neg this.not_gt,
       Nat.sub_zero]
     intro j hj

Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

@@ -601,7 +601,7 @@ private theorem _root_.IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul_field {K : Ty
     [Field K] {ζ : K} (x y : K) (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
     x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y) := by
   by_cases hy : y = 0
-  · simp only [hy, zero_pow (Nat.not_eq_zero_of_lt hpos), sub_zero, mul_zero, prod_const]
+  · simp only [hy, zero_pow (Nat.ne_zero_of_lt hpos), sub_zero, mul_zero, prod_const]
     congr
     rw [h.card_nthRootsFinset]
   convert congr_arg (eval (x/y) · * y ^ card (nthRootsFinset n K)) <| X_pow_sub_one_eq_prod hpos h

MathlibTest/Multigoal.lean

@@ -123,7 +123,7 @@ example : True ∧ True := by
 -- Exclude `fail_if_success` and `success_if_fail_with_msg` from linting.
 example : True := by
   fail_if_success done
-  success_if_fail_with_msg "internal exception #4" done
+  success_if_fail_with_msg "internal exception #5" done
   exact .intro
 
 /-!

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "40eaac3108ab30c91732fa2962d26d849ebc8242",
+   "rev": "fcc3faa429c1ab53c0504b076e03c852512a04e3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-02-06
+leanprover/lean4:nightly-2025-02-09