refine ⟨p, ?_, k, ?_, ?_⟩
case neg.h
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
hk : ¬k = 1
⊢ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
case neg.h.refine_1
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
hk : ¬k = 1
⊢ ↑p < √↑N

case neg.h.refine_2
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
hk : ¬k = 1
⊢ k ≤ Nat.log 2 N

case neg.h.refine_3
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
hk : ¬k = 1
⊢ n = p ^ k