import Mathlib.Data.PNat.Basic
import Mathlib.Tactic
/-!
# USA Mathematical Olympiad 2019, Problem 1
Let ℕ+ be the set of positive integers.
A function f: ℕ+ → ℕ+ satisfies the equation
fᶠ⁽ⁿ⁾(n)⬝f²(n) = n^2
for all positive integers n, where fᵏ(m) means f iterated k times on m.
Given this information, determine all possible values of f(1000).
-/
namespace Usa2019P1
snip
/- determine -/ abbrev solution_set : Set ℕ+ := sorry
theorem usa2019_p1 (m : ℕ+) :
m ∈ solution_set ↔
(∃ f : ℕ+ → ℕ+,
(∀ n, f^[f n] n * f (f n) = n ^ 2) ∧
m = f 1000) := sorry
end Usa2019P1
This problem has a complete formalized solution.