case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
⊢ dedup ([] ++ l₂) = [] ∪ dedup l₂

case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
⊢ dedup (a :: l₁ ++ l₂) = a :: l₁ ∪ dedup l₂
α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
induction' l₁ with a l₁ IH
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = List.union l₁ (dedup l₂)
⊢ dedup (a :: l₁ ++ l₂) = List.insert a (List.union l₁ (dedup l₂))
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
⊢ dedup (a :: l₁ ++ l₂) = a :: l₁ ∪ dedup l₂
simp only [instUnionList, cons_union] at *
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = List.union l₁ (dedup l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = List.union l₁ (dedup l₂)
⊢ dedup (a :: l₁ ++ l₂) = List.insert a (List.union l₁ (dedup l₂))
rw [← IH, cons_append]
case pos
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = List.union l₁ (dedup l₂)
h : a ∈ dedup (l₁ ++ l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))

case neg
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = List.union l₁ (dedup l₂)
h : ¬a ∈ dedup (l₁ ++ l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = List.union l₁ (dedup l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
by_cases h : a ∈ dedup (l₁ ++ l₂)
no goals
case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
⊢ dedup ([] ++ l₂) = [] ∪ dedup l₂
rfl
no goals
case pos
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = List.union l₁ (dedup l₂)
h : a ∈ dedup (l₁ ++ l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
rw [dedup_cons_of_mem' h, insert_of_mem h]
no goals
case neg
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = List.union l₁ (dedup l₂)
h : ¬a ∈ dedup (l₁ ++ l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
rw [dedup_cons_of_not_mem' h, insert_of_not_mem h]