Theorem: List.Nodup.append (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
l l' : List α
nodup : Nodup l
nodup' : Nodup l'
h : ∀ (a : α), a ∈ l → ¬a ∈ l'
⊢ Nodup (l ++ l')
Tactic:
induction l with
| nil => exact nodup'
| cons a l IH =>
  specialize IH nodup.tail fun a ha =>
    h a <| mem_cons_of_mem _ ha
  refine nodup_cons_of_notmem_nodup a ?_ IH
  simp only [append_eq, mem_append, not_or]
  exact ⟨nodup.head, h a <| l.mem_cons_self a⟩
State after:
no goals

State before:
case nil
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
nodup : Nodup []
h : ∀ (a : α), a ∈ [] → ¬a ∈ l'
⊢ Nodup ([] ++ l')
Tactic:
exact nodup'
State after:
no goals

State before:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
IH : Nodup l → (∀ (a : α), a ∈ l → ¬a ∈ l') → Nodup (l ++ l')
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
⊢ Nodup (a :: l ++ l')
Tactic:
specialize IH nodup.tail fun a ha =>
  h a <| mem_cons_of_mem _ ha
State after:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ Nodup (a :: l ++ l')

State before:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ Nodup (a :: l ++ l')
Tactic:
refine nodup_cons_of_notmem_nodup a ?_ IH
State after:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ ¬a ∈ List.append l l'

State before:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ ¬a ∈ List.append l l'
Tactic:
simp only [append_eq, mem_append, not_or]
State after:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ ¬a ∈ l ∧ ¬a ∈ l'

State before:
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ ¬a ∈ l ∧ ¬a ∈ l'
Tactic:
exact ⟨nodup.head, h a <| l.mem_cons_self a⟩
State after:
no goals