feat(Data/SetLike): add more IsConcrete type classes

[martinwintermath]

Add

• IsConcreteEmpty
• HasConcreteUniv
• IsConcreteSingleton
• IsConcreteInsert
• IsConcreteCompl

Zulip: #mathlib4 > More `IsConcrete` classes for `SetLike`

---

[github-actions]

PR summary 99381a425f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ HasConcreteUniv
+ IsConcreteCompl
+ IsConcreteEmpty
+ IsConcreteInsert
+ IsConcreteSingleton
+ coe_compl
+ coe_empty
+ coe_insert
+ coe_singleton
+ coe_univ
+ empty_le
+ empty_ne_univ
+ eq_empty_iff_forall_notMem
+ eq_empty_of_forall_notMem
+ eq_empty_of_le_empty
+ eq_univ_iff_forall
+ eq_univ_of_forall
+ eq_univ_of_le
+ exists_mem_of_nonempty
+ forall_mem_empty
+ le_empty_iff
+ le_eq_empty
+ le_univ
+ lt_univ_iff
+ mem_empty_iff_false
+ ne_univ_iff_exists_notMem
+ not_le_iff_exists_mem_notMem
+ not_univ_le
+ univ
+ univ_le_iff
+ univ_unique

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[vihdzp]

I think we should be using ∅ for only (fin)sets. We should use ⊥ for everything else.

(Ideally I'd prefer using ⊥ always, but that's a conversation for some other time.)

[martinwintermath]

There seem to be some efforts to make set-notation available for objects that behave like sets: see #32983. And it makes sense to me: an IsConcrete-instance expresses that the object behaves, for all practical purpose, like a set. Why distinguish this in notation?

I asked about this here: #mathlib4 > Abstracting the substructure lattice construction @ 💬, if you want to discuss.

[martinwintermath]

Also, ⊥ is context dependent. ∅ really only expresses "the empty set". Why not use it if you really mean it?

(I guess my question is: "why is there set notation if we are not supposed to use it?", but this might be more related to your "conversation for another time".)

[vihdzp]

What #32983 does is ensure that ⊆ gets elaborated as ≤ for these types, which is in line with my comment that we should be primarily employing order notation.

⊥ and ∅ are both context-dependent, but the difference is that we already have swaths of API for ⊥, whereas for ∅ we really just have the Set/Finset API.

[martinwintermath]

What #32983 does is ensure that ⊆ gets elaborated as ≤ for these types, which is in line with my comment that we should be primarily employing order notation.

But it also delaborates the order relation for set-likes as ⊆ (according to my clarification here).

⊥ and ∅ are both context-dependent, but the difference is that we already have swaths of API for ⊥, whereas for ∅ we really just have the Set/Finset API.

But you are probably right: if #32983 continuous as proposed and does the same for other set notations, we will also defeq ∅ and ⊥, and all the bot-API becomes available for ∅. In particular, the IsConcreteEmpty features will already be included in any potential IsConcreteBot or so. But as it stands right now, I need to duplicate if I want to enable both notations.

[vihdzp]

Likewise with univ and ⊤.