chore: ofNat lemmas for Complex.normSq and abs (#7975)

Having `_ofNat` lemmas is important for confluence given that for both `normSq` and `abs`, the `_ofReal` lemma is `@[simp]` and so is `ofReal_ofNat`. We already have lemmas for 0 and 1 from the bundled classes for both functions, so I'm only adding lemmas for the `AtLeastTwo` case here.

Author: timotree3

Mathlib/Analysis/Complex/Basic.lean

@@ -158,7 +158,7 @@ theorem norm_rat (r : ℚ) : ‖(r : ℂ)‖ = |(r : ℝ)| := by
 
 @[simp 1100]
 theorem norm_nat (n : ℕ) : ‖(n : ℂ)‖ = n :=
-  abs_of_nat _
+  abs_natCast _
 #align complex.norm_nat Complex.norm_nat
 
 @[simp 1100]

Mathlib/Data/Complex/Basic.lean

@@ -638,6 +638,11 @@ theorem normSq_one : normSq 1 = 1 :=
   normSq.map_one
 #align complex.norm_sq_one Complex.normSq_one
 
+@[simp]
+theorem normSq_ofNat (n : ℕ) [n.AtLeastTwo] :
+    normSq (no_index (OfNat.ofNat n : ℂ)) = OfNat.ofNat n * OfNat.ofNat n := by
+  simp [normSq]
+
 @[simp]
 theorem normSq_I : normSq I = 1 := by simp [normSq]
 set_option linter.uppercaseLean3 false in
@@ -990,11 +995,13 @@ nonrec theorem abs_of_nonneg {r : ℝ} (h : 0 ≤ r) : Complex.abs r = r :=
   (Complex.abs_ofReal _).trans (abs_of_nonneg h)
 #align complex.abs_of_nonneg Complex.abs_of_nonneg
 
-theorem abs_of_nat (n : ℕ) : Complex.abs n = n :=
-  calc
-    Complex.abs n = Complex.abs (n : ℝ) := by rw [ofReal_nat_cast]
-    _ = _ := Complex.abs_of_nonneg (Nat.cast_nonneg n)
-#align complex.abs_of_nat Complex.abs_of_nat
+theorem abs_natCast (n : ℕ) : Complex.abs n = n := Complex.abs_of_nonneg (Nat.cast_nonneg n)
+#align complex.abs_of_nat Complex.abs_natCast
+
+@[simp]
+theorem abs_ofNat (n : ℕ) [n.AtLeastTwo] :
+    Complex.abs (no_index (OfNat.ofNat n : ℂ)) = OfNat.ofNat n :=
+  abs_natCast n
 
 theorem mul_self_abs (z : ℂ) : Complex.abs z * Complex.abs z = normSq z :=
   Real.mul_self_sqrt (normSq_nonneg _)
@@ -1019,11 +1026,7 @@ theorem abs_I : Complex.abs I = 1 := by simp [Complex.abs]
 set_option linter.uppercaseLean3 false in
 #align complex.abs_I Complex.abs_I
 
-@[simp]
-theorem abs_two : Complex.abs 2 = 2 :=
-  calc
-    Complex.abs 2 = Complex.abs (2 : ℝ) := rfl
-    _ = (2 : ℝ) := Complex.abs_of_nonneg (by norm_num)
+theorem abs_two : Complex.abs 2 = 2 := abs_ofNat 2
 #align complex.abs_two Complex.abs_two
 
 @[simp]

Mathlib/NumberTheory/LSeries.lean

@@ -117,7 +117,7 @@ theorem zeta_LSeriesSummable_iff_one_lt_re {z : ℂ} : LSeriesSummable ζ z ↔
     · simp [h0]
     simp only [cast_zero, natCoe_apply, zeta_apply, succ_ne_zero, if_false, cast_succ, one_div,
       Complex.norm_eq_abs, map_inv₀, Complex.abs_cpow_real, inv_inj, zero_add]
-    rw [← cast_one, ← cast_add, Complex.abs_of_nat, cast_add, cast_one]
+    rw [← cast_one, ← cast_add, Complex.abs_natCast, cast_add, cast_one]
 #align nat.arithmetic_function.zeta_l_series_summable_iff_one_lt_re Nat.ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re
 
 @[simp]