Formalize finite implications from 3342

[vlad902]

Two small notes to the reviewers:

• This is my first time using \lean and \leanok in the blueprint, it seems straightforward but please check that I'm using it correctly.
• Finite.fn_eventually_periodic (and maybe fn_periodic) will probably be moved to somewhere common for use in #809, I included it with the proofs for 3342 for now since I'm not done with that proof yet and not sure what it will look like in the end.

[madvorak]

Congratulations!

[vlad902]

Thank you for the feedback!

[madvorak]

LGTM, somebody just check the leanok which I don't know how to use either.

[pitmonticone]

Thank you @vlad902. Please adopt the following template:

\begin{latex_decl}[Name] \label{label} \lean{lean_decl} \leanok
  text
\end{latex_decl}

\begin{proof} \uses{list_of_labels} \leanok 
  text
\end{proof}

[vlad902]

I've made the mentioned updates but I've been stuck making the build work. My limited understanding is that the recent mathlib/lean bump is responsible for it, but I don't fully understand it. Previously, e.g. in the following example:

example {G : Type*} [Finite G] (f : G → G) : False := by
  obtain ⟨p₁, p₂, ne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (Nat.iterate f ·)

[Finite G -> G] was automatically synthesized, and now it's not. Perhaps this is due to lean4#6024 (EDIT: The lean version hasn't actually been updated, so it's not this), I'm trying to debug.

[vlad902]

The cause was much more prosaic: I believe mathlib 9a9cb1894400637ebac1c1c8ac2702c23412ee5e simply split some imports I was previously transitively depending on, and I no longer imported the instance I needed.