feat: add Nat.cast_id and grind attribute to Int.cast_id

Adds `Nat.cast_id` to `Init/Data/Nat/Lemmas.lean` with
`simp`, `norm_cast`, and `grind =` attributes.

Also adds `grind =` to the existing `Int.cast_id`.

🤖 Prepared with Claude Code

Co-Authored-By: Claude <[email protected]>

Author: kim-em

src/Init/Data/Int/LemmasAux.lean

@@ -62,7 +62,7 @@ theorem natCast_succ_pos (n : Nat) : 0 < (n.succ : Int) := natCast_pos.2 n.succ_
 
 @[simp high] theorem natCast_nonpos_iff {n : Nat} : (n : Int) ≤ 0 ↔ n = 0 := by omega
 
-@[simp, norm_cast] theorem cast_id {n : Int} : Int.cast n = n := rfl
+@[simp, norm_cast, grind =] theorem cast_id {n : Int} : Int.cast n = n := rfl
 
 @[simp] theorem ble'_eq_true (a b : Int) : (Int.ble' a b = true) = (a ≤ b) := by
   cases a <;> cases b <;> simp [Int.ble'] <;> omega

src/Init/Data/Nat/Lemmas.lean

@@ -12,6 +12,7 @@ public import Init.Data.Nat.Log2
 import all Init.Data.Nat.Log2
 public import Init.Data.Nat.Power2
 public import Init.Data.Nat.Mod
+public import Init.Data.Cast
 import Init.TacticsExtra
 import Init.BinderPredicates
 
@@ -1800,3 +1801,7 @@ instance decidableExistsFin (P : Fin n → Prop) [DecidablePred P] : Decidable (
   decidable_of_iff (∃ k, k < n ∧ ((h: k < n) → P ⟨k, h⟩))
     ⟨fun ⟨k, a⟩ => Exists.intro ⟨k, a.left⟩ (a.right a.left),
     fun ⟨i, e⟩ => Exists.intro i.val ⟨i.isLt, fun _ => e⟩⟩
+
+/-! ### cast -/
+
+@[simp, norm_cast, grind =] theorem cast_id (n : Nat) : Nat.cast n = n := rfl