English
If for all k < m we have ¬p k and nth p n ≠ 0, then nth (λi. p(i+m)) n + m = nth p n.
Русский
Если для всех k < m верно ¬p k и nth p n ≠ 0, то nth (λ i, p(i+m)) n + m = nth p n.
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {m n}:\\\\mathbb{N},\\\\ (\\\\forall k < m,\\\\ ¬p k) \\\\Rightarrow \\\\ nth\\\\ p\\\\ n \\\\neq 0 \\\\Rightarrow \\\\ nth\\\\ (\\\\lambda i\\\\,\\\\ p (i+m))\\\\ n + m =\\\\ nth\\\\ p\\\\ n.$$$
Lean4
theorem nth_add {m n : ℕ} (h0 : ∀ k < m, ¬p k) (h : nth p n ≠ 0) : nth (fun i ↦ p (i + m)) n + m = nth p n :=
by
refine
nth_comp_of_strictMono (strictMono_id.add_const m) (fun k hk ↦ ?_) (fun hf ↦ lt_card_toFinset_of_nth_ne_zero h hf)
by_contra hn
simp_rw [id_eq, Set.mem_range, eq_comm] at hn
exact h0 _ (not_le.mp fun h ↦ hn (le_iff_exists_add'.mp h)) hk
