α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) [] l)
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
⊢ NodupKeys (dedupKeys l)
dsimp [dedupKeys]
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' l)
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) [] l)
generalize hl : nil = l'
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
this : NodupKeys l'
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' l)
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' l)
have : NodupKeys l' := by
  rw [← hl]
  apply nodup_nil
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
this : NodupKeys l'
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' l)
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
this : NodupKeys l'
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' l)
clear hl
case nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' [])

case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
x : Sigma β
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' (x :: xs))
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
this : NodupKeys l'
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' l)
induction' l with x xs l_ih
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ NodupKeys []
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ NodupKeys l'
rw [← hl]
no goals
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ NodupKeys []
apply nodup_nil
no goals
case nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' [])
apply this
case cons.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' ({ fst := fst✝, snd := snd✝ } :: xs))
case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
x : Sigma β
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' (x :: xs))
cases x
case cons.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ keys (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)) ∧
    NodupKeys (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs))
case cons.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' ({ fst := fst✝, snd := snd✝ } :: xs))
simp [dedupKeys]
case cons.mk.left
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ keys (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs))

case cons.mk.right
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ NodupKeys (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs))
case cons.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ keys (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)) ∧
    NodupKeys (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs))
constructor
case cons.mk.left
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ List.erase (keys (foldr (fun x => kinsert x.fst x.snd) l' xs)) fst✝
case cons.mk.left
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ keys (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs))
simp [keys_kerase]
no goals
case cons.mk.left
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ List.erase (keys (foldr (fun x => kinsert x.fst x.snd) l' xs)) fst✝
apply l_ih.not_mem_erase
no goals
case cons.mk.right
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l' : List (Sigma β)
this : NodupKeys l'
xs : List (Sigma β)
l_ih : NodupKeys (foldr (fun x => kinsert x.fst x.snd) l' xs)
fst✝ : α
snd✝ : β fst✝
⊢ NodupKeys (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs))
exact l_ih.kerase _