more deprecations for leanprover/lean4#10967

Author: kim-em

Archive/Imo/Imo1988Q6.lean

@@ -233,14 +233,14 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
         rw [← sub_eq_zero, ← h_root]
         ring
       rw [hzx] at hpos
-      replace hpos : z * x + 1 > 0 := pos_of_mul_pos_left hpos (Int.ofNat_zero_le k)
+      replace hpos : z * x + 1 > 0 := pos_of_mul_pos_left hpos (Int.natCast_nonneg k)
       replace hpos : z * x ≥ 0 := Int.le_of_lt_add_one hpos
       apply nonneg_of_mul_nonneg_left hpos (mod_cast hx)
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt
       calc
         z * y > x * x := by apply mul_lt_mul' <;> omega
-        _ ≥ x * x - k := sub_le_self _ (Int.ofNat_zero_le k)
+        _ ≥ x * x - k := sub_le_self _ (Int.natCast_nonneg k)
   · -- There is no base case in this application of Vieta jumping.
     simp
 

Archive/Imo/Imo2024Q5.lean

@@ -387,7 +387,7 @@ lemma Path.findFstEq_fst_sub_one_mem (p : Path N) {r : Fin (N + 2)} (hr : r ≠
   rw [← cells.takeWhile_append_dropWhile (p := fun c ↦ ! decide (r ≤ c.1)),
     List.isChain_append] at valid_move_seq
   have ha := valid_move_seq.2.2
-  simp only [List.head?_eq_head hd', List.getLast?_eq_getLast ht, Option.mem_def,
+  simp only [List.head?_eq_some_head hd', List.getLast?_eq_some_getLast ht, Option.mem_def,
     Option.some.injEq, forall_eq'] at ha
   nth_rw 1 [← cells.takeWhile_append_dropWhile (p := fun c ↦ ! decide (r ≤ c.1))]
   refine List.mem_append_left _ ?_

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -114,15 +114,17 @@ theorem counted_succ_succ (p q : ℕ) :
     obtain ⟨hl₀, hl₁, hl₂⟩ := hl
     obtain hlast | hlast := hl₂ (l.head hlnil) (List.head_mem hlnil)
     · refine Or.inl ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
-      · rw [List.count_tail, hl₀, List.head?_eq_head hlnil, hlast, beq_self_eq_true, if_pos rfl,
-          Nat.add_sub_cancel]
-      · rw [List.count_tail, hl₁, List.head?_eq_head hlnil, hlast, if_neg (by decide), Nat.sub_zero]
+      · rw [List.count_tail, hl₀, List.head?_eq_some_head hlnil, hlast, beq_self_eq_true,
+          if_pos rfl, Nat.add_sub_cancel]
+      · rw [List.count_tail, hl₁, List.head?_eq_some_head hlnil, hlast, if_neg (by decide),
+          Nat.sub_zero]
       · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
       · rw [← hlast, List.cons_head_tail]
     · refine Or.inr ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
-      · rw [List.count_tail, hl₀, List.head?_eq_head hlnil, hlast, if_neg (by decide), Nat.sub_zero]
-      · rw [List.count_tail, hl₁, List.head?_eq_head hlnil, hlast, beq_self_eq_true, if_pos rfl,
-          Nat.add_sub_cancel]
+      · rw [List.count_tail, hl₀, List.head?_eq_some_head hlnil, hlast, if_neg (by decide),
+          Nat.sub_zero]
+      · rw [List.count_tail, hl₁, List.head?_eq_some_head hlnil, hlast, beq_self_eq_true,
+          if_pos rfl, Nat.add_sub_cancel]
       · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
       · rw [← hlast, List.cons_head_tail]
   · rintro (⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩ | ⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩)

MathlibTest/ExtractGoal.lean

@@ -164,14 +164,14 @@ example : ∀ n, n < n + 1 := by
 
 -- Throwing metavariables into the terms
 /--
-info: theorem _example.extracted_1 (m : ℕ) (this : m < m.succ.succ) : m < m + 1 := sorry
+info: theorem _example.extracted_1 (m : ℕ) (this : m < (m + 1).succ) : m < m + 1 := sorry
 ---
 warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example : ∀ n, n < n + 1 := by
   intro m
   show _
-  have : m < _ := Nat.lt.step (Nat.lt.base m)
+  have : m < _ := Nat.lt_succ_of_lt (Nat.lt_add_one m)
   extract_goal
   sorry

MathlibTest/Have.lean

@@ -33,9 +33,9 @@ example : True := by
   have _h : Nat
   · exact this
   have _h' x : x < x + 1
-  · exact Nat.lt.base x
+  · exact Nat.lt_add_one x
   have _h'' (x : Nat) : x < x + 1
-  · exact Nat.lt.base x
+  · exact Nat.lt_add_one x
   let _m
   · exact 6
   let _m' x (y : Nat) : x + y = y + x

MathlibTest/lift.lean

@@ -21,7 +21,7 @@ example (n : ℤ) (hn : 0 ≤ n) : 0 ≤ n + 1 := by
 example (n : ℤ) (hn : 0 ≤ n) : 0 ≤ n + 1 := by
   lift n to ℕ using hn
   guard_target =ₛ 0 ≤ (n : Int) + 1
-  exact Int.le_add_one (Int.ofNat_zero_le _)
+  exact Int.le_add_one (Int.natCast_nonneg _)
 
 example (n : ℤ) (hn : 0 ≤ n) : 0 ≤ n + 1 := by
   have hn' := hn