no goals
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
⊢ List.diff (a :: l₁) l₂ = if a ∈ l₂ then List.diff l₁ (List.erase l₂ a) else a :: List.diff l₁ l₂
induction l₂ generalizing l₁ with
| nil => rfl
| cons b l₂ ih => by_cases h : a = b <;> simp [*, eq_comm]
no goals
case nil
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
⊢ List.diff (a :: l₁) [] = if a ∈ [] then List.diff l₁ (List.erase [] a) else a :: List.diff l₁ []
rfl
no goals
case cons
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), List.diff (a :: l₁) l₂ = if a ∈ l₂ then List.diff l₁ (List.erase l₂ a) else a :: List.diff l₁ l₂
l₁ : List α
⊢ List.diff (a :: l₁) (b :: l₂) =
    if a ∈ b :: l₂ then List.diff l₁ (List.erase (b :: l₂) a) else a :: List.diff l₁ (b :: l₂)
by_cases h : a = b <;> simp [*, eq_comm]