chore: bump dependencies (#10315)

kim-em · kim-em · commit ba9f2e5baab5 · 2024-02-07T15:18:19.000Z
Co-authored-by: Scott Morrison &lt;scott.morrison@gmail.com&gt;
diff --git a/Archive/Imo/Imo1981Q3.lean b/Archive/Imo/Imo1981Q3.lean
@@ -149,7 +149,7 @@ variable {K : ℕ} (HK : N < fib K + fib (K + 1)) {N}
 theorem m_n_bounds {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ fib K ∧ n ≤ fib (K + 1) := by
   obtain ⟨k : ℕ, hm : m = fib k, hn : n = fib (k + 1)⟩ := h1.imp_fib m
   by_cases h2 : k < K + 1
-  · have h3 : k ≤ K := lt_succ_iff.mp h2
+  · have h3 : k ≤ K := Nat.lt_succ_iff.mp h2
     constructor
     · calc
         m = fib k := hm
diff --git a/Mathlib/Combinatorics/Additive/Behrend.lean b/Mathlib/Combinatorics/Additive/Behrend.lean
@@ -241,7 +241,7 @@ that we then optimize by tweaking the parameters. The (almost) optimal parameter
 theorem exists_large_sphere_aux (n d : ℕ) : ∃ k ∈ range (n * (d - 1) ^ 2 + 1),
     (↑(d ^ n) / ((n * (d - 1) ^ 2 :) + 1) : ℝ) ≤ (sphere n d k).card := by
   refine' exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => _) nonempty_range_succ _
-  · rw [mem_range, lt_succ_iff]
+  · rw [mem_range, Nat.lt_succ_iff]
     exact sum_sq_le_of_mem_box hx
   · rw [card_range, _root_.nsmul_eq_mul, mul_div_assoc', cast_add_one, mul_div_cancel_left,
       card_box]
diff --git a/Mathlib/Combinatorics/Quiver/Arborescence.lean b/Mathlib/Combinatorics/Quiver/Arborescence.lean
@@ -5,7 +5,6 @@ Authors: David Wärn
 -/
 import Mathlib.Combinatorics.Quiver.Path
 import Mathlib.Combinatorics.Quiver.Subquiver
-import Mathlib.Data.Nat.Defs
 import Mathlib.Order.WellFounded
 
 #align_import combinatorics.quiver.arborescence from "leanprover-community/mathlib"@"fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e"
diff --git a/Mathlib/Combinatorics/SetFamily/LYM.lean b/Mathlib/Combinatorics/SetFamily/LYM.lean
@@ -242,7 +242,7 @@ theorem IsAntichain.sperner [Fintype α] {𝒜 : Finset (Finset α)}
     rw [mem_range] at hr
     refine' div_le_div_of_le_left _ _ _ <;> norm_cast
     · exact Nat.zero_le _
-    · exact choose_pos (lt_succ_iff.1 hr)
+    · exact choose_pos (Nat.lt_succ_iff.1 hr)
     · exact choose_le_middle _ _
 #align finset.is_antichain.sperner Finset.IsAntichain.sperner
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
@@ -90,7 +90,7 @@ theorem equitabilise_aux (hs : a * m + b * (m + 1) = s.card) :
     refine' ⟨R.extend ht.ne_empty sdiff_disjoint (sdiff_sup_cancel hts), _, _, _⟩
     · simp only [extend_parts, mem_insert, forall_eq_or_imp, and_iff_left hR₁, htn, hn]
       exact ite_eq_or_eq _ _ _
-    · exact fun x hx => (card_le_card <| sdiff_subset _ _).trans (lt_succ_iff.1 <| h _ hx)
+    · exact fun x hx => (card_le_card <| sdiff_subset _ _).trans (Nat.lt_succ_iff.1 <| h _ hx)
     simp_rw [extend_parts, filter_insert, htn, m.succ_ne_self.symm.ite_eq_right_iff]
     split_ifs with ha
     · rw [hR₃, if_pos ha]
diff --git a/Mathlib/Computability/Ackermann.lean b/Mathlib/Computability/Ackermann.lean
@@ -323,11 +323,11 @@ theorem exists_lt_ack_of_nat_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) :
     apply add_lt_ack
   -- Left projection:
   · refine' ⟨0, fun n => _⟩
-    rw [ack_zero, lt_succ_iff]
+    rw [ack_zero, Nat.lt_succ_iff]
     exact unpair_left_le n
   -- Right projection:
   · refine' ⟨0, fun n => _⟩
-    rw [ack_zero, lt_succ_iff]
+    rw [ack_zero, Nat.lt_succ_iff]
     exact unpair_right_le n
   all_goals cases' IHf with a ha; cases' IHg with b hb
   -- Pairing:
diff --git a/Mathlib/Computability/PartrecCode.lean b/Mathlib/Computability/PartrecCode.lean
@@ -1106,7 +1106,7 @@ theorem evaln_prim : Primrec fun a : (ℕ × Code) × ℕ => evaln a.1.1 a.1.2 a
       · simp [evaln]
       let k := k' + 1
       simp only [show k'.succ = k from rfl]
-      simp? [Nat.lt_succ_iff] at nk says simp only [List.mem_range, lt_succ_iff] at nk
+      simp? [Nat.lt_succ_iff] at nk says simp only [List.mem_range, Nat.lt_succ_iff] at nk
       have hg :
         ∀ {k' c' n},
           Nat.pair k' (encode c') < Nat.pair k (encode c) →
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -902,7 +902,7 @@ theorem nthLe_cons {l : List α} {a : α} {n} (hl) :
   split_ifs with h
   · simp [nthLe, h]
   cases l
-  · rw [length_singleton, lt_succ_iff, nonpos_iff_eq_zero] at hl
+  · rw [length_singleton, Nat.lt_succ_iff, nonpos_iff_eq_zero] at hl
     contradiction
   cases n
   · contradiction
@@ -1292,7 +1292,7 @@ theorem take_one_drop_eq_of_lt_length {l : List α} {n : ℕ} (h : n < l.length)
   · by_cases h₁ : l = []
     · subst h₁
       rw [get_singleton]
-      simp only [length_singleton, lt_succ_iff, nonpos_iff_eq_zero] at h
+      simp only [length_singleton, Nat.lt_succ_iff, nonpos_iff_eq_zero] at h
       subst h
       simp
     have h₂ := h
diff --git a/Mathlib/Data/List/Intervals.lean b/Mathlib/Data/List/Intervals.lean
@@ -220,7 +220,7 @@ theorem filter_le_of_bot {n m : ℕ} (hnm : n < m) : ((Ico n m).filter fun x =>
   rw [← filter_lt_of_succ_bot hnm]
   exact filter_congr' fun _ _ => by
     rw [decide_eq_true_eq, decide_eq_true_eq]
-    exact lt_succ_iff.symm
+    exact Nat.lt_succ_iff.symm
 #align list.Ico.filter_le_of_bot List.Ico.filter_le_of_bot
 
 /-- For any natural numbers n, a, and b, one of the following holds:
diff --git a/Mathlib/Data/List/NatAntidiagonal.lean b/Mathlib/Data/List/NatAntidiagonal.lean
@@ -38,7 +38,7 @@ def antidiagonal (n : ℕ) : List (ℕ × ℕ) :=
 theorem mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ antidiagonal n ↔ x.1 + x.2 = n := by
   rw [antidiagonal, mem_map]; constructor
   · rintro ⟨i, hi, rfl⟩
-    rw [mem_range, lt_succ_iff] at hi
+    rw [mem_range, Nat.lt_succ_iff] at hi
     exact add_tsub_cancel_of_le hi
   · rintro rfl
     refine' ⟨x.fst, _, _⟩
@@ -97,7 +97,7 @@ theorem map_swap_antidiagonal {n : ℕ} :
   rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ←
     range_eq_range', map_map]
   apply map_congr
-  simp (config := { contextual := true }) [Nat.sub_sub_self, lt_succ_iff]
+  simp (config := { contextual := true }) [Nat.sub_sub_self, Nat.lt_succ_iff]
 #align list.nat.map_swap_antidiagonal List.Nat.map_swap_antidiagonal
 
 end Nat
diff --git a/Mathlib/Data/Nat/Cast/Order.lean b/Mathlib/Data/Nat/Cast/Order.lean
@@ -107,7 +107,7 @@ theorem one_le_cast : 1 ≤ (n : α) ↔ 1 ≤ n := by rw [← cast_one, cast_le
 
 @[simp, norm_cast]
 theorem cast_lt_one : (n : α) < 1 ↔ n = 0 := by
-  rw [← cast_one, cast_lt, lt_succ_iff, ← bot_eq_zero, le_bot_iff]
+  rw [← cast_one, cast_lt, Nat.lt_succ_iff, ← bot_eq_zero, le_bot_iff]
 #align nat.cast_lt_one Nat.cast_lt_one
 
 @[simp, norm_cast]
diff --git a/Mathlib/Data/Nat/Choose/Factorization.lean b/Mathlib/Data/Nat/Choose/Factorization.lean
@@ -57,7 +57,7 @@ in the binomial coefficient. -/
 theorem factorization_choose_le_one (p_large : n < p ^ 2) : (choose n k).factorization p ≤ 1 := by
   apply factorization_choose_le_log.trans
   rcases eq_or_ne n 0 with (rfl | hn0); · simp
-  exact lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)
+  exact Nat.lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)
 #align nat.factorization_choose_le_one Nat.factorization_choose_le_one
 
 theorem factorization_choose_of_lt_three_mul (hp' : p ≠ 2) (hk : p ≤ k) (hk' : p ≤ n - k)
diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean
@@ -74,7 +74,6 @@ alias _root_.LT.lt.nat_succ_le := succ_le_of_lt
 lemma not_succ_lt_self : ¬ succ n < n := not_lt_of_ge n.le_succ
 #align nat.not_succ_lt_self Nat.not_succ_lt_self
 
-lemma lt_succ_iff : m < succ n ↔ m ≤ n := ⟨le_of_lt_succ, lt_succ_of_le⟩
 #align nat.lt_succ_iff Nat.lt_succ_iff
 
 lemma succ_le_iff : succ m ≤ n ↔ m < n := ⟨lt_of_succ_le, succ_le_of_lt⟩
@@ -89,18 +88,17 @@ lemma le_succ_iff : m ≤ n.succ ↔ m ≤ n ∨ m = n.succ := by
 alias ⟨of_le_succ, _⟩ := le_succ_iff
 #align nat.of_le_succ Nat.of_le_succ
 
-lemma lt_succ_iff_lt_or_eq : m < n.succ ↔ m < n ∨ m = n := lt_succ_iff.trans Nat.le_iff_lt_or_eq
 #align nat.lt_succ_iff_lt_or_eq Nat.lt_succ_iff_lt_or_eq
 
 lemma eq_of_lt_succ_of_not_lt (hmn : m < n + 1) (h : ¬ m < n) : m = n :=
-  (lt_succ_iff_lt_or_eq.1 hmn).resolve_left h
+  (Nat.lt_succ_iff_lt_or_eq.1 hmn).resolve_left h
 #align nat.eq_of_lt_succ_of_not_lt Nat.eq_of_lt_succ_of_not_lt
 
 lemma eq_of_le_of_lt_succ (h₁ : n ≤ m) (h₂ : m < n + 1) : m = n :=
   Nat.le_antisymm (le_of_succ_le_succ h₂) h₁
 #align nat.eq_of_le_of_lt_succ Nat.eq_of_le_of_lt_succ
 
-lemma lt_iff_le_pred : ∀ {n}, 0 < n → (m < n ↔ m ≤ n - 1) | _ + 1, _ => lt_succ_iff
+lemma lt_iff_le_pred : ∀ {n}, 0 < n → (m < n ↔ m ≤ n - 1) | _ + 1, _ => Nat.lt_succ_iff
 #align nat.lt_iff_le_pred Nat.lt_iff_le_pred
 
 lemma le_of_pred_lt : ∀ {m}, pred m < n → m ≤ n
@@ -112,11 +110,11 @@ lemma lt_iff_add_one_le : m < n ↔ m + 1 ≤ n := by rw [succ_le_iff]
 #align nat.lt_iff_add_one_le Nat.lt_iff_add_one_le
 
 -- Just a restatement of `Nat.lt_succ_iff` using `+1`.
-lemma lt_add_one_iff : m < n + 1 ↔ m ≤ n := lt_succ_iff
+lemma lt_add_one_iff : m < n + 1 ↔ m ≤ n := Nat.lt_succ_iff
 #align nat.lt_add_one_iff Nat.lt_add_one_iff
 
 -- A flipped version of `lt_add_one_iff`.
-lemma lt_one_add_iff : m < 1 + n ↔ m ≤ n := by simp only [Nat.add_comm, lt_succ_iff]
+lemma lt_one_add_iff : m < 1 + n ↔ m ≤ n := by simp only [Nat.add_comm, Nat.lt_succ_iff]
 #align nat.lt_one_add_iff Nat.lt_one_add_iff
 
 -- This is true reflexively, by the definition of `≤` on ℕ,
@@ -173,7 +171,7 @@ lemma or_exists_succ : p 0 ∨ (∃ n, p (n + 1)) ↔ ∃ n, p n :=
 #align nat.or_exists_succ Nat.or_exists_succ
 
 lemma forall_lt_succ : (∀ m < n + 1, p m) ↔ (∀ m < n, p m) ∧ p n := by
-  simp only [lt_succ_iff, Nat.le_iff_lt_or_eq, or_comm, forall_eq_or_imp, and_comm]
+  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq, or_comm, forall_eq_or_imp, and_comm]
 #align nat.forall_lt_succ Nat.forall_lt_succ
 
 lemma exists_lt_succ : (∃ m < n + 1, p m) ↔ (∃ m < n, p m) ∨ p n := by
