no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
⊢ List.erase (b :: l) a = eraseP (fun b => decide (a = b)) (b :: l)
if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP a l]
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : a = b
⊢ List.erase (b :: l) a = eraseP (fun b => decide (a = b)) (b :: l)
simp [h]
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a = b
⊢ List.erase (b :: l) a = eraseP (fun b => decide (a = b)) (b :: l)
simp [h, Ne.symm h, erase_eq_eraseP a l]