English
If a1 ≠ a2, then a1 ∈ (kerase a2 l).keys is equivalent to a1 ∈ l.keys. This holds for any l.
Русский
Если a1 ≠ a2, то a1 принадлежит ключам kerase a2 l тогда и только тогда, когда a1 принадлежит ключам l.
LaTeX
$$∀ {α β} {l : List (Σ β)} {a1 a2}, a1 ≠ a2 → (a1 ∈ (kerase a2 l).keys ↔ a1 ∈ l.keys)$$
Lean4
@[simp]
theorem notMem_keys_kerase (a) {l : List (Sigma β)} (nd : l.NodupKeys) : a ∉ (kerase a l).keys := by
induction l with
| nil => simp
| cons hd tl ih =>
simp only [nodupKeys_cons] at nd
by_cases h : a = hd.1
· subst h
simp [nd.1]
· simp [h, ih nd.2]