no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b = a
⊢ List.erase (b :: l) a = if b = a then l else b :: List.erase l a
simp [List.erase, h]
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬b = a
⊢ List.erase (b :: l) a = if b = a then l else b :: List.erase l a
simp [List.erase, h, (beq_eq_false_iff_ne _ _).2 h]