English
If a1 and a2 are distinct, then for any list l, an element a1 belongs to the set of keys of kerase a2 l if and only if a1 belongs to the set of keys of l. In words, erasing a different key from the list does not affect membership of a distinct key in the key set.
Русский
Если a1 и a2 различны, то для любого списка l элемент a1 принадлежит множеству ключей kerase a2 l тогда и только тогда, когда a1 принадлежит множеству ключей l.
LaTeX
$$$\forall {a_1 a_2} {l : List (\Sigma \beta)} (h : a_1 \neq a_2), a_1 \in (kerase a_2 l).keys \leftrightarrow a_1 \in l.keys$$$
Lean4
@[simp]
theorem mem_keys_kerase_of_ne {a₁ a₂} {l : List (Sigma β)} (h : a₁ ≠ a₂) : a₁ ∈ (kerase a₂ l).keys ↔ a₁ ∈ l.keys :=
(Iff.intro mem_keys_of_mem_keys_kerase) fun p =>
if q : a₂ ∈ l.keys then
match l, kerase a₂ l, exists_of_kerase q, p with
| _, _, ⟨_, _, _, _, rfl, rfl⟩, p => by simpa [keys, h] using p
else by simp [q, p]
