feat: port Init.Data.Nat.Lemmas (#5782)

Previously this was an ad-hoc port

Mathlib/Data/Nat/Dist.lean

@@ -118,7 +118,7 @@ theorem dist_succ_succ {i j : Nat} : dist (succ i) (succ j) = dist i j := by
 #align nat.dist_succ_succ Nat.dist_succ_succ
 
 theorem dist_pos_of_ne {i j : Nat} : i ≠ j → 0 < dist i j := fun hne =>
-  Nat.lt_by_cases
+  Nat.ltByCases
     (fun h : i < j => by rw [dist_eq_sub_of_le (le_of_lt h)]; apply tsub_pos_of_lt h)
     (fun h : i = j => by contradiction) fun h : i > j => by
     rw [dist_eq_sub_of_le_right (le_of_lt h)]; apply tsub_pos_of_lt h

Mathlib/Data/Nat/Factorization/Basic.lean

@@ -795,7 +795,7 @@ we can define `P` for all natural numbers. -/
 @[elab_as_elim]
 def recOnPrimePow {P : ℕ → Sort _} (h0 : P 0) (h1 : P 1)
     (h : ∀ a p n : ℕ, p.Prime → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)) : ∀ a : ℕ, P a := fun a =>
-  Nat.strong_rec_on a fun n =>
+  Nat.strongRecOn a fun n =>
     match n with
     | 0 => fun _ => h0
     | 1 => fun _ => h1

Mathlib/Data/Nat/Fib.lean

@@ -291,7 +291,7 @@ theorem fib_dvd (m n : ℕ) (h : m ∣ n) : fib m ∣ fib n := by
 
 theorem fib_succ_eq_sum_choose :
     ∀ n : ℕ, fib (n + 1) = ∑ p in Finset.Nat.antidiagonal n, choose p.1 p.2 :=
-  two_step_induction rfl rfl fun n h1 h2 => by
+  twoStepInduction rfl rfl fun n h1 h2 => by
     rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']
     simp [choose_succ_succ, Finset.sum_add_distrib, add_left_comm]
 #align nat.fib_succ_eq_sum_choose Nat.fib_succ_eq_sum_choose