Membership of small finset

Stream: new members

[Justus Springer]

What's the idiomatic way of solving problems like these? Is there a tactic that can do this?

import data.finset.basic

example : 7 ∈ ({1, 2, 3, 4, 5, 6, 7, 8} : finset ℕ) :=
begin
  right, right, right, right, right, right, left, refl,
end

[Kevin Buzzard]

norm_num

[Justus Springer]

Wow, it works even for types other than ℕ. Thanks!

[Justus Springer]

I didn't expect that, I thought norm_num only proves stuff about numbers.

[Kevin Buzzard]

yeah, this is some kind of relatively recent plugin which Mario wrote for it I think.

[Eric Rodriguez]

Why use norm_num over dec_trivial?

[Kevin Buzzard]

I don't believe in decidability.

[Mario Carneiro]

norm_num doesn't know anything about this problem, but it calls simp using norm_num to discharge side goals

[Mario Carneiro]

in fact, I think simp alone will do this