Finset.le_eq_subset

Stream: mathlib4

[Yury G. Kudryashov]

Here is an #mwe:

import Mathlib.Data.Finset.Basic

example (s : Finset ℕ) : Finset.coeEmb s = s := by simp -- works
example (s : Finset ℕ) : Finset.coeEmb.1 s = s := by simp -- fails

[Yury G. Kudryashov]

Why it fails

In the first case, LE.le is not applied, so it doesn't get simplified to HasSubset.Subset. In the second case, docs#RelEmbedding.coe_toEmbedding turns it into (fun a b => a ≤ b) which gets simplified to fun a b => a ⊆ b, so docs#Finset.coe_coeEmb no longer applies.

[Yury G. Kudryashov]

What should we do about it?

[Yury G. Kudryashov]

I would prefer to get rid of ⊆ for sets and finsets but I was told that it's bad for pedagogical reasons.

[Antoine Chambert-Loir]

I agree that it is a burden to have to rewrite subset as le or the other way round. Is it possible to have subset be just notation for le?

[Yaël Dillies]

Yes, Kyle and I have some work towards it

[Yaël Dillies]

but I won't have time to finish it before this summer

[Antoine Chambert-Loir]

Can't you delegate some things from the big plate you seem to have? Nobody's too young to suffer burn out, but still...

[Yaël Dillies]

Go wild :smile: :point_down:
Kyle Miller said:

Here's an experiment with what we talked about in Bonn regarding Set using lattice operations but pretty printing using set notation: https://github.com/leanprover-community/mathlib4/tree/kmill_set_use_lattice