refactor(ring_theory/perfection): faster proof of coeff_frobenius (#…

…6159)

4X smaller proof term, elaboration 800ms -> 50ms

Co-authors: `lean-gptf`, Stanislas Polu

Note: supplying `coeff_pow_p f n` also works but takes 500ms to
elaborate


Co-authored-by: Jesse Michael Han <39395247+jesse-michael-han@users.noreply.github.com>

src/ring_theory/perfection.lean

@@ -92,7 +92,7 @@ f.2 n
 
 lemma coeff_frobenius (f : ring.perfection R p) (n : ℕ) :
   coeff R p (n + 1) (frobenius _ p f) = coeff R p n f :=
-by convert coeff_pow_p f n
+by apply coeff_pow_p f n -- `coeff_pow_p f n` also works but is slow!
 
 lemma coeff_iterate_frobenius (f : ring.perfection R p) (n m : ℕ) :
   coeff R p (n + m) (frobenius _ p ^[m] f) = coeff R p n f :=