English
There is a natural correspondence between the set {x ∈ Ioc a b | x ≡ v (mod r)} after casting to integers and the corresponding integer interval with ZMOD congruence.
Русский
Существует естественная корреспонденция между множеством {x ∈ Ioc a b | x ≡ v (mod r)} после приведения к целым и соответствующим интервалом целых чисел с ZMOD-конгруентностью.
LaTeX
$$$\{x \in \mathrm{Ioc}\ a\ b \mid x \equiv v \pmod{r}\}.map \mathrm{castEmbedding} = \{x \in \mathrm{Ioc}\ (a : \mathbb{Z})\ (b : \mathbb{Z}) \mid x \equiv v \pmod{r}\}$$$
Lean4
theorem Ioc_filter_modEq_cast {v : ℕ} :
{x ∈ Ioc a b | x ≡ v [MOD r]}.map castEmbedding = {x ∈ Ioc (a : ℤ) (b : ℤ) | x ≡ v [ZMOD r]} :=
by
ext x
simp only [mem_map, mem_filter, mem_Ioc, 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 cutsat); exact ⟨x, by simp_all [natCast_modEq_iff]⟩
