feat(Data/NNReal): nnabs n = n for n : ℕ (#39577)

From MeanFourier

Author: YaelDillies

Mathlib/Data/NNReal/Defs.lean

@@ -355,13 +355,15 @@ theorem mk_natCast (n : ℕ) : NNReal.mk (n : ℝ) (n.cast_nonneg) = n :=
   NNReal.eq (NNReal.coe_natCast n).symm
 
 @[simp]
-theorem _root_.Real.toNNReal_coe_nat (n : ℕ) : Real.toNNReal n = n :=
+theorem _root_.Real.toNNReal_natCast (n : ℕ) : Real.toNNReal n = n :=
   NNReal.eq <| by simp [Real.coe_toNNReal]
 
+@[deprecated (since := "2026-05-19")] alias _root_.Real.toNNReal_coe_nat := Real.toNNReal_natCast
+
 @[simp]
 theorem _root_.Real.toNNReal_ofNat (n : ℕ) [n.AtLeastTwo] :
     Real.toNNReal ofNat(n) = OfNat.ofNat n :=
-  Real.toNNReal_coe_nat n
+  Real.toNNReal_natCast n
 
 /-- `Real.toNNReal` and `NNReal.toReal : ℝ≥0 → ℝ` form a Galois insertion. -/
 def gi : GaloisInsertion Real.toNNReal (↑) :=
@@ -910,6 +912,9 @@ theorem coe_toNNReal_le (x : ℝ) : (toNNReal x : ℝ) ≤ |x| :=
 
 @[simp] lemma toNNReal_abs (x : ℝ) : |x|.toNNReal = nnabs x := NNReal.coe_injective <| by simp
 
+@[simp high] lemma nnabs_natCast (n : ℕ) : nnabs n = n := by simp
+@[simp high] lemma nnabs_ofNat (n : ℕ) [n.AtLeastTwo] : nnabs ofNat(n) = ofNat(n) := by simp
+
 theorem cast_natAbs_eq_nnabs_cast (n : ℤ) : (n.natAbs : ℝ≥0) = nnabs n := by
   ext
   rw [NNReal.coe_natCast, Nat.cast_natAbs, Real.coe_nnabs, Int.cast_abs]