English
There is a natural correspondence between the set {x in Ico a b | x ≡ v (mod r)} under natural embedding to integers and the corresponding integer interval with congruence modulo r. In particular, the image of the nat-interval under castEmbedding equals the integer-interval with ZMOD congruence.
Русский
Существует естественная взаимно однозначная соответствие между множествами {x ∈ Ico a b | x ≡ v (mod r)} после включения в целые числа и соответствующим целочисленным интервалом с той же конгруэнтностью модуль r; образ nat-интервала равен интервалу целых чисел с ZMOD-конгруентностью.
LaTeX
$$$\{x \in \mathrm{Ico}\ a\ b \mid x \equiv v \pmod{r}\}.map \mathrm{castEmbedding} = \{x \in \mathrm{Ico}\ (a:\mathbb{Z})\ (b:\mathbb{Z}) \mid x \equiv v \pmod{r}\}$$$
Lean4
theorem Ico_filter_modEq_cast {v : ℕ} :
{x ∈ Ico a b | x ≡ v [MOD r]}.map castEmbedding = {x ∈ Ico (a : ℤ) (b : ℤ) | x ≡ v [ZMOD r]} :=
by
ext x
simp only [mem_map, mem_filter, mem_Ico, castEmbedding_apply]
constructor
· simp_rw [forall_exists_index, ← natCast_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h
· intro h; lift x to ℕ using (by omega); exact ⟨x, by simp_all [natCast_modEq_iff]⟩
