case nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
⊢ dlookup a (dedupKeys []) = dlookup a []

case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l_hd : Sigma β
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
⊢ dlookup a (dedupKeys (l_hd :: tail✝)) = dlookup a (l_hd :: tail✝)
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ dlookup a (dedupKeys l) = dlookup a l
induction' l with l_hd _ l_ih
case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l_hd : Sigma β
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
⊢ dlookup a (dedupKeys (l_hd :: tail✝)) = dlookup a (l_hd :: tail✝)
case nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
⊢ dlookup a (dedupKeys []) = dlookup a []

case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l_hd : Sigma β
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
⊢ dlookup a (dedupKeys (l_hd :: tail✝)) = dlookup a (l_hd :: tail✝)
rfl
case cons.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
a' : α
b : β a'
⊢ dlookup a (dedupKeys ({ fst := a', snd := b } :: tail✝)) = dlookup a ({ fst := a', snd := b } :: tail✝)
case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l_hd : Sigma β
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
⊢ dlookup a (dedupKeys (l_hd :: tail✝)) = dlookup a (l_hd :: tail✝)
cases' l_hd with a' b
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
a' : α
b : β a'
h : a = a'
⊢ dlookup a (dedupKeys ({ fst := a', snd := b } :: tail✝)) = dlookup a ({ fst := a', snd := b } :: tail✝)

case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ dlookup a (dedupKeys ({ fst := a', snd := b } :: tail✝)) = dlookup a ({ fst := a', snd := b } :: tail✝)
case cons.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
a' : α
b : β a'
⊢ dlookup a (dedupKeys ({ fst := a', snd := b } :: tail✝)) = dlookup a ({ fst := a', snd := b } :: tail✝)
by_cases h : a = a'
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
b : β a
⊢ dlookup a (dedupKeys ({ fst := a, snd := b } :: tail✝)) = dlookup a ({ fst := a, snd := b } :: tail✝)
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
a' : α
b : β a'
h : a = a'
⊢ dlookup a (dedupKeys ({ fst := a', snd := b } :: tail✝)) = dlookup a ({ fst := a', snd := b } :: tail✝)
subst a'
no goals
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
b : β a
⊢ dlookup a (dedupKeys ({ fst := a, snd := b } :: tail✝)) = dlookup a ({ fst := a, snd := b } :: tail✝)
rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]
case neg.a
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ a ≠ { fst := a', snd := b }.fst
case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ dlookup a (dedupKeys ({ fst := a', snd := b } :: tail✝)) = dlookup a ({ fst := a', snd := b } :: tail✝)
rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]
no goals
case neg.a
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a (dedupKeys tail✝) = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ a ≠ { fst := a', snd := b }.fst
exact h