SelbergSieve.sum_mul_subst

lemma sum_mul_subst (k n : ℕ) {f : ℕ → ℝ} (h : ∀ l, l ∣ n → ¬ k ∣ l → f l = 0) :      ∑ l ∈ n.divisors, f l    = ∑ m ∈ n.divisors, if k*m ∣ n then f (k*m) else 0 := by  by_cases hn: n = 0  · simp [hn]  by_cases hkn : k ∣ n  swap  · rw [sum_eq_zero, sum_eq_zero]    · rintro m _      rw [if_neg]      rintro h      apply hkn      exact (Nat.dvd_mul_right k m).trans h    · intro l hl; apply h l (dvd_of_mem_divisors hl)      apply fun hkl => hkn <| hkl.trans (dvd_of_mem_divisors hl)  trans (∑ l ∈ n.divisors, ∑ m ∈ n.divisors, if l=k*m then f l else 0)  · rw [sum_congr rfl]; intro l hl    by_cases hkl : k ∣ l    swap    · rw [h l (dvd_of_mem_divisors hl) hkl, sum_eq_zero];      intro m _; rw [ite_id]    rw [sum_eq_single (l/k)]    · rw[if_pos]; rw [Nat.mul_div_cancel' hkl]    · intro m _ hmlk      apply if_neg; revert hmlk; contrapose!; intro hlkm      rw [hlkm, mul_comm, Nat.mul_div_cancel];      apply Nat.pos_of_dvd_of_pos hkn (Nat.pos_of_ne_zero hn)    · contrapose!; intro _      rw [mem_divisors]      exact ⟨Trans.trans (Nat.div_dvd_of_dvd hkl) (dvd_of_mem_divisors hl), hn⟩  · rw [sum_comm, sum_congr rfl]; intro m _    split_ifs with hdvd    · rw [sum_ite_eq_of_mem']      simp only [mem_divisors, hdvd, ne_eq, hn, not_false_eq_true, and_self]    · apply sum_eq_zero; intro l hl      apply if_neg;      rintro rfl      simp only [mem_divisors, ne_eq] at hl      exact hdvd hl.1