α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ eraseP (fun b => decide (a = b)) l₁ <+ eraseP (fun b => decide (a = b)) l₂
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ List.erase l₁ a <+ List.erase l₂ a
simp only [erase_eq_eraseP]
no goals
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ eraseP (fun b => decide (a = b)) l₁ <+ eraseP (fun b => decide (a = b)) l₂
exact h.eraseP