English
The membership of b in dlookup a (kunion l1 l2) is equivalent to (b in dlookup a l1) or (a not in l1.keys and b in dlookup a l2).
Русский
Членство b в dlookup a (kunion l1 l2) эквивалентно (b в dlookup a l1) или (a не в keys l1 и b в dlookup a l2).
LaTeX
$$$ b \\in dlookup\\ a\\ (kunion\\ l_1\\ l_2) \\iff b \\in dlookup\\ a\\ l_1 \\lor (a \\notin l_1.\\keys \\land b \\in dlookup\\ a\\ l_2) $$$
Lean4
theorem mem_dlookup_kunion {a} {b : β a} {l₁ l₂ : List (Sigma β)} :
b ∈ dlookup a (kunion l₁ l₂) ↔ b ∈ dlookup a l₁ ∨ a ∉ l₁.keys ∧ b ∈ dlookup a l₂ := by
induction l₁ generalizing l₂ with
| nil => simp
| cons s _ ih =>
obtain ⟨a'⟩ := s
by_cases h₁ : a = a'
· subst h₁
simp
· simp [h₁, @ih (kerase a' l₂)]
