English
If nth p n ≠ 0, then n < #hf.toFinset for hf : (setOf p).Finite.
Русский
Если nth p n ≠ 0, то n < #hf.toFinset при hf : (setOf p).Finite.
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {n}:\\\\mathbb{N},\\\\ nth\\\\ p\\\\ n \\\\neq 0 \\\\Rightarrow \\\\forall hf:\\\\{x:\\\\mathbb{N}\\\\mid p x\\\\}\\\\Finite,\\\\ n < #hf.toFinset.$$$
Lean4
theorem lt_card_toFinset_of_nth_ne_zero {n : ℕ} (h : nth p n ≠ 0) (hf : (setOf p).Finite) : n < #hf.toFinset :=
by
simp only [ne_eq, nth_eq_zero, not_or, not_exists, not_le] at h
exact h.2 hf