apply Nat.minFac_le h.pos
case pos.hxy.h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
a✝ : i ∈ Finset.range n
h : IsPrimePow i
this : 0 < i.minFac
⊢ i.minFac ≤ i
no goals