@@ -285,7 +283,8 @@ lemma one_lt_mul_iff : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n) := by
 attribute [simp] Nat.div_self
 
 lemma div_le_iff_le_mul_add_pred (hb : 0 < b) : a / b ≤ c ↔ a ≤ b * c + (b - 1) := by
-  rw [← lt_succ_iff, div_lt_iff_lt_mul hb, succ_mul, Nat.mul_comm]; cases hb <;> exact lt_succ_iff
+  rw [← Nat.lt_succ_iff, div_lt_iff_lt_mul hb, succ_mul, Nat.mul_comm]
+  cases hb <;> exact Nat.lt_succ_iff
 #align nat.div_le_iff_le_mul_add_pred Nat.div_le_iff_le_mul_add_pred
 
 /-- A version of `Nat.div_lt_self` using successors, rather than additional hypotheses. -/
@@ -706,7 +705,7 @@ lemma find_eq_iff (h : ∃ n : ℕ, p n) : Nat.find h = m ↔ p m ∧ ∀ n < m,
 #align nat.find_lt_iff Nat.find_lt_iff
 
 @[simp] lemma find_le_iff (h : ∃ n : ℕ, p n) (n : ℕ) : Nat.find h ≤ n ↔ ∃ m ≤ n, p m := by
-  simp only [exists_prop, ← lt_succ_iff, find_lt_iff]
+  simp only [exists_prop, ← Nat.lt_succ_iff, find_lt_iff]
 #align nat.find_le_iff Nat.find_le_iff
 
 @[simp] lemma le_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n ≤ Nat.find h ↔ ∀ m < n, ¬ p m := by
