chore(number_theory/sum_four_squares): squeeze simps (#18461)

This proof goes from 20s to 8s. Adding a missing `norm_cast` lemma makes it possible to replace some `simp`s with `push_cast`
leanprover-community · Feb 18, 2023 · 297619e · 297619e
1 parent 2738d2c
commit 297619e
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 13 deletions.
diff --git a/src/data/zmod/basic.lean b/src/data/zmod/basic.lean
@@ -778,7 +778,7 @@ begin
   { refl }
 end
 
-@[simp] lemma coe_val_min_abs : ∀ {n : ℕ} (x : zmod n), (x.val_min_abs : zmod n) = x
+@[simp, norm_cast] lemma coe_val_min_abs : ∀ {n : ℕ} (x : zmod n), (x.val_min_abs : zmod n) = x
 | 0       x := int.cast_id x
 | k@(n+1) x :=
 begin

diff --git a/src/number_theory/sum_four_squares.lean b/src/number_theory/sum_four_squares.lean
@@ -28,7 +28,7 @@ namespace int
 
 lemma sq_add_sq_of_two_mul_sq_add_sq {m x y : ℤ} (h : 2 * m = x^2 + y^2) :
   m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2 :=
-have even (x^2 + y^2), by simp [h.symm, even_mul],
+have even (x^2 + y^2), by simp [←h, even_mul],
 have hxaddy : even (x + y), by simpa [sq] with parity_simps,
 have hxsuby : even (x - y), by simpa [sq] with parity_simps,
 (mul_right_inj' (show (2*2 : ℤ) ≠ 0, from dec_trivial)).1 $
@@ -113,15 +113,16 @@ have hm : ∃ m < p, 0 < m ∧ ∃ a b c d : ℤ, a^2 + b^2 + c^2 + d^2 = m * p,
     (λ hk0, by { rw [hk0, int.coe_nat_zero, zero_mul] at hk,
       exact ne_of_gt (show a^2 + b^2 + 1 > 0, from add_pos_of_nonneg_of_pos
         (add_nonneg (sq_nonneg _) (sq_nonneg _)) zero_lt_one) hk.1 }),
-    a, b, 1, 0, by simpa [sq] using hk.1⟩,
+    a, b, 1, 0, by simpa only [zero_pow two_pos, one_pow, add_zero] using hk.1⟩,
 let m := nat.find hm in
 let ⟨a, b, c, d, (habcd : a^2 + b^2 + c^2 + d^2 = m * p)⟩ := (nat.find_spec hm).snd.2 in
 by haveI hm0 : ne_zero m := ne_zero.of_pos (nat.find_spec hm).snd.1; exact
 have hmp : m < p, from (nat.find_spec hm).fst,
 m.mod_two_eq_zero_or_one.elim
   (λ hm2 : m % 2 = 0,
     let ⟨k, hk⟩ := nat.dvd_iff_mod_eq_zero.2 hm2 in
-    have hk0 : 0 < k, from nat.pos_of_ne_zero $ λ _, by { simp [*, lt_irrefl] at * },
+    have hk0 : 0 < k, from nat.pos_of_ne_zero $
+      by { rintro rfl, rw mul_zero at hk, exact ne_zero.ne m hk },
     have hkm : k < m, { rw [hk, two_mul], exact (lt_add_iff_pos_left _).2 hk0 },
     false.elim $ nat.find_min hm hkm ⟨lt_trans hkm hmp, hk0,
       sum_four_squares_of_two_mul_sum_four_squares
@@ -134,7 +135,7 @@ m.mod_two_eq_zero_or_one.elim
           y := (c : zmod m).val_min_abs, z := (d : zmod m).val_min_abs in
       have hnat_abs : w^2 + x^2 + y^2 + z^2 =
           (w.nat_abs^2 + x.nat_abs^2 + y.nat_abs ^2 + z.nat_abs ^ 2 : ℕ),
-        by simp [sq],
+        by { push_cast, simp_rw sq_abs, },
       have hwxyzlt : w^2 + x^2 + y^2 + z^2 < m^2,
         from calc w^2 + x^2 + y^2 + z^2
             = (w.nat_abs^2 + x.nat_abs^2 + y.nat_abs ^2 + z.nat_abs ^ 2 : ℕ) : hnat_abs
@@ -144,7 +145,8 @@ m.mod_two_eq_zero_or_one.elim
             (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _))
             (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _))
             (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _)
-        ... = 4 * (m / 2 : ℕ) ^ 2 : by simp [sq, bit0, bit1, mul_add, add_mul, add_assoc]
+        ... = 4 * (m / 2 : ℕ) ^ 2 : by simp only [bit0_mul, one_mul, two_smul,
+                                                  nat.cast_add, nat.cast_pow, add_assoc]
         ... < 4 * (m / 2 : ℕ) ^ 2 + ((4 * (m / 2) : ℕ) * (m % 2 : ℕ) + (m % 2 : ℕ)^2) :
           (lt_add_iff_pos_right _).2 (by { rw [hm2, int.coe_nat_one, one_pow, mul_one],
             exact add_pos_of_nonneg_of_pos (int.coe_nat_nonneg _) zero_lt_one })
@@ -153,16 +155,16 @@ m.mod_two_eq_zero_or_one.elim
             pow_add, add_comm, add_left_comm] },
       have hwxyzabcd : ((w^2 + x^2 + y^2 + z^2 : ℤ) : zmod m) =
           ((a^2 + b^2 + c^2 + d^2 : ℤ) : zmod m),
