chore(Data/Nat/Bitwise) deprecate upstreamed lemma 'bitwise_lt' (#20284)

Replaces `bitwise_lt` with a deprecated alias to [`bitwise_lt_two_pow`](https://github.com/leanprover/lean4/blob/fe45ddd6105078a0a3bd855e5d94673e794f6b88/src/Init/Data/Nat/Bitwise/Lemmas.lean#L428-L453), which was added to core in leanprover/lean4@ca94124.

Found by [`tryAtEachStep`](https://github.com/dwrensha/tryAtEachStep).

Author: dwrensha

Mathlib/Data/Nat/Bitwise.lean

@@ -368,29 +368,15 @@ theorem even_xor {m n : ℕ} : Even (m ^^^ n) ↔ (Even m ↔ Even n) := by
 @[simp] theorem bit_lt_two_pow_succ_iff {b x n} : bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n := by
   cases b <;> simp <;> omega
 
-/-- If `x` and `y` fit within `n` bits, then the result of any bitwise operation on `x` and `y` also
-fits within `n` bits -/
-theorem bitwise_lt {f x y n} (hx : x < 2 ^ n) (hy : y < 2 ^ n) :
-    bitwise f x y < 2 ^ n := by
-  induction x using Nat.binaryRec' generalizing n y with
-  | z =>
-    simp only [bitwise_zero_left]
-    split <;> assumption
-  | @f bx nx hnx ih =>
-    cases y using Nat.binaryRec' with
-    | z =>
-      simp only [bitwise_zero_right]
-      split <;> assumption
-    | f «by» ny hny =>
-      rw [bitwise_bit' _ _ _ _ hnx hny]
-      cases n <;> simp_all
+@[deprecated bitwise_lt_two_pow (since := "2024-12-28")]
+alias bitwise_lt := bitwise_lt_two_pow
 
 lemma shiftLeft_lt {x n m : ℕ} (h : x < 2 ^ n) : x <<< m < 2 ^ (n + m) := by
   simp only [Nat.pow_add, shiftLeft_eq, Nat.mul_lt_mul_right (Nat.two_pow_pos _), h]
 
 /-- Note that the LHS is the expression used within `Std.BitVec.append`, hence the name. -/
 lemma append_lt {x y n m} (hx : x < 2 ^ n) (hy : y < 2 ^ m) : y <<< n ||| x < 2 ^ (n + m) := by
-  apply bitwise_lt
+  apply bitwise_lt_two_pow
   · rw [add_comm]; apply shiftLeft_lt hy
   · apply lt_of_lt_of_le hx <| Nat.pow_le_pow_right (le_succ _) (le_add_right _ _)