case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <+~ a :: List.erase l a

case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <+~ a :: List.erase l a
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <+~ a :: List.erase l a
by_cases h : a ∈ l
no goals
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <+~ a :: List.erase l a
exact (perm_cons_erase h).subperm
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <+~ a :: l
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <+~ a :: List.erase l a
rw [erase_of_not_mem h]
no goals
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <+~ a :: l
exact (sublist_cons _ _).subperm