Lean: generalizing a legendreSym-specific sum proof to any real Dirichlet character

To port a proof written for legendreSym p : ℤ → ℤ to a real character χ mod composite N, define the integer-valued g x := χ.intVal (x : ZMod N) (intVal = if χ j = 1 then 1 else if χ j = -1 then -1 else 0) and prove only the facts the old proof used: g 0 = 0, g (N - x) = -g x (oddness), g (2x) = g 2 * g x (multiplicativity, via casting (intVal a : ℂ) = χ a and exact_mod_cast), g 2 ^ 2 = 1. Then the old body ports by textual substitution: legendreSym p ↦ g, legendreSym.mul ↦ the multiplicativity lemma (direction flips: the old ← legendreSym.mul becomes a forward rw [hmul2]), range p ↦ range N. Gotcha: (2 : ℤ) cast into ZMod N shows up as ↑2, so rcases ... with h | h <;> push_cast at h before simp; and a goal that rw already closes by rfl makes a following push_cast fail with 'No goals'.