-- Mathlib/Data/List/Sigma.lean
theorem nodupKeys_dedupKeys (l : List (Sigma β)) : NodupKeys (dedupKeys l)

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
⊢ (foldr (fun x => kinsert x.fst x.snd) [] l).NodupKeys

Tactic:
generalize hl : nil = l'

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ (foldr (fun x => kinsert x.fst x.snd) l' l).NodupKeys

Proof state:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ fst✝ ∉ (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)).keys ∧
    (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)).NodupKeys

Tactic:
constructor

Result:
case cons.mk.left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ fst✝ ∉ (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)).keys

case cons.mk.right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)).NodupKeys

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
this : l'.NodupKeys
⊢ (foldr (fun x => kinsert x.fst x.snd) l' l).NodupKeys

Tactic:
clear hl

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
this : l'.NodupKeys
⊢ (foldr (fun x => kinsert x.fst x.snd) l' l).NodupKeys

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
this : l'.NodupKeys
⊢ (foldr (fun x => kinsert x.fst x.snd) l' l).NodupKeys

Tactic:
induction' l with x xs l_ih

Result:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
⊢ (foldr (fun x => kinsert x.fst x.snd) l' []).NodupKeys

case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
x : Sigma β
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
⊢ (foldr (fun x => kinsert x.fst x.snd) l' (x :: xs)).NodupKeys

Proof state:
case cons.mk.left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ fst✝ ∉ (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)).keys

Tactic:
simp only [keys_kerase]

Result:
case cons.mk.left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ fst✝ ∉ (foldr (fun x => kinsert x.fst x.snd) l' xs).keys.erase fst✝

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
x : Sigma β
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
⊢ (foldr (fun x => kinsert x.fst x.snd) l' (x :: xs)).NodupKeys

Tactic:
cases x

Result:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ (foldr (fun x => kinsert x.fst x.snd) l' (⟨fst✝, snd✝⟩ :: xs)).NodupKeys

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ [].NodupKeys

Tactic:
apply nodup_nil

Result:
no goals

Proof state:
case cons.mk.right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)).NodupKeys

Tactic:
exact l_ih.kerase _

Result:
no goals

Proof state:
case cons.mk.left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ fst✝ ∉ (foldr (fun x => kinsert x.fst x.snd) l' xs).keys.erase fst✝

Tactic:
apply l_ih.not_mem_erase

Result:
no goals

Proof state:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ (foldr (fun x => kinsert x.fst x.snd) l' (⟨fst✝, snd✝⟩ :: xs)).NodupKeys

Tactic:
simp only [foldr_cons, kinsert_def, nodupKeys_cons, ne_eq, not_true]

Result:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x => kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ fst✝ ∉ (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)).keys ∧
    (kerase fst✝ (foldr (fun x => kinsert x.fst x.snd) l' xs)).NodupKeys

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ (foldr (fun x => kinsert x.fst x.snd) l' l).NodupKeys

Tactic:
have : NodupKeys l' := by
  rw [← hl]
  apply nodup_nil

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
this : l'.NodupKeys
⊢ (foldr (fun x => kinsert x.fst x.snd) l' l).NodupKeys

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ l'.NodupKeys

Tactic:
rw [← hl]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ [].NodupKeys

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

Tactic:
dsimp [dedupKeys]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
⊢ (foldr (fun x => kinsert x.fst x.snd) [] l).NodupKeys

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
⊢ (foldr (fun x => kinsert x.fst x.snd) l' []).NodupKeys

Tactic:
apply this

Result:
no goals