English
For any integer x and NeZero n, the natural projection of x into Fin n has value equal to x mod n.
Русский
Для целого x и не нуля n изображение x в Fin n имеет значение x mod n.
LaTeX
$$$(x : \text{Fin } n).\text{val} = (x \bmod n).\text{toNat}$$$
Lean4
@[simp]
theorem val_intCast {n : Nat} [NeZero n] (x : Int) : (x : Fin n).val = (x % n).toNat :=
by
rw [Fin.intCast_def']
split <;> rename_i h
· simp [Int.emod_natAbs_of_nonneg h]
· simp only [Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]
split <;> rename_i h
· rw [← Int.natCast_dvd] at h
rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]
· rw [Int.emod_natAbs_of_neg (by cutsat) (NeZero.ne n), if_neg (by rwa [← Int.natCast_dvd] at h)]
have : x % n < n := Int.emod_lt_of_pos x (by have := NeZero.ne n; cutsat)
cutsat
