rcases prime_or_pow N n hnN hnprime with hp | ⟨m, hm, k, hk, h⟩
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
case inl
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
hp : n.Prime
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n

case inr.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n