α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ y✝ ∈ dlookup x✝ (s₁ ∪ s₂).entries ↔ y✝ ∈ dlookup x✝ (s₂ ∪ s₁).entries
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂).entries ↔ y ∈ dlookup x (s₂ ∪ s₁).entries
intros
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝ ↔
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ y✝ ∈ dlookup x✝ (s₁ ∪ s₂).entries ↔ y✝ ∈ dlookup x✝ (s₂ ∪ s₁).entries
simp
case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝

case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝ ↔
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
constructor <;> intro h'
case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝

case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
cases' h' with h' h'
case mp.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
right
case mp.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₂.entries
case mp.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
refine' ⟨_, h'⟩
case mp.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ x✝ ∈ keys s₁
case mp.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₂.entries
apply h
case mp.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ Option.isSome (some y✝) = true
case mp.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ x✝ ∈ keys s₁
rw [keys, ← List.dlookup_isSome, h']
no goals
case mp.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ Option.isSome (some y✝) = true
exact rfl
case mp.inr.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝
case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
left
no goals
case mp.inr.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝
rw [h'.2]
case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝

case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
cases' h' with h' h'
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
right
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₁.entries
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
refine' ⟨_, h'⟩
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ False
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₁.entries
intro h''
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ x✝ ∈ keys s₂
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ False
apply h _ h''
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ Option.isSome (some y✝) = true
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ x✝ ∈ keys s₂
rw [keys, ← List.dlookup_isSome, h']
no goals
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ Option.isSome (some y✝) = true
exact rfl
case mpr.inr.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝
case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
left
no goals
case mpr.inr.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝
rw [h'.2]