case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
l : List α
⊢ List.insert x (List.insert y l) ~ List.insert y (List.insert x l)
by_cases xl : x ∈ l <;> by_cases yl : y ∈ l <;> simp [xl, yl]
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : x = y
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)

case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : ¬x = y
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)
by_cases xy : x = y
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : ¬x = y
⊢ x :: y :: l ~ y :: x :: l
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : ¬x = y
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)
simp [List.insert, xl, yl, xy, Ne.symm xy]
no goals
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : ¬x = y
⊢ x :: y :: l ~ y :: x :: l
constructor
no goals
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : x = y
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)
simp [xy]