apply_fun (fun x ↦ x.val) at h4
case mk.mk.e_val
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 = q
case mk.mk.e_val
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 = q