Lean: Möbius-free reduction of character sums to primitive characters

To pass from an interval bound for a primitive Dirichlet character ψ to sums restricted to n coprime to r (the imprimitive case), avoid ArithmeticFunction.moebius. Do strong induction on r: take p = r.minFac, write r = p^e * s with p ∤ s (Nat.exists_eq_pow_mul_and_not_dvd), split the coprime-to-s filter by p ∣ n (sum_filter_not_add_sum_filter), and turn the multiples of p in Ico a b into Ico (a ⌈/⌉ p) (b ⌈/⌉ p) via sum_nbij' (p * ·) (· / p) using Nat.ceilDiv_le_iff_le_mul (and its negation for the upper end). The bound becomes 2^#{p ∈ r.primeFactors | ¬p ∣ q} * B, and primes dividing the modulus cost nothing since ψ p = 0. Gotchas: rw [Nat.coprime_mul_iff_left] inside an if fails with a Decidable motive error, use simp only; primeFactors (p^e*s) = insert p s.primeFactors via Nat.primeFactors_mul + Nat.primeFactors_prime_pow.