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

Adds  in a new file  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.lean

@@ -20,6 +20,7 @@ public import Init.Data.Nat.Power2
 public import Init.Data.Nat.Linear
 public import Init.Data.Nat.SOM
 public import Init.Data.Nat.Lemmas
+public import Init.Data.Nat.Cast
 public import Init.Data.Nat.Mod
 public import Init.Data.Nat.Lcm
 public import Init.Data.Nat.Compare

src/Init/Data/Nat/Cast.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+public import Init.Data.Cast
+public import Init.Data.Nat.Lemmas
+
+public section
+
+namespace Nat
+
+@[simp, norm_cast, grind =] theorem cast_id (n : Nat) : Nat.cast n = n := rfl
+
+end Nat