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

State before:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
⊢ Nodup (a :: l)
Tactic:
refine .cons ?_ hnodup
State after:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'

State before:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'
Tactic:
intros _ hal h
State after:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
a'✝ : α
hal : a'✝ ∈ l
h : a = a'✝
⊢ False

State before:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
a'✝ : α
hal : a'✝ ∈ l
h : a = a'✝
⊢ False
Tactic:
cases h
State after:
case refl
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
hal : a ∈ l
⊢ False

State before:
case refl
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
hal : a ∈ l
⊢ False
Tactic:
exact ha hal
State after:
no goals