Lean: lift a congruence mod p to an equality of small integers
To show x = y in ℤ from (x : ZMod p) = y when |x|, |y| < p/2: rewrite with ZMod.intCast_eq_intCast_iff_dvd_sub to get (p:ℤ) ∣ y - x, then apply Int.eq_zero_of_abs_lt_dvd and discharge |y - x| < p with rw [abs_lt] at *; constructor <;> omega (omega handles (p:ℤ) / 2). For a small integer representative of y : ZMod p use y.valMinAbs: ZMod.coe_valMinAbs, ZMod.valMinAbs_eq_zero, ZMod.natAbs_valMinAbs_le (natAbs ≤ p/2; after rw [Int.abs_eq_natAbs], omega gives 2|d| ≤ p). Gotcha: exact_mod_cast on 2 * |d| ≤ p produces ↑|d|, not |↑d|; use rw [← Int.cast_abs] first. Jordan's inequality is Real.mul_le_sin (2/π·x ≤ sin x on [0, π/2]), and Complex.norm_exp_I_mul_ofReal_sub_one gives |e^{ix} - 1| = |2 sin(x/2)|.
Checked on Mathlib v4.35.0: all the names exist with the stated statements, and the main recipe compiles as written (
rw [ZMod.intCast_eq_intCast_iff_dvd_sub] at h, thenInt.eq_zero_of_abs_lt_dvd h (by rw [abs_lt] at *; constructor <;> omega), thenomega). I could not reproduce the exact_mod_cast gotcha. Fromh : 2 * |d| ≤ (p:ℤ),exact_mod_cast hcloses2 * |(d:ℝ)| ≤ pdirectly, and the reverse direction works too. What does fail is starting from the ℕ formh : 2 * d.natAbs ≤ p(as omega gives it afterInt.abs_eq_natAbs):exact_mod_castreports a mismatch with2 * |d| ≤ ↑p. There,rw [← Int.cast_abs, Int.abs_eq_natAbs]; exact_mod_cast hworks.