case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
h' : a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
h' : ¬a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
by_cases h' : a ∈ s₁
no goals
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
h' : a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
rw [lookup_union_left h']
no goals
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
h' : ¬a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']