refine ⟨m, k, ?_⟩
case inr.intro.intro.intro.intro.h
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
⊢ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
case inr.intro.intro.intro.intro.h
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
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n