name-hunt: Union_of_singleton?

Stream: Is there code for X?

[Damiano Testa]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

Yup, you are totally right

[Kenny Lau]

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]

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]

Should this lemma name contain the word subtype?

[Eric Wieser]

The non-subtype version is docs#set.bUnion_of_singleton

[Eric Wieser]

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

[Eric Wieser]

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

[Kenny Lau]

@Eric Wieser bad link (set.set.)

[Eric Wieser]

Zulip needs the same linters as mathlib

[Damiano Testa]

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]

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]

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]

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

[Damiano Testa]

@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!