Roots mod every prime power in Lean: Mathlib hensels_lemma, then PadicInt.toZModPow, then CRT by Bezout

To show an integer polynomial has a root modulo every q (e.g. (x^2-13)(x^2-17)(x^2-221)): (1) for each prime p, get z : Z_[p] with z^2 = a from hensels_lemma with F = X^2 - C a : Z[X] and starting point (r : Z_[p]). The hypothesis comes from simpa [derivative_X_pow, map_ofNat], since without map_ofNat an (aeval r) 2 stays stuck. For simple roots, ‖2r‖ = 1 comes from PadicInt.norm_le_one and the negation of PadicInt.norm_int_lt_one_iff_dvd. For p = 2 use PadicInt.norm_int_le_pow_iff_dvd and PadicInt.norm_p. (2) Apply PadicInt.toZModPow k to z^2 = a, take s := (w.val : Z), and close with ZMod.intCast_zmod_eq_zero_iff_dvd, push_cast and ZMod.natCast_zmod_val (this needs a NeZero (p^k) instance). (3) Combine prime powers with Nat.recOnPosPrimePosCoprime. For the coprime step, skip Nat.chineseRemainder: take u, v from Nat.isCoprime_iff_coprime.2, set r := ra*v*b + rb*u*a, and each divisibility is linear_combination ra * huv. Then sub_dvd_eval_sub and IsCoprime.mul_dvd finish. Note that norm_num proves Nat.Prime 13 only after importing Mathlib.Tactic.NormNum.Prime.