finite set lemmas very hard to use

Stream: general

[Chris Hughes]

A lot of the finite set lemmas are extremely difficult to use. For example set.empty_card can only be used in a rewrite, if I've used fintype_empty as my fintype instance in my goal. Would it be a good idea to make fintype instances an argument to the lemma whenever they're used in the statement of a theorem?

[Kevin Buzzard]

You mean instead of using the type class resolution system?

[Kevin Buzzard]

Let me just comment that if I've understood your question correctly then I had the same problems using the is_ring_hom typeclass and it seemed to me initially that by far the easiest fix was just to make it not a typeclass

[Kevin Buzzard]

but instead I started that typeclass woes thread, and every time I got stuck or frustrated, Mario explained how to do it

[Kevin Buzzard]

Actually on re-reading -- are you asking something else?

[Mario Carneiro]

The solution is to use that fintype is a subsingleton to fix your argument