Subset equal {0} of Subsingleton

Stream: Is there code for X?

[Xavier Roblot]

I could not find the following results:

import Mathlib.Data.Set.Basic

variable {α : Type*} [Subsingleton α] (s : Set α) [h : Nonempty s]

theorem Set.subset_eq_of_subsingleton (a : α) : s = {a} := by
  refine Set.subsingleton_of_subsingleton.eq_singleton_of_mem ?_
  obtain ⟨⟨x, hx⟩⟩ := (inferInstance : Nonempty s)
  rwa [← Subsingleton.elim a x] at hx

theorem Set.subset_eq_zero_of_subsingleton [Zero α] : s = {0} := Set.subset_eq_of_subsingleton s 0

theorem Set.subset_eq_one_of_subsingleton [One α] : s = {1} := Set.subset_eq_of_subsingleton s 1

Is it something that should be added to Mathlib?

[Eric Rodriguez]

yes, also maybe a version for Unique/default

[Ruben Van de Velde]

import Mathlib

section
variable {α : Type*} [Unique α] {s : Set α} (h : s.Nonempty)

theorem Set.Nonempty.eq_singleton_of_nonempty : s = {default} := by
  refine (Nonempty.subset_singleton_iff h).mp ?_
  intro x _
  simp [Unique.uniq _ x]

theorem Set.Nonempty.eq_singleton_zero_of_nonempty [Zero α] : s = {0} := by convert Set.Nonempty.eq_singleton_of_nonempty h

theorem Set.Nonempty.eq_singleton_one_of_nonempty [One α] : s = {1} := by convert Set.Nonempty.eq_singleton_of_nonempty h

end

variable {α : Type*} [Subsingleton α] {s : Set α} (h : s.Nonempty)

noncomputable def uniqueOfNonempty : Unique α := uniqueOfSubsingleton h.choose

theorem Set.Nonempty.eq_singleton_of_nonempty_of_subsingleton :
    letI := uniqueOfNonempty h
    s = {default} := by
  letI := uniqueOfNonempty h
  exact h.eq_singleton_of_nonempty

theorem Set.subset_eq_of_subsingleton (a : α) : s = {a} := by
  rw [h.eq_singleton_of_nonempty_of_subsingleton, Unique.uniq _ a]

theorem Set.subset_eq_zero_of_subsingleton [Zero α] : s = {0} := Set.subset_eq_of_subsingleton h 0

theorem Set.subset_eq_one_of_subsingleton [One α] : s = {1} := Set.subset_eq_of_subsingleton h 1

[Xavier Roblot]

Thanks. Can you go ahead and PR your more complete version?

[Ruben Van de Velde]

I don't have time for it right now, but feel free to reuse my code :)

[Xavier Roblot]

#8423