have h4 :=
  calc p^2
    = f^[f p] p * f^[2] p := (hf p).symm
  _ = f^[f q] q * f^[2] q := by rw[h3, h1]
  _ = q^2 := hf 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
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] 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
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
h4 : p ^ 2 = q ^ 2
⊢ p = q