α : Type u_1
β : Type ?u.103025
γ : Type ?u.103028
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val
α : Type u_1
β : Type ?u.103025
γ : Type ?u.103028
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
⊢ (insert a s).val = dedup (a ::ₘ s.val)
rw [dedup_cons, dedup_eq_self]
no goals
α : Type u_1
β : Type ?u.103025
γ : Type ?u.103028
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val
rfl