BrunTitchmarsh.prime_or_pow

theorem prime_or_pow (N n : ℕ) (hnN : n < N) (hnprime : IsPrimePow n) :    Nat.Prime n ∨ (∃ (m : ℕ), m < Real.sqrt N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k) := by  rw [isPrimePow_nat_iff_bounded n] at hnprime  obtain ⟨p, -, k, -, hp, hk_pos, hpkn⟩ := hnprime  by_cases hk : k = 1  · left    rw [← hpkn, hk, pow_one]    exact hp  right  refine ⟨p, ?_, k, ?_, ?_⟩  · rw [Real.lt_sqrt]    · norm_cast      calc        p ^ 2 ≤ p ^ k := by gcongr <;> [exact hp.one_le; omega]      _ = n := hpkn      _ < N := hnN    · positivity  · calc      _ ≤ Nat.log p n := Nat.le_log_of_pow_le hp.one_lt hpkn.le      _ ≤ Nat.log 2 n := Nat.log_anti_left (by norm_num) hp.two_le      _ ≤ Nat.log 2 N := Nat.log_mono_right hnN.le  · exact_mod_cast hpkn.symm