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

case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a = b
⊢ List.erase (a :: l) b <+~ a :: List.erase l b
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ List.erase (a :: l) b <+~ a :: List.erase l b
by_cases h : a = b
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ List.erase (a :: l) a <+~ a :: List.erase l a
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
h : a = b
⊢ List.erase (a :: l) b <+~ a :: List.erase l b
subst b
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <+~ a :: List.erase l a
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ List.erase (a :: l) a <+~ a :: List.erase l a
rw [erase_cons_head]
no goals
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <+~ a :: List.erase l a
apply subperm_cons_erase
no goals
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a = b
⊢ List.erase (a :: l) b <+~ a :: List.erase l b
rw [erase_cons_tail _ h]