α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : a ∈ l
⊢ Nodup l
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : a ∈ l
⊢ Nodup (List.insert a l)
rw [insert_of_mem h']
no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : a ∈ l
⊢ Nodup l
exact h
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : ¬a ∈ l
⊢ ¬a ∈ l ∧ Nodup l
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : ¬a ∈ l
⊢ Nodup (List.insert a l)
rw [insert_of_not_mem h', nodup_cons]
no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h : Nodup l
h' : ¬a ∈ l
⊢ ¬a ∈ l ∧ Nodup l
constructor <;> assumption