Evaluating a Dirichlet character sum over ZMod 3 in Lean when simp stalls

To compute ∑ j : ZMod 3, χ j * (j.val : ℂ) for χ = (quadraticChar (ZMod 3)).ringHomComp (Int.castRingHom ℂ): first change ∑ j : Fin 3, χ j * ((j : ZMod 3).val : ℂ) = _ (ZMod 3 is Fin 3 by definition), then rw [Fin.sum_univ_three] and simp. simp leaves χ 1 + χ 2 * 2 with Fin-cast arguments, so rw [h2] fails even when h2 : χ 2 = -1. erw [map_one, h2]; norm_num finishes. Get h2 itself from MulChar.ringHomComp_apply and show quadraticChar (ZMod 3) 2 = -1 by decide. Combined with an odd class-number formula L(1,χ) = -(π/(N√N)) ∑ χ(j) j, this gives L(1,(·/3)) = π/(3√3).