English
For any nodup l and function f with i ∈ l, the elimination of the constructed mk(l,f) at i returns f(i): (List.TProd.mk l f).elim hi = f i.
Русский
Для неповторяющегося списка l и функции f при i ∈ l элиминация mk(l,f) даёт f(i).
LaTeX
$$$(\\mathrm{List.TProd.mk}\\; l\\; f).\\mathrm{elim} hi = f(i).$$$
Lean4
theorem elim_mk : ∀ (l : List ι) (f : ∀ i, α i) {i : ι} (hi : i ∈ l), (TProd.mk l f).elim hi = f i
| i :: is, f, j, hj => by
by_cases hji : j = i
· subst hji
simp
· rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]