chore(RingTheory/RootsOfUnity/Complex): golf using grind

Author: SnirBroshi

Mathlib/RingTheory/RootsOfUnity/Complex.lean

@@ -55,25 +55,21 @@ theorem isPrimitiveRoot_exp_two_rat (q : ℚ) : IsPrimitiveRoot (exp (2 * π * I
 theorem isPrimitiveRoot_exp_rat_of_even_num (q : ℚ) (h : Even q.num) :
     IsPrimitiveRoot (exp (π * I * q)) q.den := by
   have ⟨n, hn⟩ := even_iff_exists_two_nsmul _ |>.mp h
-  convert isPrimitiveRoot_exp_two_rat (n / q.den : ℚ) using 1
-  · nth_rw 1 [← q.num_div_den]
-    simp [hn]
-    ring_nf
+  convert isPrimitiveRoot_exp_two_rat (n / q.den) using 1
+  · nth_rw 1 [← q.num_div_den, hn]
+    grind [Rat.cast_mul, Rat.cast_ofNat]
   · rw [← Int.cast_natCast, ← Rat.divInt_eq_div, ← Rat.mk_eq_divInt _ _ (by simp) ?_]
-    refine Nat.Coprime.coprime_mul_left (k := 2) ?_
-    convert q.reduced
-    grind
+    apply Nat.Coprime.coprime_mul_left (k := 2)
+    grind [Rat.reduced]
 
 theorem isPrimitiveRoot_exp_rat_of_odd_num (q : ℚ) (h : Odd q.num) :
     IsPrimitiveRoot (exp (π * I * q)) (2 * q.den) := by
   convert isPrimitiveRoot_exp_two_rat (q / 2) using 1
-  · push_cast
-    ring_nf
+  · grind [Rat.cast_div, Rat.cast_ofNat]
   · nth_rw 2 [← q.num_div_den]
-    rw [mul_comm, div_div, ← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul]
-    rw [← Rat.divInt_eq_div, ← Nat.cast_ofNat (R := ℤ), ← Nat.cast_mul]
-    rw [← Rat.mk_eq_divInt _ _ (by simp) ?_]
-    exact Nat.Coprime.mul_right q.reduced h.natAbs.coprime_two_right
+    rw [mul_comm, div_div, ← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul,
+      ← Rat.divInt_eq_div, ← Nat.cast_ofNat (R := ℤ), ← Nat.cast_mul,
+      ← Rat.mk_eq_divInt _ _ (by simp) (Nat.Coprime.mul_right q.reduced h.natAbs.coprime_two_right)]
 
 theorem isPrimitiveRoot_exp (n : ℕ) (h0 : n ≠ 0) : IsPrimitiveRoot (exp (2 * π * I / n)) n := by
   simpa only [Nat.cast_one, one_div] using