-        by simp [w, x, y, z, sq],
+        by push_cast,
       have hwxyz0 : ((w^2 + x^2 + y^2 + z^2 : ℤ) : zmod m) = 0,
         by rw [hwxyzabcd, habcd, int.cast_mul, cast_coe_nat, zmod.nat_cast_self, zero_mul],
       let ⟨n, hn⟩ := ((char_p.int_cast_eq_zero_iff _ m _).1 hwxyz0) in
       have hn0 : 0 < n.nat_abs, from int.nat_abs_pos_of_ne_zero (λ hn0,
         have hwxyz0 : (w.nat_abs^2 + x.nat_abs^2 + y.nat_abs^2 + z.nat_abs^2 : ℕ) = 0,
           by { rw [← int.coe_nat_eq_zero, ← hnat_abs], rwa [hn0, mul_zero] at hn },
         have habcd0 : (m : ℤ) ∣ a ∧ (m : ℤ) ∣ b ∧ (m : ℤ) ∣ c ∧ (m : ℤ) ∣ d,
-          by simpa [add_eq_zero_iff' (sq_nonneg (_ : ℤ)) (sq_nonneg _),
-            pow_two, w, x, y, z, (char_p.int_cast_eq_zero_iff _ m _), and.assoc] using hwxyz0,
+          by simpa only [add_eq_zero_iff, int.nat_abs_eq_zero, zmod.val_min_abs_eq_zero, and.assoc,
+                         pow_eq_zero_iff two_pos, char_p.int_cast_eq_zero_iff _ m _] using hwxyz0,
         let ⟨ma, hma⟩ := habcd0.1,     ⟨mb, hmb⟩ := habcd0.2.1,
             ⟨mc, hmc⟩ := habcd0.2.2.1, ⟨md, hmd⟩ := habcd0.2.2.2 in
         have hmdvdp : m ∣ p,
@@ -172,13 +174,14 @@ m.mod_two_eq_zero_or_one.elim
         (hp.1.eq_one_or_self_of_dvd _ hmdvdp).elim hm1
         (λ hmeqp, by simpa [lt_irrefl, hmeqp] using hmp)),
       have hawbxcydz : ((m : ℕ) : ℤ) ∣ a * w + b * x + c * y + d * z,
-        from (char_p.int_cast_eq_zero_iff (zmod m) m _).1 $ by { rw [← hwxyz0], simp, ring },
+        from (char_p.int_cast_eq_zero_iff (zmod m) m _).1 $
+          by { rw [← hwxyz0], simp_rw [sq], push_cast },
       have haxbwczdy : ((m : ℕ) : ℤ) ∣ a * x - b * w - c * z + d * y,
-        from (char_p.int_cast_eq_zero_iff (zmod m) m _).1 $ by { simp [sub_eq_add_neg], ring },
+        from (char_p.int_cast_eq_zero_iff (zmod m) m _).1 $ by { push_cast, ring },
       have haybzcwdx : ((m : ℕ) : ℤ) ∣ a * y + b * z - c * w - d * x,
-        from (char_p.int_cast_eq_zero_iff (zmod m) m _).1 $ by { simp [sub_eq_add_neg], ring },
+        from (char_p.int_cast_eq_zero_iff (zmod m) m _).1 $ by { push_cast, ring },
       have hazbycxdw : ((m : ℕ) : ℤ) ∣ a * z - b * y + c * x - d * w,
-        from (char_p.int_cast_eq_zero_iff (zmod m) m _).1 $ by { simp [sub_eq_add_neg], ring },
+        from (char_p.int_cast_eq_zero_iff (zmod m) m _).1 $ by { push_cast, ring },
       let ⟨s, hs⟩ := hawbxcydz, ⟨t, ht⟩ := haxbwczdy, ⟨u, hu⟩ := haybzcwdx, ⟨v, hv⟩ := hazbycxdw in
       have hn_nonneg : 0 ≤ n,
         from nonneg_of_mul_nonneg_right