α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ length (eraseP (fun b => decide (a = b)) l) = pred (length l)
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ length (List.erase l a) = pred (length l)
rw [erase_eq_eraseP]
no goals
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ length (eraseP (fun b => decide (a = b)) l) = pred (length l)
exact length_eraseP_of_mem h (decide_eq_true rfl)