-- Mathlib/Data/List/Sigma.lean
theorem dlookup_kunion_left {a} {l₁ l₂ : List (Sigma β)} (h : a ∈ l₁.keys) :
    dlookup a (kunion l₁ l₂) = dlookup a l₁

Proof state:
case cons.inl.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h : a = ⟨a', snd✝⟩.fst
⊢ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
subst h

Result:
case cons.inl.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
snd✝ : β a
⊢ dlookup a ((⟨a, snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a, snd✝⟩ :: tail✝)

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : ¬a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
simp [h', ih h]

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
snd✝ : β a
⊢ dlookup a (⟨a, snd✝⟩ :: tail✝.kunion (kerase ⟨a, snd✝⟩.fst l₂)) = dlookup a (⟨a, snd✝⟩ :: tail✝)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : a ∈ l₁.keys
⊢ dlookup a (l₁.kunion l₂) = dlookup a l₁

Tactic:
induction' l₁ with s _ ih generalizing l₂ <;> simp at h

Result:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a = s.fst ∨ a ∈ tail✝.keys
⊢ dlookup a ((s :: tail✝).kunion l₂) = dlookup a (s :: tail✝)

Proof state:
case cons.inl.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
snd✝ : β a
⊢ dlookup a ((⟨a, snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a, snd✝⟩ :: tail✝)

Tactic:
simp

Result:
no goals

Proof state:
case cons.inr.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
by_cases h' : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : ¬a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
subst h'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
snd✝ : β a
⊢ dlookup a (⟨a, snd✝⟩ :: tail✝.kunion (kerase ⟨a, snd✝⟩.fst l₂)) = dlookup a (⟨a, snd✝⟩ :: tail✝)

Proof state:
case cons.inr.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
⊢ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
rw [kunion_cons]

Result:
case cons.inr.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a = s.fst ∨ a ∈ tail✝.keys
⊢ dlookup a ((s :: tail✝).kunion l₂) = dlookup a (s :: tail✝)

Tactic:
rcases h with h | h <;> obtain ⟨a'⟩ := s

Result:
case cons.inl.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h : a = ⟨a', snd✝⟩.fst
⊢ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a', snd✝⟩ :: tail✝)

case cons.inr.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
⊢ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a', snd✝⟩ :: tail✝)