obtain ⟨q, hq⟩ := q
case mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
q : ℕ+
p : ℕ
hp : 0 < p
hpq : f ⟨p, hp⟩ = f q
h1 : f^[2] ⟨p, hp⟩ = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] q
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f q)] q
h4 : ⟨p, hp⟩ ^ 2 = q ^ 2
⊢ ⟨p, hp⟩ = q
case mk.mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ⟨p, hp⟩ ^ 2 = ⟨q, hq⟩ ^ 2
⊢ ⟨p, hp⟩ = ⟨q, hq⟩