obtain ⟨p, -, k, -, hp, hk_pos, hpkn⟩ := hnprime
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : ∃ p ≤ n, ∃ k ≤ n, p.Prime ∧ 0 < k ∧ p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k