suggest giving failing exact

Stream: general

[Bolton Bailey]

Mwe below gives an example where suggestgives an exact which then fails. The issue is fixed when I do @card_le_of_subset _ but not @card_le_of_subset or `@card_le_of_subset _ _ so it seems to be that monotone is defined as a quantification over arguments and suggest doesn't know the right number of underscores to put after the @card_le_of_subset.

Would anyone care to elaborate (har!) on why suggest detects this lemma but fails to propose the right amount of elaboration for it?

import data.nat.interval

open finset

example : monotone (@card (finset ℕ)) :=
begin
  -- suggest, -- Try this: exact card_le_of_subset ...
  -- exact card_le_of_subset, -- Invalid type ascription
  apply card_le_of_subset, -- works
end

[Bolton Bailey]

Also: library_search fails but library_search! finds exact card_le_of_subset.

[Kevin Buzzard]

Yeah this does occasionally happen. There might already be an issue for this on GitHub

[Bolton Bailey]

might be issues#5659 Edit: How do I link to a mathlib issue from Zulip? mathlib#5659

[Scott Morrison]

The Lean 3 pretty printer is often wrong; this isn't something specific to exact. If you were to tweak suggest so that it printed things with pp.all true, you'd discover its solution was in fact correct.

[Scott Morrison]

This sort of thing stops being a problem in Lean 4.