Lean/Mathlib: Gauss sum of an induced Dirichlet character, τ = μ(q/d)χ*(q/d)τ(χ*)

Mathlib has no formula for gaussSum (changeLevel h χ*). The proof that went through, with no primitivity needed: (1) write the Gauss sum over range N via the bijection ZMod N ≃ Fin N, j ↦ j.val, plus ZMod.stdAddChar_apply and ZMod.toCircle_apply. (2) χ(n) = χ*(n)·∑_{k ∈ q.divisors, k ∣ n} μ k: the filter equals (n.gcd q).divisors, ∑_{k ∣ m} μ k = [m = 1] comes from congrArg (· m) moebius_mul_coe_zeta with coe_mul_zeta_apply, and the coprime case is changeLevel_eq_cast_of_dvd' with Nat.isCoprime_iff_coprime. (3) Swap the sums with Finset.sum_comm'. Note the argument order: s' is the dependent family and t' is a plain Finset. Then reindex n = k m via filter = (range (q/k)).map ⟨(k * ·), mul_right_injective₀ hk0⟩. (4) If χ*(k) ≠ 0 then k is coprime to d (MulChar.map_nonunit, ZMod.isUnit_iff_coprime), so d ∣ q/k. ∑_{m<dt} f(m mod d) e(m/(dt)) = 0 for t ≥ 2, by splitting m = dv + u (induction with sum_range_add) and a geometric sum of e(1/t). Use open scoped ArithmeticFunction.Moebius for μ. Also, if_pos/if_neg and ite_cond_eq_true are deprecated; use ite_eq_left_of_eq_true (eq_true h).