ι : Type ?u.7883
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x ∈ {y}
ι : Type ?u.7883
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ {x, y} = [x, y]
rw [insert_neg, singleton_eq]
no goals
ι : Type ?u.7883
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x ∈ {y}
rwa [singleton_eq, mem_singleton]