English
The simp-normal form of mem_lookup_union: for a : α, b : β a, s1 s2 : Finmap β, lookup a (s1 ∪ s2) = some b iff b ∈ lookup a s1 ∨ (¬(a ∈ s1) ∧ b ∈ lookup a s2).
Русский
Упрощенная симп-форма mem_lookup_union: для a : α, b : β a, s1 s2 : Finmap β выполняется lookup a (s1 ∪ s2) = some b тогда и только тогда, когда b ∈ lookup a s1 или (a ∉ s1 и b ∈ lookup a s2).
LaTeX
$$$ \operatorname{lookup}(a, \text{Finmap}.\,\text{union}(s_1,s_2)) = \text{some } b \;\iff\; (b \in \operatorname{lookup}(a, s_1)) \lor \bigl( \neg(a \in s_1) \land b \in \operatorname{lookup}(a, s_2) \bigr) $$$
Lean4
/-- `simp`-normal form of `mem_lookup_union` -/
@[simp]
theorem mem_lookup_union' {a} {b : β a} {s₁ s₂ : Finmap β} :
lookup a (s₁ ∪ s₂) = some b ↔ b ∈ lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ lookup a s₂ :=
induction_on₂ s₁ s₂ fun _ _ => AList.mem_lookup_union
