exact fun p _ => Finset.sum_nonneg fun n _ => pow_nonneg (hf_nonneg p) n
case h0
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ ∀ i ∈ d.primeFactors, 0 ≤ ∑ n ∈ Finset.Icc 1 M, f i ^ n
no goals