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