α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
h₁ : a ∈ l₁
h₂ : ¬a ∈ b :: l₂
⊢ a ∈ List.diff (List.erase l₁ b) l₂
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
h₁ : a ∈ l₁
h₂ : ¬a ∈ b :: l₂
⊢ a ∈ List.diff l₁ (b :: l₂)
rw [diff_cons]
no goals
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
h₁ : a ∈ l₁
h₂ : ¬a ∈ b :: l₂
⊢ a ∈ List.diff (List.erase l₁ b) l₂
exact mem_diff_of_mem ((mem_erase_of_ne <| ne_of_not_mem_cons h₂).2 h₁) (mt (.tail _) h₂)