English
If f is strictly increasing and covers the range of indices through p, then composing nth with f preserves nth equality with p, i.e., f(nth (fun i => p (f i)) n) = nth p n.
Русский
Если f строго возрастает и достигает диапазона индексов через p, то составление nth с f сохраняет равенство nth p n: f(nth (fun i => p (f i)) n) = nth p n.
LaTeX
$$$\\\\forall {p:{\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}}\\\\ {n} {f:{\\\\mathbb{N}\\\\to \\\\mathbb{N}}},\\\\ StrictMono f \\\\Rightarrow \\\\ (\\\\forall k,\\\\ p k \\\\Rightarrow k \\\\in \\\\mathrm{range}\\\\ f) \\\\Rightarrow \\\\ (\\\\forall hfi:{\\\\{x:\\\\mathsf{N}\\\\mid p x\\\\}}\\\\Finite,\\\\ n < hfi.toFinset.card) \\\\Rightarrow \\\\ f(nth\\\\ (\\\\lambda i\\\\,\\\\ p (f i))\\\\ n) = nth\\\\ p\\\\ n.$$$
Lean4
theorem nth_comp_of_strictMono {n : ℕ} {f : ℕ → ℕ} (hf : StrictMono f) (h0 : ∀ k, p k → k ∈ Set.range f)
(h : ∀ hfi : (setOf p).Finite, n < hfi.toFinset.card) : f (nth (fun i ↦ p (f i)) n) = nth p n :=
by
have hs {p' : ℕ → Prop} (h0p' : ∀ k, p' k → k ∈ Set.range f) : f '' {i | p' (f i)} = setOf p' :=
by
ext i
refine ⟨fun ⟨_, hi, h⟩ ↦ h ▸ hi, fun he ↦ ?_⟩
rcases h0p' _ he with ⟨t, rfl⟩
exact ⟨t, he, rfl⟩
induction n using Nat.case_strong_induction_on
case _ =>
simp_rw [nth_zero]
replace h := nth_mem _ h
rw [← hs h0, ← hf.monotone.map_csInf]
rcases h0 _ h with ⟨t, ht⟩
exact ⟨t, Set.mem_setOf_eq ▸ ht ▸ h⟩
case _ n ih =>
repeat nth_rw 1 [nth_eq_sInf]
have h0' : ∀ k', (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f := fun _ h ↦ h0 _ h.1
rw [← hs h0', ← hf.monotone.map_csInf]
· convert rfl using 8 with k m' hm
nth_rw 2 [← hf.lt_iff_lt]
convert Iff.rfl using 2
exact ih m' (Nat.lt_add_one_iff.mp hm) fun hfi ↦ hm.trans (h hfi)
· rcases h0 _ (nth_mem _ h) with ⟨t, ht⟩
exact ⟨t, ht ▸ (nth_mem _ h), fun _ hk ↦ ht ▸ nth_lt_nth' hk h⟩
