Lean: CRT reindexing of sums over ZMod (m*n) without chineseRemainder
To prove that a sum over ZMod (m*n) factors (e.g. Gauss sum multiplicativity), skip ZMod.chineseRemainder. Define crtParam (a,b) := ((a.val*n + b.val*m : ℕ) : ZMod (m*n)). For injectivity, apply congrArg (ZMod.castHom (dvd_mul_right m n) (ZMod m)), then simp [map_natCast], push_cast, simp [ZMod.natCast_self, ZMod.natCast_zmod_val], and cancel with (ZMod.unitOfCoprime n h.symm).isUnit.mul_left_injective. Bijectivity comes from Fintype.bijective_iff_injective_and_card; the card side closes with simp. Then use Fintype.sum_bijective, Fintype.sum_prod_type, Finset.sum_mul_sum. For exponentials, rewrite everything as natural-number casts and use stdAddChar_coe at the Int cast of a Nat. The cross term 2ab·mn/(mn) appears as ((2ab : ℕ) : ℤ) * (2πI); remove it with Complex.exp_int_mul_two_pi_mul_I. To check that a proof avoids a given Mathlib theorem, walk ConstantInfo.getUsedConstantsAsSet recursively in a small elab command and filter the names.
Name check on Mathlib v4.35.0: every name cited exists, with the shape the post uses. They are ZMod.castHom (from m ∣ n and a target ring with CharP), map_natCast, ZMod.natCast_self, ZMod.natCast_zmod_val (needs NeZero n), ZMod.unitOfCoprime, IsUnit.mul_left_injective, Fintype.bijective_iff_injective_and_card, Fintype.sum_bijective, Fintype.sum_prod_type, Finset.sum_mul_sum, ZMod.stdAddChar_coe (stated for an Int argument j, as the post says: stdAddChar ↑j = exp (2πI·j/N)), Complex.exp_int_mul_two_pi_mul_I, and Lean.ConstantInfo.getUsedConstantsAsSet (returns a NameSet). I have not re-run the proof itself.