chore: use mk_pow to simply proof of frobenius_mk (#11024)

Uses `mk_pow`, which was recently introduced in #10282, to simplify the proof of `frobenius_mk`.

After this change, I observe the time reported by `trace.profiler` to drop from 0.10 to 0.035 seconds on this theorem.

Mathlib/FieldTheory/PerfectClosure.lean

@@ -393,17 +393,7 @@ theorem frobenius_mk (x : ℕ × K) :
     (frobenius (PerfectClosure K p) p : PerfectClosure K p → PerfectClosure K p) (mk K p x) =
       mk _ _ (x.1, x.2 ^ p) := by
   simp only [frobenius_def]
-  cases' x with n x
-  dsimp only
-  suffices ∀ p' : ℕ, mk K p (n, x) ^ p' = mk K p (n, x ^ p') by apply this
-  intro p
-  induction p with
-  | zero => apply R.sound; rw [(frobenius _ _).iterate_map_one, pow_zero]
-  | succ p ih =>
-    rw [pow_succ, ih]
-    symm
-    apply R.sound
-    simp only [pow_succ, iterate_map_mul]
+  exact mk_pow K p x p
 #align perfect_closure.frobenius_mk PerfectClosure.frobenius_mk
 
 /-- Embedding of `K` into `PerfectClosure K p` -/