English
Kerase operations commute: kerase a2 (kerase a1 l) = kerase a1 (kerase a2 l) for all a1,a2 and l, with appropriate case distinctions; in particular, if a1=a2 the equality is trivial, otherwise the two orders yield the same result after careful case analysis.
Русский
Удаление по ключу kerase допускает коммутативность: kerase a2 (kerase a1 l) = kerase a1 (kerase a2 l) для любых a1,a2 и l, при разборе по случаям.
LaTeX
$$∀ {a1 a2} {l : List (Σ β)}, kerase a2 (kerase a1 l) = kerase a1 (kerase a2 l)$$
Lean4
theorem kerase_comm (a₁ a₂) (l : List (Sigma β)) : kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l) :=
if h : a₁ = a₂ then by simp [h]
else
if ha₁ : a₁ ∈ l.keys then
if ha₂ : a₂ ∈ l.keys then
match l, kerase a₁ l, exists_of_kerase ha₁, ha₂ with
| _, _, ⟨b₁, l₁, l₂, a₁_nin_l₁, rfl, rfl⟩, _ =>
if h' : a₂ ∈ l₁.keys then by
simp [kerase_append_left h', kerase_append_right (mt (mem_keys_kerase_of_ne h).mp a₁_nin_l₁)]
else by
simp [kerase_append_right h', kerase_append_right a₁_nin_l₁,
@kerase_cons_ne _ _ _ a₂ ⟨a₁, b₁⟩ _ (Ne.symm h)]
else by simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂]
else by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]
