English
Let a be an index from α and l be a list of pairs (a',b) with a' varying over α. If a appears among the first components (the keys) of l, then there exist a value b for which the a-th entry is (a,b) and there are lists l1, l2 such that a is not among the keys of l1, l equals l1 concatenated with the entry (a,b) followed by l2, and kerase a l equals l1 concatenated with l2. In other words, one can isolate the occurrence of a in l and remove it from the list while preserving the rest.
Русский
Пусть a принадлежит α, а l — список пар (α, β). Если a встречается среди ключей списка l, то существует b: β a и существует разбиение l на l1 и l2 такие, что a не принадлежит l1.keys, l = l1 ++ ⟨a,b⟩ :: l2 и kerase a l = l1 ++ l2. То есть можно выделить первое вхождение ключа a в l и удалить его, не трогая остальное.
LaTeX
$$$\forall {a : \alpha} {l : List (\ Sigma \beta)} (h : a \in l.keys), \exists b : \beta a, \exists l_1 l_2 : List (\Sigma \beta), a \notin l_1.keys \land l = l_1 ++ \langle a,b\rangle :: l_2 \land kerase a l = l_1 ++ l_2$$$
Lean4
theorem exists_of_kerase {a : α} {l : List (Sigma β)} (h : a ∈ l.keys) :
∃ (b : β a) (l₁ l₂ : List (Sigma β)), a ∉ l₁.keys ∧ l = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a l = l₁ ++ l₂ := by
induction l with
| nil => cases h
| cons hd tl ih =>
by_cases e : a = hd.1
· subst e
exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩
· simp only [keys_cons, mem_cons] at h
rcases h with h | h
· exact absurd h e
rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩
exact ⟨b, hd :: tl₁, tl₂, not_mem_cons_of_ne_of_not_mem e h₁, by (rw [h₂]; rfl), by simp [e, h₃]⟩
