feat(algebra/group_power): int.nat_abs_pow_two (#2811)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

src/algebra/group_power.lean

@@ -671,6 +671,9 @@ lemma units_pow_two (u : units ℤ) : u ^ 2 = 1 :=
 lemma units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) : u ^ n = u ^ (n % 2) :=
 by conv {to_lhs, rw ← nat.mod_add_div n 2}; rw [pow_add, pow_mul, units_pow_two, one_pow, mul_one]
 
+@[simp] lemma nat_abs_pow_two (x : ℤ) : (x.nat_abs ^ 2 : ℤ) = x ^ 2 :=
+by rw [pow_two, int.nat_abs_mul_self', pow_two]
+
 end int
 
 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=

src/number_theory/sum_four_squares.lean

@@ -48,8 +48,8 @@ have hk0 : 0 ≤ k, from nonneg_of_mul_nonneg_left
     by rw [hk, int.nat_abs_of_nonneg hk0, mul_comm],
   lt_of_mul_lt_mul_left
     (calc p * k.nat_abs = a.val_min_abs.nat_abs ^ 2 + b.val_min_abs.nat_abs ^ 2 + 1 :
-        by rw [← int.coe_nat_inj', int.coe_nat_add, int.coe_nat_add, nat.pow_two, nat.pow_two,
-          int.nat_abs_mul_self, int.nat_abs_mul_self, ← _root_.pow_two, ← _root_.pow_two,
+        by rw [← int.coe_nat_inj', int.coe_nat_add, int.coe_nat_add, int.coe_nat_pow,
+          int.coe_nat_pow, int.nat_abs_pow_two, int.nat_abs_pow_two,
           int.coe_nat_one, hk, int.coe_nat_mul, int.nat_abs_of_nonneg hk0]
       ... ≤ (p / 2) ^ 2 + (p / 2)^2 + 1 :
         add_le_add
@@ -206,8 +206,8 @@ let ⟨w, x, y, z, h₂⟩ := sum_four_squares (n / min_fac n) in
  (a * w + b * x + c * y + d * z).nat_abs,
   begin
     rw [← int.coe_nat_inj', ← nat.mul_div_cancel' (min_fac_dvd (k+2)), int.coe_nat_mul, ← h₁, ← h₂],
-    simp [nat.pow_two, int.coe_nat_add, int.nat_abs_mul_self'],
-    ring,
+    simp,
+    ring
   end⟩
 
 end nat