apply Nat.factorization_eq_zero_of_not_dvd
case pos
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∉ d.primeFactors
hpp : p.Prime
⊢ (i a ha).factorization p = 0
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∉ d.primeFactors
hpp : p.Prime
⊢ ¬p ∣ i a ha