## Stream: general

### Topic: cardinal

#### orlando (May 03 2020 at 00:13):

Hello, I have a problem :grinning_face_with_smiling_eyes:

Do you have an idea ?

import data.fintype.basic
example (X : Type)[fintype X][decidable_eq X]  : fintype.card ({x : X | true }) = fintype.card X := begin
-- I don't understand why i'm always dealing with this kind of thing ???

end


#### Kevin Buzzard (May 03 2020 at 00:16):

Is there something like fintype.card_univ?

#### Yury G. Kudryashov (May 03 2020 at 00:22):

1. Open fintype/basic
2. Search for card.

#### Reid Barton (May 03 2020 at 00:23):

fintype.card_congr \$ equiv.set.univ X

#### Kevin Buzzard (May 03 2020 at 00:24):

Would a hammer have found this?

#### Reid Barton (May 03 2020 at 00:24):

I found the second part by library_search

#### Reid Barton (May 03 2020 at 00:25):

Good question though.

#### Kevin Buzzard (May 03 2020 at 00:30):

After a while you learn how to use a type and you pick up sufficiently many tricks that you can solve problems like this yourself. I think I can solve most trivial-to-mathematician questions about natin Lean now.

#### orlando (May 03 2020 at 01:16):

thx @Reid Barton !
It's ok ! But I have a problem, i think, in my calculus,  card  is calculate in a ring  R  and not in  nat  ... or i don't know that strange :confused:

Rt : ↑(card ↥{x : G | true}) = ↑(card G)
⊢ ↑(card ↥{x : G | true}) = ↑(card G)    --- not the same ↑  and i don't understand for the moment !


I try to isolate the problem tomorow !

#### Yury G. Kudryashov (May 03 2020 at 01:22):

One of these should work:

1. rw [fintype.card_congr (equiv.set.univ α)].
2. congr, then exact fintype.card_congr (equiv.set.univ α).

#### Yury G. Kudryashov (May 03 2020 at 01:22):

(I think that both should work but didn't test)

#### orlando (May 03 2020 at 02:24):

good : i don't understand why but  apply fintype.card_congr, exact equiv.set.univ G,  work the other proposition doesn't work in my context !

thx @Yury G. Kudryashov and @Reid Barton and @Kevin Buzzard ... i can sleep now :sweat_smile:

Last updated: May 14 2021 at 05:20 UTC