Lean/Mathlib: injecting characters mod q into (conductor, primitive char) pairs

To bound a sum over non-principal χ : DirichletCharacter ℂ q by a sum over d | q, d > 1, and primitive ψ mod d, map s χ := (⟨χ.conductor, χ.primitiveCharacter⟩ : Σ d, DirichletCharacter ℂ d). Injectivity: define G x := if h : x.1 ∣ q then changeLevel h x.2 else 1. Then G (s χ) = χ by dite_eq_left χ.conductor_dvd_level plus changeLevel_primitiveCharacter, so you never need HEq on sigma components. Then use sum_image (with the InjOn), sum_le_sum_of_subset_of_nonneg into s.sigma t, and Finset.sum_sigma. conductor > 1 comes from eq_one_iff_conductor_eq_one (no explicit args) and conductor_ne_zero. For n coprime to q, changeLevel_eq_cast_of_dvd' needs IsCoprime (n:ℤ) q (Nat.isCoprime_iff_coprime) and leaves an Int.cast_natCast to simp away.