English
For xs,y s.t. xs Nodup and xs ~ ys, we have: the value List.applyId(xs.zip ys) x belongs to ys if and only if x belongs to xs.
Русский
Пусть xs без повторов и xs эквивалентно ys; тогда значение List.applyId(xs.zip ys) для x принадлежит ys тогда и только тогда x принадлежит xs.
LaTeX
$$$\text{List.applyId}(xs.zip ys)\; x \in ys \iff x \in xs$$$
Lean4
theorem applyId_mem_iff [DecidableEq α] {xs ys : List α} (h₀ : List.Nodup xs) (h₁ : xs ~ ys) (x : α) :
List.applyId.{u} (xs.zip ys) x ∈ ys ↔ x ∈ xs :=
by
simp only [List.applyId]
cases h₃ : List.dlookup x (List.map Prod.toSigma (xs.zip ys)) with
| none =>
dsimp [Option.getD]
rw [h₁.mem_iff]
| some val =>
have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀
replace h₁ : xs.length = ys.length := h₁.length_eq
dsimp
induction xs generalizing ys with
| nil => contradiction
| cons x' xs xs_ih =>
rcases ys with - | ⟨y, ys⟩
· cases h₃
dsimp [List.dlookup] at h₃; split_ifs at h₃ with h
· rw [Option.some_inj] at h₃
subst x'; subst val
simp only [List.mem_cons, true_or]
· obtain - | ⟨h₀, h₅⟩ := h₀
obtain - | ⟨h₂, h₄⟩ := h₂
have h₆ := Nat.succ.inj h₁
specialize xs_ih h₅ h₃ h₄ h₆
simp only [Ne.symm h, xs_ih, List.mem_cons]
suffices val ∈ ys by tauto
rw [← Option.mem_def, List.mem_dlookup_iff] at h₃
· simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃
rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
apply (List.of_mem_zip h₃).2
simp only [List.NodupKeys, List.keys, comp_def, Prod.fst_toSigma, List.map_map]
rwa [List.map_fst_zip (le_of_eq h₆)]
