English
The embedding from m to n produced by the natural directed system is exactly the canonical iterated embedding given by the standard leRecOn construction. In other words, natLERec f′ m n h coincides with Nat.leRecOn h (λk. f′k).
Русский
Встраивание из m в n, получаемое из направленной цепи натурального индекса, совпадает с каноническим повторным вложением, заданным через конструкцию Nat.leRecOn.
LaTeX
$$$\\operatorname{natLERec}(f',m,n,h) = \\operatorname{Nat.leRecOn}(h,\\lambda k. f'(k)).$$$
Lean4
@[simp]
theorem coe_natLERec (m n : ℕ) (h : m ≤ n) : (natLERec f' m n h : G' m → G' n) = Nat.leRecOn h (@fun k => f' k) :=
by
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
ext x
induction k with
| zero =>
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [natLERec, Nat.leRecOn_self, Embedding.refl_apply, Nat.leRecOn_self]
| succ k ih =>
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec, Embedding.comp_apply, ih]