@@ -771,44 +770,10 @@ end FindGreatest
 
 /-! ### Decidability of predicates -/
 
--- To work around lean4#2552, we use `match` instead of `if/casesOn` with decidable instances.
-instance decidableBallLT :
-  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
-| 0, _, _ => isTrue fun _ ↦ (by cases ·)
-| n + 1, P, H =>
-  match decidableBallLT n (P · <| lt_succ_of_lt ·) with
-  | isFalse h => isFalse (h fun _ _ ↦ · _ _)
-  | isTrue h =>
-    match H n Nat.le.refl with
-    | isFalse p => isFalse (p <| · _ _)
-    | isTrue p => isTrue fun _ h' ↦ (lt_succ_iff_lt_or_eq.1 h').elim (h _) fun hn ↦ hn ▸ p
 #align nat.decidable_ball_lt Nat.decidableBallLT
-
--- To verify we don't have a regression on the speed, we put a difficult example.
--- any regression should take a huge amount of heartbeats -- we are currently at 187621.
--- For reference, the instance using `casesOn` took 44544 for 4; this one takes 1299 for 4.
-example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide
-
-instance decidableForallFin (P : Fin n → Prop) [DecidablePred P] : Decidable (∀ i, P i) :=
-  decidable_of_iff (∀ k h, P ⟨k, h⟩) ⟨fun m ⟨k, h⟩ ↦ m k h, fun m k h ↦ m ⟨k, h⟩⟩
 #align nat.decidable_forall_fin Nat.decidableForallFin
