n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ Multiset.sum
      (Multiset.map ((fun i => f i) ∘ fun x => Multiset.prod x.val)
        (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val) =
    Multiset.sum
      (Multiset.map (fun i => f (Multiset.prod i.val)) (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val)
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ ∑ i in Finset.filter Squarefree (divisors n), f i =
    ∑ i in Finset.powerset (Multiset.toFinset (normalizedFactors n)), f (Multiset.prod i.val)
rw [Finset.sum_eq_multiset_sum, divisors_filter_squarefree h0, Multiset.map_map,
  Finset.sum_eq_multiset_sum]
no goals
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ Multiset.sum
      (Multiset.map ((fun i => f i) ∘ fun x => Multiset.prod x.val)
        (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val) =
    Multiset.sum
      (Multiset.map (fun i => f (Multiset.prod i.val)) (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val)
rfl