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

State before:
α : Type u
β : Type v
l : List α
nodup : Nodup l
p : α → Bool
⊢ Nodup (List.filter p l)
Tactic:
induction l with
| nil => exact .nil
| cons a l IH =>
  specialize IH nodup.tail
  dsimp [List.filter]
  cases p a <;> dsimp
  . exact IH
  . refine nodup_cons_of_notmem_nodup _ ?_ IH
    intro ha
    exact nodup.head <| l.filter_sublist.subset ha
State after:
no goals

State before:
case nil
α : Type u
β : Type v
p : α → Bool
nodup : Nodup []
⊢ Nodup (List.filter p [])
Tactic:
exact .nil
State after:
no goals

State before:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
IH : Nodup l → Nodup (List.filter p l)
nodup : Nodup (a :: l)
⊢ Nodup (List.filter p (a :: l))
Tactic:
specialize IH nodup.tail
State after:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p (a :: l))

State before:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p (a :: l))
Tactic:
dsimp [List.filter]
State after:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup
    (match p a with
    | true => a :: List.filter p l
    | false => List.filter p l)

State before:
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup
    (match p a with
    | true => a :: List.filter p l
    | false => List.filter p l)
Tactic:
cases p a <;> dsimp
State after:
case cons.false
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p l)

case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)

State before:
case cons.false
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p l)

case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)
Tactic:
. exact IH
State after:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)

State before:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)
Tactic:
. refine nodup_cons_of_notmem_nodup _ ?_ IH
  intro ha
  exact nodup.head <| l.filter_sublist.subset ha
State after:
no goals

State before:
case cons.false
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p l)
Tactic:
exact IH
State after:
no goals

State before:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)
Tactic:
refine nodup_cons_of_notmem_nodup _ ?_ IH
State after:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ ¬a ∈ List.filter p l

State before:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ ¬a ∈ List.filter p l
Tactic:
intro ha
State after:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
ha : a ∈ List.filter p l
⊢ False

State before:
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
ha : a ∈ List.filter p l
⊢ False
Tactic:
exact nodup.head <| l.filter_sublist.subset ha
State after:
no goals