no goals
α : Type u_1
l l₁ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₂ : List α
⊢ [] <+ []
rfl
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : a ∈ List.union l₁ l₂
⊢ t ++ l₂ = a :: l₁ ∪ l₂
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : a ∈ l₁ ∪ l₂
⊢ t ++ l₂ = a :: l₁ ∪ l₂
simp only [instUnionList] at h
no goals
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : a ∈ List.union l₁ l₂
⊢ t ++ l₂ = a :: l₁ ∪ l₂
simp only [e, instUnionList, cons_union, insert_of_mem h]
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : ¬a ∈ List.union l₁ l₂
⊢ a :: t ++ l₂ = a :: l₁ ∪ l₂
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : ¬a ∈ l₁ ∪ l₂
⊢ a :: t ++ l₂ = a :: l₁ ∪ l₂
simp only [instUnionList] at h
no goals
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : ¬a ∈ List.union l₁ l₂
⊢ a :: t ++ l₂ = a :: l₁ ∪ l₂
simp only [cons_append, instUnionList, cons_union, e, insert_of_not_mem h]