gcongr with p hp
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
⊢ ∏ p ∈ d.primeFactors, f p / (1 - f p) ≥ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f 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

case h1
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
p : ℕ
hp : p ∈ d.primeFactors
⊢ ∑ n ∈ Finset.Icc 1 M, f p ^ n ≤ f p / (1 - f p)