English
If two ALists s1 and s2 are disjoint, then the entries of their union commute up to permutation: (s1 ∪ s2).entries is perm-equivalent to (s2 ∪ s1).entries.
Русский
Если два AList-объединения s1 и s2 несовместны, то множество их элементов совпадает до перестановки: (s1 ∪ s2).entries переставляется к (s2 ∪ s1).entries.
LaTeX
$$Disjoint(s1,s2) → (s1 ∪ s2).entries ~ (s2 ∪ s1).entries$$
Lean4
theorem union_comm_of_disjoint {s₁ s₂ : AList β} (h : Disjoint s₁ s₂) : (s₁ ∪ s₂).entries ~ (s₂ ∪ s₁).entries :=
lookup_ext (AList.nodupKeys _) (AList.nodupKeys _)
(by
intros; simp only [union_entries, Option.mem_def, dlookup_kunion_eq_some]
constructor <;> intro h'
· rcases h' with h' | h'
· right
refine ⟨?_, h'⟩
apply h
rw [keys, ← List.dlookup_isSome, h']
exact rfl
· left
rw [h'.2]
· rcases h' with h' | h'
· right
refine ⟨?_, h'⟩
intro h''
apply h _ h''
rw [keys, ← List.dlookup_isSome, h']
exact rfl
· left
rw [h'.2])
