α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
a : α
⊢ (if a ∈ l₁ then List.diff (List.erase l₁ a) l₂ else List.diff l₁ l₂) = List.diff (List.erase l₁ a) l₂
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
a : α
⊢ List.diff l₁ (a :: l₂) = List.diff (List.erase l₁ a) l₂
simp [List.diff]
no goals
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
a : α
⊢ (if a ∈ l₁ then List.diff (List.erase l₁ a) l₂ else List.diff l₁ l₂) = List.diff (List.erase l₁ a) l₂
split <;> simp [*, erase_of_not_mem]