case h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
a : α
⊢ List.erase (List.diff l₁ l₂) a = List.diff l₁ (a :: l₂)
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
a : α
⊢ List.diff l₁ (a :: l₂) = List.erase (List.diff l₁ l₂) a
apply Eq.symm
no goals
case h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
a : α
⊢ List.erase (List.diff l₁ l₂) a = List.diff l₁ (a :: l₂)
induction l₂ generalizing l₁ <;> simp [erase_comm, *]