have h1 : f^[2] p = f^[2] q := by
  apply_fun f at hpq
  exact hpq
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
⊢ p = q
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
⊢ p = q