-- Mathlib/Data/List/Sigma.lean
theorem dlookup_dedupKeys (a : α) (l : List (Sigma β)) : dlookup a (dedupKeys l) = dlookup a l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
b : β a
⊢ dlookup a (⟨a, b⟩ :: tail✝).dedupKeys = dlookup a (⟨a, b⟩ :: tail✝)

Tactic:
rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Tactic:
rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]

Result:
case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

Proof state:
case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

Tactic:
exact h

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l_hd : Sigma β
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
⊢ dlookup a (l_hd :: tail✝).dedupKeys = dlookup a (l_hd :: tail✝)

Tactic:
obtain ⟨a', b⟩ := l_hd

Result:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : a = a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
b : β a
⊢ dlookup a (⟨a, b⟩ :: tail✝).dedupKeys = dlookup a (⟨a, b⟩ :: tail✝)

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ dlookup a l.dedupKeys = dlookup a l

Tactic:
induction' l with l_hd _ l_ih

Result:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ dlookup a [].dedupKeys = dlookup a []

case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l_hd : Sigma β
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
⊢ dlookup a (l_hd :: tail✝).dedupKeys = dlookup a (l_hd :: tail✝)

Proof state:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Tactic:
by_cases h : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : a = a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ dlookup a [].dedupKeys = dlookup a []

Tactic:
rfl

Result:
no goals