exact? suggests "Tactic."

Stream: mathlib4

[Alex Meiburg]

import Mathlib
example [Nonempty α] [Fintype α] : 0 < Finset.univ.card (α := α) :=
  by exact?

gives

Try this: exact Tactic.card_univ_pos α

but

example [Nonempty α] [Fintype α] : 0 < Finset.univ.card (α := α) :=
  by exact Tactic.card_univ_pos α

gives

unknown identifier 'Tactic.card_univ_pos'

[Damiano Testa]

It seems that exact? find private theorems:

Mathlib/Data/Fintype/Card.lean:1302:private theorem card_univ_pos (α : Type*) [Fintype α] [Nonempty α] :

[Matthew Ballard]

(Perfect time for a chrome incognito emoji)

[Alex Meiburg]

Raises question of why that theorem is private :thinking:

[Damiano Testa]

I think that you "should" be using docs#Finite.card_pos, that uses Prop-valued assumptions, rather than Type-valued ones.

[Damiano Testa]

Nevertheless, this exact? behaviour seems suboptimal...

[Kyle Miller]

Alex Meiburg said:

Raises question of why that theorem is private :thinking:

Easy answer: it used to be for a positivity extension, but that extension is currently commented out since it was never ported. It's good practice for tactics to restate all theorems that they use, rather than referring to global theorems, since that reduces the risk of refactors breaking the assumptions in the metaprograms. The Qq library does help a bit with reducing this risk.

[Kyle Miller]

It's wrapping up Finset.univ_nonempty.card_pos, which is already in the library, and which is what exact? ought to give you.

[Kim Morrison]

Alex Meiburg said:

import Mathlib
example [Nonempty α] [Fintype α] : 0 < Finset.univ.card (α := α) :=
  by exact?

gives

Try this: exact Tactic.card_univ_pos α

but

example [Nonempty α] [Fintype α] : 0 < Finset.univ.card (α := α) :=
  by exact Tactic.card_univ_pos α

gives

unknown identifier 'Tactic.card_univ_pos'

This is already fixed on nightly-testing, so should come good when we release v4.8.0-rc1.

[Kim Morrison]

(Also, just noting how autoImplicit fragmentation causes a problem: this is a fine MWE in a downstream project that doesn't turn off autoImplicits, but can't be copied and pasted as is into Mathlib...)

[Mario Carneiro]

to be fair it also can't be copied and pasted as is into mathlib because it uses import Mathlib

[Kevin Buzzard]

It can be copied and pasted into Mathlib/scratch.lean