English
Let xs, ys be lists with xs Nodup and same length as ys. For any x,y and index i, if xs[i]? = some x, then List.applyId(xs.zip ys) x = y iff ys[i]? = some y.
Русский
Пусть xs, ys — списки, xs без повторов и равной длины; для любого x,y и индекса i, если xs[i]? = some x, то List.applyId(xs.zip ys) x = y тогда и только тогда ys[i]? = some y.
LaTeX
$$$\forall xs ys,\; xs\Nodup \rightarrow xs.length = ys.length \rightarrow \forall x,y,i,\; xs[i]? = \mathrm{Some}(x) \rightarrow \big(\mathrm{List.applyId}(xs.zip ys)\; x = y \iff ys[i]? = \mathrm{Some}(y)\big)$$$
Lean4
theorem applyId_zip_eq [DecidableEq α] {xs ys : List α} (h₀ : List.Nodup xs) (h₁ : xs.length = ys.length) (x y : α)
(i : ℕ) (h₂ : xs[i]? = some x) : List.applyId.{u} (xs.zip ys) x = y ↔ ys[i]? = some y := by
induction xs generalizing ys i with
| nil => cases h₂
| cons x' xs xs_ih =>
cases i
· simp only [length_cons, lt_add_iff_pos_left, add_pos_iff, Nat.lt_add_one, or_true, getElem?_eq_getElem,
getElem_cons_zero, Option.some.injEq] at h₂
subst h₂
cases ys
· cases h₁
· simp
· cases ys
· cases h₁
· obtain - | ⟨h₀, h₁⟩ := h₀
simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢
rw [if_neg]
· apply xs_ih <;> solve_by_elim [Nat.succ.inj]
· apply h₀; apply List.mem_of_getElem? h₂
