## Stream: Is there code for X?

### Topic: name-hunt: Union_of_singleton?

#### Damiano Testa (Nov 26 2020 at 04:49):

Dear All,

I have been unable to find the lemma below, but I would imagine that it is already in mathlib: do you know what is its name?

On a golfing technique, can you unify the rcases with exact?

Thank you!

import data.set.lattice

lemma setext {α : Type*} (s : set α) : s = ⋃ i : s , {i} :=
begin
--  ext1, simp,  also proves this lemma
ext1 x,
refine ⟨λ hx, set.mem_Union.mpr ⟨⟨x, hx⟩, rfl⟩, λ hx, _⟩,
rcases set.mem_Union.mp hx with ⟨x, _, rfl⟩,
exact subtype.val_prop x,
end


#### Johan Commelin (Nov 26 2020 at 05:32):

-- src/data/set/lattice.lean:438
@[simp] theorem sUnion_singleton (s : set α) : ⋃₀ {s} = s := Sup_singleton


#### Johan Commelin (Nov 26 2020 at 05:32):

atm, you can't combine rcases with exact. And I don't know how to turn it into a syntax that would really save many characters.

#### Kenny Lau (Nov 26 2020 at 07:31):

I don't think that is the theorem he's looking for?

#### Johan Commelin (Nov 26 2020 at 07:33):

Yup, you are totally right

#### Kenny Lau (Nov 26 2020 at 07:34):

import data.set.lattice

lemma setext {α : Type*} (s : set α) : s = ⋃ i : s , {i} :=
set.subset.antisymm (λ i his, set.mem_Union.2 ⟨⟨i, his⟩, rfl⟩) $set.Union_subset$ λ i, set.singleton_subset_iff.2 i.2


#### Damiano Testa (Nov 26 2020 at 08:09):

Dear @Johan Commelin and @Kenny Lau , thank you for your inputs! Kenny's proof works for me! I do not know whether this lemma should be added to data.set.lattice. Do you have an opinion?

#### Eric Wieser (Nov 26 2020 at 08:44):

Should this lemma name contain the word subtype?

#### Eric Wieser (Nov 26 2020 at 09:18):

The non-subtype version is docs#set.bUnion_of_singleton

#### Eric Wieser (Nov 26 2020 at 09:18):

lemma setext {α : Type*} (s : set α) : s = ⋃ (i ∈ s), {i} :=
(set.bUnion_of_singleton s).symm


#### Eric Wieser (Nov 26 2020 at 09:28):

docs#set.Union_of_singleton is also close, but it's missing the coercions

#### Kenny Lau (Nov 26 2020 at 09:47):

@Eric Wieser bad link (set.set.)

#### Eric Wieser (Nov 26 2020 at 09:47):

Zulip needs the same linters as mathlib

#### Damiano Testa (Nov 26 2020 at 10:44):

I do not necessarily insist on this lemma appearing in mathlib. I was simply surprised that it was not. However, it is a lemma that I am using and, so far, I have not been able to make the other suggestions work (except for Kenny's).

#### Eric Wieser (Nov 26 2020 at 10:56):

Perhaps this is the more useful lemma?

lemma set.Union_subtype {α : Type*} (s : set α) (f : α → set α) :
(⋃ (i : s), f i) = ⋃ (i ∈ s), f i :=
set.subset.antisymm
(λ x hx, by {
obtain ⟨i, hi⟩ := set.mem_Union.mp hx,
exact set.mem_Union.mpr ⟨i, set.mem_Union.mpr ⟨i.prop, hi⟩⟩, })
(λ x hx, by {
obtain ⟨i, hi⟩ := set.mem_Union.mp hx,
obtain ⟨hi, hhi⟩ := set.mem_Union.mp hi,
exact set.mem_Union.mpr ⟨⟨i, hi⟩, hhi⟩, })


#### Damiano Testa (Nov 26 2020 at 11:23):

For my actual example, I have not been able to use set.Union_subtype, though this is likely due to the fact that I am not understanding what is going on. I tried applying it with f given by λ i, singleton i and it did not work...

#### Eric Wieser (Nov 26 2020 at 11:55):

lemma setext {α : Type*} (s : set α) : s = ⋃ i : s , {i} :=
by rw [set.Union_subtype, set.bUnion_of_singleton],


#### Damiano Testa (Nov 26 2020 at 14:03):

@Eric Wieser this now works, thank you!

As I only use it once, I do not really have a strong opinion on which form of these lemmas to prefer, nor whether they "should be" in mathlib!

In any case, thank you all for your help!

Last updated: May 07 2021 at 22:14 UTC