-
-instance decidableBallLe (n : ℕ) (P : ∀ k ≤ n, Prop) [∀ n h, Decidable (P n h)] :
-    Decidable (∀ n h, P n h) :=
-  decidable_of_iff (∀ (k) (h : k < succ n), P k (le_of_lt_succ h))
-    ⟨fun m k h ↦ m k (lt_succ_of_le h), fun m k _ ↦ m k _⟩
-#align nat.decidable_ball_le Nat.decidableBallLe
-
-instance decidableExistsLT [h : DecidablePred p] : DecidablePred fun n ↦ ∃ m : ℕ, m < n ∧ p m
-  | 0 => isFalse (by simp)
-  | n + 1 =>
-    @decidable_of_decidable_of_iff _ _ (@instDecidableOr _ _ (decidableExistsLT n) (h n))
-      (by simp only [lt_succ_iff_lt_or_eq, or_and_right, exists_or, exists_eq_left])
+#align nat.decidable_ball_le Nat.decidableBallLE
 #align nat.decidable_exists_lt Nat.decidableExistsLT
-
-instance decidableExistsLe [DecidablePred p] : DecidablePred fun n ↦ ∃ m : ℕ, m ≤ n ∧ p m :=
-  fun n ↦ decidable_of_iff (∃ m, m < n + 1 ∧ p m)
-    (exists_congr fun _ ↦ and_congr_left' lt_succ_iff)
-#align nat.decidable_exists_le Nat.decidableExistsLe
+#align nat.decidable_exists_le Nat.decidableExistsLE
 
 end Nat
diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -390,7 +390,7 @@ theorem descFactorial_self : ∀ n : ℕ, n.descFactorial n = n !
 theorem descFactorial_eq_zero_iff_lt {n : ℕ} : ∀ {k : ℕ}, n.descFactorial k = 0 ↔ n < k
   | 0 => by simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]
   | succ k => by
