## Stream: maths

### Topic: Lifting a finite set to a finset

#### Ryan Lahfa (Apr 01 2020 at 19:32):

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 (Apr 01 2020 at 19:37):

finset X not finset

#### Ryan Lahfa (Apr 01 2020 at 19:38):

… Thanks, sorry for the stupid question!

#### Kevin Buzzard (Apr 01 2020 at 19:38):

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 (Apr 01 2020 at 19:39):

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

#### Ryan Lahfa (Apr 01 2020 at 19:39):

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

#### Ryan Lahfa (Apr 01 2020 at 19:40):

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 (Apr 01 2020 at 19:41):

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

Last updated: May 10 2021 at 07:15 UTC