Lean/Mathlib: evaluating a character sum over a small ZMod without knowing the character

To pin down an abstract real character χ mod 15 on [0, 8): simp only [show (15+1)/2 = 8 by norm_num, Finset.sum_range_succ, Finset.range_zero, Finset.sum_empty] expands the sum; non-units vanish via χ.map_nonunit with (ZMod.isUnit_iff_coprime a 15) and by decide on ¬ Nat.Coprime a 15; IsUnit (2 : ZMod 15) is by decide. Express other values multiplicatively: rewrite χ 7 = χ (-1 * (2 * (2 * 2))) by rw [← map_mul ...] then congr 1 (the ZMod 15 identity closes by rfl/decide automatically; a trailing decide then errors with 'No goals'). Note decide cannot be used on goals containing free variables like χ: first reduce to a closed ZMod equation. In a public module, prefer local instance : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩ to avoid exporting duplicate Fact instances.