no goals
α : Type uu
β : Type vv
l₁✝ l₂ : List α
inst✝ : DecidableEq α
a : α
l₁ : List α
⊢ ∃ x, a :: l₁ <+ a :: List.diff l₁ []
simp
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
⊢ List.diff (List.erase (a :: l₁) b) l₂ <+~ a :: List.diff (List.erase l₁ b) l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
⊢ List.diff (a :: l₁) (b :: l₂) <+~ a :: List.diff l₁ (b :: l₂)
simp only [diff_cons]
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
⊢ List.diff (a :: List.erase l₁ b) l₂ <+~ a :: List.diff (List.erase l₁ b) l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
⊢ List.diff (List.erase (a :: l₁) b) l₂ <+~ a :: List.diff (List.erase l₁ b) l₂
refine' ((erase_cons_subperm_cons_erase a b l₁).diff_right l₂).trans _
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
⊢ List.diff (a :: List.erase l₁ b) l₂ <+~ a :: List.diff (List.erase l₁ b) l₂
apply subperm_cons_diff