Sieve.prod_factors_sum_pow_compMult

theorem prod_factors_sum_pow_compMult (M : ℕ) (hM : M ≠ 0) (f : ArithmeticFunction ℝ)    (hf : CompletelyMultiplicative f) (d : ℕ) (hd : Squarefree d) :    ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p^n)    = ∑ m ∈ (d^M).divisors.filter (d ∣ ·), f m := by  rw [Finset.prod_sum]  let i : (a:_) → (ha : a ∈ Finset.pi d.primeFactors fun p => Finset.Icc 1 M) → ℕ :=    fun a _ => ∏ p ∈ d.primeFactors.attach, p.1 ^ (a p p.2)  have hfact_i : ∀ a ha,      ∀ p , Nat.factorization (i a ha) p = if hp : p ∈ d.primeFactors then a p hp else 0 := by    intro a ha p    by_cases hp : p ∈ d.primeFactors    · rw [dif_pos hp, Nat.factorization_prod, Finset.sum_apply',        Finset.sum_eq_single ⟨p, hp⟩, Nat.factorization_pow, Finsupp.smul_apply,        Nat.Prime.factorization_self (Nat.prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp)]      · ring      · intro q _ hq        rw [Nat.factorization_pow, Finsupp.smul_apply, smul_eq_zero]; right        apply Nat.factorization_eq_zero_of_not_dvd        rw [Nat.Prime.dvd_iff_eq, ← exists_eq_subtype_mk_iff]        · push Not          exact fun _ => hq        · exact Nat.prime_of_mem_primeFactorsList <| List.mem_toFinset.mp q.2        · exact (Nat.prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp).ne_one      · intro h        exfalso        exact h (Finset.mem_attach _ _)      · exact fun q _ => pow_ne_zero _ (ne_of_gt (Nat.pos_of_mem_primeFactorsList          (List.mem_toFinset.mp q.2)))    · rw [dif_neg hp]      by_cases hpp : p.Prime      swap      · apply Nat.factorization_eq_zero_of_not_prime _ hpp      apply Nat.factorization_eq_zero_of_not_dvd      intro hp_dvd      obtain ⟨⟨q, hq⟩, _, hp_dvd_pow⟩ := Prime.exists_mem_finset_dvd hpp.prime hp_dvd      apply hp      rw [Nat.mem_primeFactors]      constructor      · exact hpp      refine ⟨?_, hd.ne_zero⟩      trans q      · apply Nat.Prime.dvd_of_dvd_pow hpp hp_dvd_pow      · apply Nat.dvd_of_mem_primeFactorsList <| List.mem_toFinset.mp hq   have hi_ne_zero : ∀ (a : _) (ha : a ∈ Finset.pi d.primeFactors fun _p => Finset.Icc 1 M),      i a ha ≠ 0 := by    intro a ha    erw [Finset.prod_ne_zero_iff]    exact fun p _ => pow_ne_zero _ (ne_of_gt (Nat.pos_of_mem_primeFactorsList      (List.mem_toFinset.mp p.property)))  have hi : ∀ (a : _) (ha : a ∈ Finset.pi d.primeFactors fun _p => Finset.Icc 1 M),      i a ha ∈ (d^M).divisors.filter (d ∣ ·) := by    intro a ha    rw [Finset.mem_filter, Nat.mem_divisors, ←Nat.factorization_le_iff_dvd hd.ne_zero      (hi_ne_zero a ha),← Nat.factorization_le_iff_dvd (hi_ne_zero a ha) (pow_ne_zero _ hd.ne_zero)]    constructor; constructor    · rw [Finsupp.le_iff]; intro p _      rw [hfact_i a ha]      by_cases hp : p ∈ d.primeFactors      · rw [dif_pos hp]        rw [Nat.factorization_pow, Finsupp.smul_apply]        simp_rw [Finset.mem_pi, Finset.mem_Icc] at ha        trans (M • 1)        · norm_num          exact (ha p hp).2        · gcongr          rw [Nat.mem_primeFactors_of_ne_zero hd.ne_zero] at hp          rw [←Nat.Prime.dvd_iff_one_le_factorization hp.1 hd.ne_zero]          exact hp.2      · rw [dif_neg hp]; norm_num    · apply pow_ne_zero _ hd.ne_zero    · rw [Finsupp.le_iff]; intro p hp      rw [Nat.support_factorization] at hp      rw [hfact_i a ha]      rw [dif_pos hp]      trans 1      · exact hd.natFactorization_le_one p      simp_rw [Finset.mem_pi, Finset.mem_Icc] at ha      exact (ha p hp).1   have h : ∀ (a : _) (ha : a ∈ Finset.pi d.primeFactors fun _p => Finset.Icc 1 M),      ∏ p ∈ d.primeFactors.attach, f (p.1 ^ (a p p.2)) = f (i a ha) := by    intro a ha    apply symm    apply hf.isMultiplicative.map_prod    intro x _ y _ hxy    simp_rw [Finset.mem_pi, Finset.mem_Icc, Nat.succ_le_iff] at ha    apply (Nat.coprime_pow_left_iff (ha x x.2).1 ..).mpr    apply (Nat.coprime_pow_right_iff (ha y y.2).1 ..).mpr    have hxp := Nat.prime_of_mem_primeFactorsList (List.mem_toFinset.mp x.2)    rw [Nat.Prime.coprime_iff_not_dvd hxp]    rw [Nat.prime_dvd_prime_iff_eq hxp <| Nat.prime_of_mem_primeFactorsList      (List.mem_toFinset.mp y.2)]    exact fun hc => hxy (Subtype.ext hc)   have i_inj : ∀ a ha b hb, i a ha = i b hb → a = b := by    intro a ha b hb hiab    apply_fun Nat.factorization at hiab    ext p hp    obtain hiabp := DFunLike.ext_iff.mp hiab p    rw [hfact_i a ha, hfact_i b hb, dif_pos hp, dif_pos hp] at hiabp    exact hiabp   have i_surj : ∀ (b : ℕ), b ∈ (d^M).divisors.filter (d ∣ ·) → ∃ a ha, i a ha = b := by    intro b hb    have h : (fun p _ => b.factorization p) ∈ Finset.pi d.primeFactors fun p => Finset.Icc 1 M := by      rw [Finset.mem_pi]; intro p hp      rw [Finset.mem_Icc]      rw [Finset.mem_filter] at hb      have hb_ne_zero : b ≠ 0 := ne_of_gt <| Nat.pos_of_mem_divisors hb.1      have hpp : p.Prime := Nat.prime_of_mem_primeFactors hp      constructor      · rw [←Nat.Prime.dvd_iff_one_le_factorization hpp hb_ne_zero]        · exact Trans.trans (Nat.dvd_of_mem_primeFactors hp) hb.2      · rw [Nat.mem_divisors] at hb        trans Nat.factorization (d^M) p        · exact (Nat.factorization_le_iff_dvd hb_ne_zero hb.left.right).mpr hb.left.left p        rw [Nat.factorization_pow, Finsupp.smul_apply, smul_eq_mul]        have : d.factorization p ≤ 1 := by          apply hd.natFactorization_le_one        exact (mul_le_iff_le_one_right (Nat.pos_of_ne_zero hM)).mpr this    use (fun p _ => Nat.factorization b p)    use h    apply Nat.eq_of_factorization_eq    · apply hi_ne_zero _ h    · exact ne_of_gt <| Nat.pos_of_mem_divisors (Finset.mem_filter.mp hb).1    intro p    rw [hfact_i (fun p _ => (Nat.factorization b) p) h p]    rw [Finset.mem_filter, Nat.mem_divisors] at hb    by_cases hp : p ∈ d.primeFactors    · rw [dif_pos hp]    · rw [dif_neg hp, eq_comm, Nat.factorization_eq_zero_iff, ←or_assoc]      rw [Nat.mem_primeFactors] at hp      left      push Not at hp      by_cases hpp : p.Prime      · right; intro h        apply absurd (hp hpp)        push Not        exact ⟨hpp.dvd_of_dvd_pow (h.trans hb.1.1), hd.ne_zero⟩      · left; exact hpp   exact Finset.sum_bij i hi i_inj i_surj h