(@univ $ perm ι).card = (card ι).factorial

Stream: Is there code for X?

[Eric Wieser]

Library search isn't finding this anyway - does it exist?

import data.fintype.basic
import data.nat.factorial

example {ι : Type*} [fintype ι] (@finset.univ (equiv.perm ι)).card = (fintype.card ι).factorial := sorry

[Kevin Buzzard]

Does it exist for ι = fin n?

[Eric Wieser]

Oh, it's docs#fintype.card_equiv docs#fintype.card_perm

[Eric Wieser]

I guess library_search couldn't unfold perm?

[Shing Tak Lam]

I think fintype.card_perm needs [decidable_eq \iota]?

[Eric Wieser]

I think in my real example I already have that, but now lean is rebuilding the universe so I guess I'll never know

[Eric Wieser]

huh, this is just a library_search quirk - exact fintype.card_perm closed my goal

[Eric Wieser]

Aha, it's docs#finset.card_univ that I was missing

[Rob Lewis]

library_search! will unfold more btw

[Rob Lewis]

Sometiimes that makes the difference.

[Adam Topaz]

@Rob Lewis Should the tactics docs mention this? (It doesn't look like they do at this point). Where does one make PRs for these docs?

[Rob Lewis]

Yes, it definitely should. The doc string for docs#tactic.interactive.library_search does actually mention it, but for some reason there's a shorter version being used for the tactic doc entry.

[Rob Lewis]

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/suggest.lean#L495 is the line that creates the doc entry.

[Rob Lewis]

In this case, the doc string right above that line is the entry. But we should just delete that and use the doc string on the tactic.

[Rob Lewis]

I'll do it.

[Rob Lewis]

#5206