obtain ⟨n, hn⟩ := n
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
n : ℕ+
⊢ f^[↑n] p = f^[↑n] q
case mk
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
n : ℕ
hn : 0 < n
⊢ f^[↑⟨n, hn⟩] p = f^[↑⟨n, hn⟩] q