-    rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, lt_succ_iff,
+    rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
       tsub_eq_zero_iff_le, lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
     exact fun h _ => h
 #align nat.desc_factorial_eq_zero_iff_lt Nat.descFactorial_eq_zero_iff_lt
diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -667,7 +667,7 @@ theorem prod_primeFactors_gcd_mul_prod_primeFactors_mul {β : Type*} [CommMonoid
 theorem setOf_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) :
     { i : ℕ | i ≠ 0 ∧ p ^ i ∣ n } = Set.Icc 1 (n.factorization p) := by
   ext
-  simp [lt_succ_iff, one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn]
+  simp [Nat.lt_succ_iff, one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn]
 #align nat.set_of_pow_dvd_eq_Icc_factorization Nat.setOf_pow_dvd_eq_Icc_factorization
 
 /-- The set of positive powers of prime `p` that divide `n` is exactly the set of
diff --git a/Mathlib/Data/Nat/Fib/Zeckendorf.lean b/Mathlib/Data/Nat/Fib/Zeckendorf.lean
@@ -100,7 +100,7 @@ lemma greatestFib_ne_zero : greatestFib n ≠ 0 ↔ n ≠ 0 := greatestFib_eq_ze
 
 lemma greatestFib_sub_fib_greatestFib_le_greatestFib (hn : n ≠ 0) :
     greatestFib (n - fib (greatestFib n)) ≤ greatestFib n - 2 := by
-  rw [← lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
+  rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
     succ_pred, ← fib_add_one]
   exact n.lt_fib_greatestFib_add_one
   · simpa
diff --git a/Mathlib/Data/Nat/Interval.lean b/Mathlib/Data/Nat/Interval.lean
@@ -179,7 +179,7 @@ theorem Icc_succ_left : Icc a.succ b = Ioc a b := by
 
 theorem Ico_succ_right : Ico a b.succ = Icc a b := by
   ext x
-  rw [mem_Ico, mem_Icc, lt_succ_iff]
+  rw [mem_Ico, mem_Icc, Nat.lt_succ_iff]
 #align nat.Ico_succ_right Nat.Ico_succ_right
 
 theorem Ico_succ_left : Ico a.succ b = Ioo a b := by
@@ -194,7 +194,7 @@ theorem Icc_pred_right {b : ℕ} (h : 0 < b) : Icc a (b - 1) = Ico a b := by
 
 theorem Ico_succ_succ : Ico a.succ b.succ = Ioc a b := by
   ext x
