instSetLikeOpens

Stream: mathlib4

[Winston Yin (尹維晨)]

I would've expected the following SetLike coercion to work, but it doesn't:

import Mathlib.Topology.Sets.Opens

variable {α : Type*} [TopologicalSpace α] (s : TopologicalSpace.Opens α)
#check Set.Nonempty s # application type mismatch
#check Set.Nonempty (s : Set α) # works

Should I not have expected this behaviour?

[Kyle Miller]

This doesn't work:

#check Set.Nonempty (s : Set _)

I suspect this is related to why the first #check isn't working.

[Winston Yin (尹維晨)]

But shouldn't that work?

[Kevin Buzzard]

I believe this is a standard and really annoying problem: Lean doesn't know which Set X the coercion is supposed to land in. In lean 3 this would fail for s : Finset alpha too. Does it still fall in lean 4?

[Kevin Buzzard]

Winston Yin (尹維晨) said:

But shouldn't that work?

The point is that there might be a coercion to some Set beta for some other beta so I think lean won't just assume it's Set alpha you mean.

[Winston Yin (尹維晨)]

I see. Slightly disappointing but no big deal.

[Emilie (Shad Amethyst)]

Isn't that something that @[default_instance] is supposed to solve?