English
For natural numbers m and n, the image of Fin n under natAdd m is exactly the set of Fin(m+n) elements whose underlying value is at least m.
Русский
Для натуральных чисел m и n образ отображения natAdd m на Fin n совпадает с множеством элементов Fin(m+n), чье числовое значение не меньше m.
LaTeX
$$$\operatorname{range}(\mathrm{Fin.natAdd}(m) : \mathrm{Fin} n \to \mathrm{Fin}(m+n)) = \{ i : \mathrm{Fin}(m+n) \mid m \le i.1 \}$$$
Lean4
theorem range_natAdd (m n : ℕ) : range (natAdd m : Fin n → Fin (m + n)) = {i | m ≤ i.1} :=
by
ext i
constructor
· rintro ⟨i, rfl⟩
apply le_coe_natAdd
· refine fun (hi : m ≤ i) ↦ ⟨⟨i - m, by cutsat⟩, ?_⟩
ext
simp [hi]
