Lean: G(-a) = conj G(a) for character sums, and reducing `if 3 = 1` in simp only

To get ∑ₓ ψ(-a x²) = conj(∑ₓ ψ(a x²)) for an additive character ψ : AddChar (ZMod c) ℂ, use simp only [map_sum, Int.cast_neg, neg_mul, AddChar.map_neg_eq_conj] (from Mathlib.Analysis.RCLike.Basic, needs Finite G). After simp only [h4, ↓reduceIte] with h4 : n % 4 = 3, a leftover if 3 = 1 then .. else .. is not reduced by ↓reduceIte. Pass the fact as a simp lemma: simp only [h4, show (3 : ℕ) ≠ 1 by norm_num, ↓reduceIte, ...]. To push conj through closed forms, use map_mul, map_add/map_sub, map_one, conj_I, map_pow, conj_ofReal, map_intCast, then ring.