Theorem: List.nodup_of_nodup_map (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
f : α → β
l : List α
h : Nodup (map f l)
⊢ Nodup l
Tactic:
induction l with
| nil => exact .nil
| cons a l IH =>
  dsimp at h
  apply nodup_cons_of_notmem_nodup
  . intro ha; exact h.head <| List.mem_map_of_mem f ha
  . exact IH h.tail
State after:
no goals

State before:
case nil
α : Type u
β : Type v
f : α → β
h : Nodup (map f [])
⊢ Nodup []
Tactic:
exact .nil
State after:
no goals

State before:
case cons
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (map f (a :: l))
⊢ Nodup (a :: l)
Tactic:
dsimp at h
State after:
case cons
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup (a :: l)

State before:
case cons
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup (a :: l)
Tactic:
apply nodup_cons_of_notmem_nodup
State after:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ ¬a ∈ l

case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l

State before:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ ¬a ∈ l

case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l
Tactic:
. intro ha; exact h.head <| List.mem_map_of_mem f ha
State after:
case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l

State before:
case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l
Tactic:
. exact IH h.tail
State after:
no goals

State before:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ ¬a ∈ l
Tactic:
intro ha
State after:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
ha : a ∈ l
⊢ False

State before:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
ha : a ∈ l
⊢ False
Tactic:
exact h.head <| List.mem_map_of_mem f ha
State after:
no goals

State before:
case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l
Tactic:
exact IH h.tail
State after:
no goals