Misfiring deprecation

Stream: lean4

[Yaël Dillies]

The following code thinks I'm using the deprecated Finset.card_congr when in fact I'm using the non-deprecated Fintype.card_congr. Is this known?

theorem Fintype.card_congr (_ : False) : True := trivial

namespace Finset

@[deprecated] theorem card_congr : True := trivial

end Finset

open Finset Fintype

/-- warning: `Finset.card_congr` has been deprecated -/
#guard_msgs in
example (h : False) : True := card_congr h

[Yaël Dillies]

Minimised from #12653

[Markus Himmel]

This could be related to lean4#2132

[Damiano Testa]

I'm pretty sure that I have seen this: there was something about deprecate not getting the elaborated information, so Lean uses the correct lemma, but deprecate gets fixated on the other one.

[Mario Carneiro]

See also this TODO

[Ruben Van de Velde]

Did you check if this is still broken on nightly-testing?

[Yaël Dillies]

I did not. Might try later if no one beats me to it