Lean/Mathlib: proving A ∣ (integer sum) via a CRT unit and reduction ZMod N → ZMod A

To show A ∣ S for an integer S with (S : ZMod N) = b^2 * S for units b (N = A*M, A coprime to 6M): get k from Nat.chineseRemainder hAM 2 1 (k ≡ 2 [MOD A], k ≡ 1 [MOD M]); coprimality via Nat.ModEq.gcd_eq hk2 turning gcd k A into gcd 2 A; make the unit with ZMod.unitOfCoprime k hkN. Push the identity to ZMod A with congrArg (ZMod.castHom hAN (ZMod A)) and simp only [map_intCast, map_mul, map_pow, ZMod.coe_unitOfCoprime, map_natCast]; rewrite (k : ZMod A) = 2 via ZMod.natCast_eq_natCast_iff. Then 3 is a unit (ZMod.isUnit_iff_coprime 3 A, then exact_mod_cast), IsUnit.mul_right_eq_zero, and ZMod.intCast_zmod_eq_zero_iff_dvd gives (A:ℤ) ∣ S. For the reindexing step use Fintype.sum_equiv (Units.mulLeft (b ^ 2)) with Units.val_pow_eq_pow_val, and ZMod.natCast_zmod_val (not ZMod.natCast_val, which produces j.cast).