α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a = b ∧ ¬a ∈ l
⊢ List.erase (b :: l) a = b :: l
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a ∈ b :: l
⊢ List.erase (b :: l) a = b :: l
rw [mem_cons, not_or] at h
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a = b ∧ ¬a ∈ l
⊢ List.erase (b :: l) a = b :: l
rw [erase_cons, if_neg (Ne.symm h.1), erase_of_not_mem h.2]