coe from `finset.subtype` to `finset`

Stream: Is there code for X?

[Youjack]

Is there such a coercion?

import data.finset.basic

universes u v

variables {α : Type u} (p : α → Prop)
instance : has_coe (finset $ subtype p) (finset α) := sorry

[Yaël Dillies]

No, you're meant to use docs#finset.image or docs#finset.map explicitly.

[Kyle Miller]

Given that there's docs#lift_fn_dom and docs#coe_subtype, it's a little surprising that there's not a has_lift (set {(x : α) // p x}) (set α) instance at least

[Kyle Miller]

I'm going off the existence of docs#lift_list for my mild surprise -- one would expect there were other container types (like set or finset) that have similar has_lift instances.

[Youjack]

I make it with docs#finset.map

import data.finset.basic

universes u v

variables {α : Type u} (p : α → Prop)
instance : has_coe (finset $ subtype p) (finset α) :=
⟨λ s, s.map $ function.embedding.subtype p⟩

[Yakov Pechersky]

I agree with Kyle, a has_lift makes sense for "functor" like containers

[Yaël Dillies]

But then that will need a bunch more API, right?

[Yakov Pechersky]

finset isn't a lawful functor though

[Yakov Pechersky]

I don't think we have any API for lift_list either

[Yaël Dillies]

What should be the coercion from finset {a : α // p a} to set α be?

[Yakov Pechersky]

No default coercion, the same way a has_lift doesn't actually provide a coercion, you have to opt into it

[Yaël Dillies]

Ah, is this just for tactic#lift?

[Kyle Miller]

No, the coercion arrow looks for has_lift instances, and every has_coe instance gives a has_lift instance automatically

[Kyle Miller]

The lift tactic is sort of for going the opposite direction of the coercion arrow, confusingly.

[Alex J. Best]

can_lift is the appropriate class for tactic#lift https://github.com/leanprover-community/mathlib/blob/9cf494e0c4e277137e102249e0d098274ee23081/src/tactic/lift.lean#L22

[Eric Wieser]

I think it's reasonable for the API to just be "↑ is not the simp-normal form, unfold it"