English
The set {m·n + k | n ∈ ℕ} equals the set of natural numbers n with n ≡ k (mod m) and n ≥ k.
Русский
Множество {m·n + k | n ∈ ℕ} равно множеству натурных чисел n such that n ≡ k (mod m) и n ≥ k.
LaTeX
$$$\mathrm{range}(n \mapsto m \cdot n + k) = \{ n \in \mathbb{N} \mid n \equiv k \pmod m \ \land\ k \le n \}$$$
Lean4
/-- The range of `(m * · + k)` on natural numbers is the set of elements `≥ k` in the
residue class of `k` mod `m`. -/
theorem range_mul_add (m k : ℕ) : Set.range (fun n : ℕ ↦ m * n + k) = {n : ℕ | (n : ZMod m) = k ∧ k ≤ n} :=
by
ext n
simp only [Set.mem_range, Set.mem_setOf_eq]
conv => enter [1, 1, y]; rw [add_comm, eq_comm]
refine ⟨fun ⟨a, ha⟩ ↦ ⟨?_, le_iff_exists_add.mpr ⟨_, ha⟩⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
· simpa using congr_arg ((↑) : ℕ → ZMod m) ha
· obtain ⟨a, ha⟩ := le_iff_exists_add.mp H₂
simp only [ha, Nat.cast_add, add_eq_left, ZMod.natCast_eq_zero_iff] at H₁
obtain ⟨b, rfl⟩ := H₁
exact ⟨b, ha⟩