-  rw [mem_Ico, mem_Ioc, succ_le_iff, lt_succ_iff]
+  rw [mem_Ico, mem_Ioc, succ_le_iff, Nat.lt_succ_iff]
 #align nat.Ico_succ_succ Nat.Ico_succ_succ
 
 @[simp]
@@ -253,7 +253,7 @@ theorem Ico_image_const_sub_eq_Ico (hac : a ≤ c) :
       rw [← succ_sub_succ c]
       exact (tsub_le_tsub_iff_left (succ_le_succ <| hx.2.le.trans h)).2 hx.2
   · rintro ⟨hb, ha⟩
-    rw [lt_tsub_iff_left, lt_succ_iff] at ha
+    rw [lt_tsub_iff_left, Nat.lt_succ_iff] at ha
     have hx : x ≤ c := (Nat.le_add_left _ _).trans ha
     refine' ⟨c - x, _, tsub_tsub_cancel_of_le hx⟩
     · rw [mem_Ico]
diff --git a/Mathlib/Data/Nat/Lattice.lean b/Mathlib/Data/Nat/Lattice.lean
@@ -115,7 +115,7 @@ theorem sInf_upward_closed_eq_succ_iff {s : Set ℕ} (hs : ∀ k₁ k₂ : ℕ,
     exact k; assumption
   · rintro ⟨H, H'⟩
     rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
-    exact ⟨H, fun n hnk hns ↦ H' <| hs n k (lt_succ_iff.mp hnk) hns⟩
+    exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩
 #align nat.Inf_upward_closed_eq_succ_iff Nat.sInf_upward_closed_eq_succ_iff
 
 /-- This instance is necessary, otherwise the lattice operations would be derived via
diff --git a/Mathlib/Data/Nat/Log.lean b/Mathlib/Data/Nat/Log.lean
@@ -135,7 +135,7 @@ theorem lt_pow_succ_log_self {b : ℕ} (hb : 1 < b) (x : ℕ) : x < b ^ (log b x
 theorem log_eq_iff {b m n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) :
     log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1) := by
   rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)
-  · rw [le_antisymm_iff, ← lt_succ_iff, ← pow_le_iff_le_log, ← lt_pow_iff_log_lt, and_comm] <;>
+  · rw [le_antisymm_iff, ← Nat.lt_succ_iff, ← pow_le_iff_le_log, ← lt_pow_iff_log_lt, and_comm] <;>
       assumption
   · have hm : m ≠ 0 := h.resolve_right hbn
     rw [not_and_or, not_lt, Ne.def, not_not] at hbn
