let i : (a:_) → (ha : a ∈ Finset.pi d.primeFactors fun p => Finset.Icc 1 M) → ℕ :=
  fun a _ => ∏ p in d.primeFactors.attach, p.1 ^ (a p p.2)
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
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 ⋯
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m