chore: golf using grind and add grind annotation

Author: euprunin

Mathlib/NumberTheory/LucasLehmer.lean

@@ -642,14 +642,7 @@ theorem sModNat_eq_sMod (p k : ℕ) (hp : 2 ≤ p) : (sModNat (2 ^ p - 1) k : 
     simp [h2]
   | succ k ih =>
     rw [sModNat, sMod, ← ih]
-    have h3 : 2 ≤ 2 ^ p - 1 := by
-      zify [h2]
-      calc (2 : ℤ)
-        _ ≤ 4 - 1 := by simp
-        _ ≤ 2 ^ p - 1 := by zify at h1; exact Int.sub_le_sub_right h1 _
-    zify [h2, h3]
-    rw [← add_sub_assoc, sub_eq_add_neg, add_assoc, add_comm _ (-2), ← add_assoc,
-      Int.add_emod_right, ← sub_eq_add_neg]
+    grind [Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.add_emod, Int.emod_eq_add_self_emod]
 
 /-- Tail-recursive version of `sModNat`. -/
 meta def sModNatTR (q k : ℕ) : ℕ :=