two instances of fintype

Stream: maths

[Casper Putz]

Hi, I have the following code where I explicitely constructed an equivalence between two types α and β → γ, and all types are fintypes. I want to conclude that α.card = γ.card ^ β.card but I have a problem with instances. I would like to something like this:

import data.fintype
open fintype

variables {α : Type*} {β : Type*} {γ : Type*}
variables [fintype α] [fintype β] [fintype γ]
variables [decidable_eq α]
variables (f : α ≃ (β → γ))

example : card α = card γ ^ card β :=
calc card α = @card (β → γ) (of_equiv α f) : eq.symm $ of_equiv_card f
        ... = card γ ^ card β : card_fun

The problem is I have two different instances of fintype (β → γ) . The one coming from fintype.of_equiv (which of_equiv_card uses) and one coming from pi.fintype (which card_fun uses). How could I solve this? Or should I try a completely different route?

[Chris Hughes]

Something like this?

example : card α = card β ^ card γ :=
calc card α = @card (β → γ) (of_equiv α f) : eq.symm $ of_equiv_card f
        ... = card (β → γ) : by congr
        ... = card γ ^ card β : card_fun

[Casper Putz]

Yes! I also needed [decidable_eq β], but then it worked :). Thanks!