Lifting a finite set to a finset

Stream: maths

[Ryan Lahfa]

I'm trying to lift a finite set to a finset using some hypothesis of finiteness.

import data.set
import data.set.finite
import data.finset

variable {X: Type}

open set
open classical
local attribute [instance] prop_decidable

set_option trace.app_builder true

lemma finite_set_has_greatest_element [preorder X] (S: set X):
  S.finite → ∃ x ∈ S, is_greatest S x := begin
  intro Hf,
  lift S to finset using Hf,
  end

But this is failing with:

[app_builder] failed to create an 'can_lift'-application, failed to solve unification constraint for #2 argument (Type ? =?= Type ? → Type ?)
app_builder_exception, more information can be obtained using command `set_option trace.app_builder true`

But, I'm not sure I understand why https://leanprover-community.github.io/mathlib_docs/data/set/finite.html#set.can_lift does not get picked up by Lean.

[Kevin Buzzard]

finset X not finset

[Ryan Lahfa]

… Thanks, sorry for the stupid question!

[Kevin Buzzard]

Thanks for that question! I had no idea about that whole machinery. I remember noticing that some trick to go from int to nat landed in Lean but I'd not realised it was so powerful.

[Kevin Buzzard]

I just learnt about how far it all went from your question.

[Ryan Lahfa]

Happy to make this very cool API more attention then, because it sounds really useful for heavy coercions :)

[Ryan Lahfa]

I guessed that lift S to finset using Hf could guess that finset has some holes and fill them itself by reusing the fact that S: set α and then trying to make some finset α too, but it's not obvious I guess

[Ryan Lahfa]

Putting a hole, i.e. lift S to (finset _) using Hf makes the error a lot more user friendly.