nonempty and set.nonempty

Stream: new members

[Heather Macbeth]

Am I supposed to be able to get set.nonempty from a set whose subtype is nonempty, without using classical (for classical.inhabited_of_nonempty or similar)? Please tell me how, if so!

import data.set.basic

example {α : Type*} {s : set α} (hs : s.nonempty) : nonempty s := set.nonempty.to_subtype hs

example {α : Type*} (s : set α) [inhabited s] : s.nonempty := ⟨(default s).1, (default s).2⟩

-- is this true?
example {α : Type*} (s : set α) [nonempty s] : s.nonempty := sorry

[Adam Topaz]

Here's a bad and non-golfed proof:

import data.set.basic

example {α : Type*} {s : set α} (hs : s.nonempty) : nonempty s := set.nonempty.to_subtype hs

example {α : Type*} (s : set α) [inhabited s] : s.nonempty := ⟨(default s).1, (default s).2⟩

-- is this true?
example {α : Type*} (s : set α) (I : nonempty s) : s.nonempty :=
begin
  tactic.unfreeze_local_instances,
  induction I,
  use I,
  exact I.2
end

[Adam Topaz]

So at least it's true :)

[Yakov Pechersky]

example {α : Type*} (s : set α) [nonempty s] : s.nonempty :=
begin
  rw set.nonempty_def,
  rw ←nonempty_subtype,
  assumption
end

[Adam Topaz]

Much better!

[Yakov Pechersky]

Found by two suggests

[Yakov Pechersky]

Golfed:

example {α : Type*} (s : set α) [nonempty s] : s.nonempty :=
set.nonempty_def.mpr (nonempty_subtype.mp ‹_›)

[Heather Macbeth]

Can you PR it? :). At least I assume it should be PR'd, it's so fundamental that perhaps it's been omitted for some good reason?

[Heather Macbeth]

Also, this seems to work:

example {α : Type*} (s : set α) [nonempty s] : s.nonempty := nonempty_subtype.mp ‹_›

[Heather Macbeth]

So maybe no need for a PR :)

[Yakov Pechersky]

#5373 too late =)