Finset.card Finset.Univ the same as Fintype.card V?

Stream: new members

[George King]

(I'm new to lean so I apologize if this question is basic)
At the top of my file I declare

variable [Fintype V] [DecidableEq V]

Then at the end of a proof I need the following fact

Finset.card Finset.Univ = Fintype.card V

I.e. the above is given as the goal in the infoview. This seems easy to prove, but I can't write it down. I get an error when writing

have h : Finset.card Finset.Univ = Fintype.card V := by sorry

Lean gives an error ("typeclass instance problem is stuck") when writing out the above line. It seems like Finset.Univ requires a Fintype as input, and then produces the universal set. However, when I pass V as input to Finset.Univ an error is also given ("function expected at Finset.Univ"). So I can't yet write down the statement. The second issue is that refl doesn't work to solve this goal, despite the fact that it seems true by definition.

[Kyle Miller]

With Fintype.univ, you can give it an expected type as a hint, like (Fintype.univ : Finset V)

[Notification Bot]

This topic was moved here from #lean4 > Finset.card Finset.Univ the same as Fintype.card V? by Kyle Miller.

[Kyle Miller]

(@George King This is a fine question. I just moved it over here to "new members")

[Kyle Miller]

This fact must be in mathlib already -- you can use the exact? tactic to try to search for it, if your goal is that fact.

[George King]

Thanks, a type annotation fixed it

[Kyle Miller]

This is actually the definition of Fintype.card, and you can use docs#Finset.card_univ