English
If hf is finite, then Range(nth p) = {0} ∪ setOf p.
Русский
Если hf конечное, то диапазон nth p равен {0} ∪ множество {x | p(x)}.
LaTeX
$$For hf finite, Set.range (nth p) = insert 0 (setOf p).$$
Lean4
theorem range_nth_of_finite (hf : (setOf p).Finite) : Set.range (nth p) = insert 0 (setOf p) := by
simpa only [← List.getD_eq_getElem?_getD, ← nth_eq_getD_sort hf, mem_sort, Set.Finite.mem_toFinset] using
Set.range_list_getD (hf.toFinset.sort (· ≤ ·)) 0