@@ -283,7 +283,7 @@ theorem clog_pos {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : 0 < clog b n := by
 theorem clog_eq_one {b n : ℕ} (hn : 2 ≤ n) (h : n ≤ b) : clog b n = 1 := by
   rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]
   have n_pos : 0 < n := (zero_lt_two' ℕ).trans_le hn
-  rw [← lt_succ_iff, Nat.div_lt_iff_lt_mul (n_pos.trans_le h), ← succ_le_iff, ← pred_eq_sub_one,
+  rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul (n_pos.trans_le h), ← succ_le_iff, ← pred_eq_sub_one,
     succ_pred_eq_of_pos (add_pos n_pos (n_pos.trans_le h)), succ_mul, one_mul]
   exact add_le_add_right h _
 #align nat.clog_eq_one Nat.clog_eq_one
diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean
@@ -67,7 +67,7 @@ theorem multiplicity_eq_card_pow_dvd {m n b : ℕ} (hm : m ≠ 1) (hn : 0 < n) (
       congr_arg _ <|
         congr_arg card <|
           Finset.ext fun i => by
-            rw [mem_filter, mem_Ico, mem_Ico, lt_succ_iff, ← @PartENat.coe_le_coe i,
+            rw [mem_filter, mem_Ico, mem_Ico, Nat.lt_succ_iff, ← @PartENat.coe_le_coe i,
               PartENat.natCast_get, ← pow_dvd_iff_le_multiplicity, and_right_comm]
             refine' (and_iff_left_of_imp fun h => lt_of_le_of_lt _ hb).symm
             cases' m with m
diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean
@@ -283,12 +283,12 @@ theorem le_nth_of_lt_nth_succ {k a : ℕ} (h : a < nth p (k + 1)) (ha : p a) : a
   cases' (setOf p).finite_or_infinite with hf hf
   · rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
     cases' lt_or_le (k + 1) hf.toFinset.card with hk hk
-    · rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, lt_succ_iff,
+    · rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, Nat.lt_succ_iff,
         ← (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h
     · rw [nth_of_card_le _ hk] at h
       exact absurd h (zero_le _).not_lt
   · rcases subset_range_nth ha with ⟨n, rfl⟩
-    rwa [nth_lt_nth hf, lt_succ_iff, ← nth_le_nth hf] at h
+    rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h
 #align nat.le_nth_of_lt_nth_succ Nat.le_nth_of_lt_nth_succ
 
 section Count
diff --git a/Mathlib/Data/Nat/Order/Basic.lean b/Mathlib/Data/Nat/Order/Basic.lean
@@ -142,7 +142,7 @@ theorem two_le_iff : ∀ n, 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1
 
 @[simp]
 theorem lt_one_iff {n : ℕ} : n < 1 ↔ n = 0 :=
-  lt_succ_iff.trans nonpos_iff_eq_zero
+  Nat.lt_succ_iff.trans nonpos_iff_eq_zero
 #align nat.lt_one_iff Nat.lt_one_iff
 
 /-! ### `add` -/
@@ -567,9 +567,10 @@ theorem findGreatest_eq_iff :
       · rintro ⟨hle, hP, hm⟩
         refine ⟨hle.trans k.le_succ, hP, fun n hlt hle => ?_⟩
         rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt')
-        exacts [hk, hm hlt <| lt_succ_iff.1 hlt']
+        exacts [hk, hm hlt <| Nat.lt_succ_iff.1 hlt']
       · rintro ⟨hle, hP, hm⟩
-        refine ⟨lt_succ_iff.1 (hle.lt_of_ne ?_), hP, fun n hlt hle => hm hlt (hle.trans k.le_succ)⟩
+        refine ⟨Nat.lt_succ_iff.1 (hle.lt_of_ne ?_), hP,
+          fun n hlt hle => hm hlt (hle.trans k.le_succ)⟩
         rintro rfl
         exact hk (hP k.succ_ne_zero)
 #align nat.find_greatest_eq_iff Nat.findGreatest_eq_iff
@@ -743,7 +744,7 @@ instance decidableLoHi (lo hi : ℕ) (P : ℕ → Prop) [H : DecidablePred P] :
 instance decidableLoHiLe (lo hi : ℕ) (P : ℕ → Prop) [DecidablePred P] :
     Decidable (∀ x, lo ≤ x → x ≤ hi → P x) :=
   decidable_of_iff (∀ x, lo ≤ x → x < hi + 1 → P x) <|
-    ball_congr fun _ _ => imp_congr lt_succ_iff Iff.rfl
+    ball_congr fun _ _ => imp_congr Nat.lt_succ_iff Iff.rfl
 #align nat.decidable_lo_hi_le Nat.decidableLoHiLe
 
 end Nat
diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean
@@ -214,7 +214,7 @@ theorem le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b :=
   rintro ⟨a, rfl⟩ ⟨b, rfl⟩
   -- porting note: Needed to give an explicit argument to `mul_add_one`
   rw [← mul_add_one n] at h
-  exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _
+  exact mul_le_mul_left' (Nat.lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _
 #align nat.le_of_lt_add_of_dvd Nat.le_of_lt_add_of_dvd
 
 #align nat.mod_div_self Nat.mod_div_self
diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean
diff --git a/Mathlib/Data/Nat/Sqrt.lean b/Mathlib/Data/Nat/Sqrt.lean
diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean
diff --git a/Mathlib/Data/PNat/Basic.lean b/Mathlib/Data/PNat/Basic.lean
diff --git a/Mathlib/Dynamics/PeriodicPts.lean b/Mathlib/Dynamics/PeriodicPts.lean
diff --git a/Mathlib/NumberTheory/Bertrand.lean b/Mathlib/NumberTheory/Bertrand.lean
diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean
diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
diff --git a/Mathlib/NumberTheory/SmoothNumbers.lean b/Mathlib/NumberTheory/SmoothNumbers.lean
diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean
diff --git a/lake-manifest.json b/lake-manifest.json
