Theorem: Misc.List.Nodup.not_mem_erase (LeanSAT/Util/Misc.lean)

State before:
α : Type u_1
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : l.Nodup
H : a ∈ l.erase a
⊢ False
Tactic:
have h := ((List.Nodup.mem_erase_iff h).mp H).left
State after:
α : Type u_1
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h✝ : l.Nodup
H : a ∈ l.erase a
h : (a != a) = true
⊢ False

State before:
α : Type u_1
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h✝ : l.Nodup
H : a ∈ l.erase a
h : (a != a) = true
⊢ False
Tactic:
simp only [bne_self_eq_false] at h
State after:
no goals