case pos
α : Type u_1
β : Type ?u.53447
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l

case neg
α : Type u_1
β : Type ?u.53447
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l
α : Type u_1
β : Type ?u.53447
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <:+ List.insert a l
by_cases h : a ∈ l
no goals
case pos
α : Type u_1
β : Type ?u.53447
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l
simp only [insert_of_mem h, insert, suffix_refl]
no goals
case neg
α : Type u_1
β : Type ?u.53447
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l
simp only [insert_of_not_mem h, suffix_cons, insert]