exists and forall in subsingleton

Stream: Is there code for X?

[Devon Tuma]

Is there already some lemma that directly gives:

lemma forall_iff_of_subsingleton_of_inhabited {α : Type*} [subsingleton α] [inhabited α]
  (p : α → Prop) : (∀ x, p x) ↔ p (arbitrary α) :=
⟨λ h, h $ arbitrary α, λ h, (λ x, subsingleton.elim (arbitrary α) x ▸ h)⟩

lemma exists_iff_of_subsingleton_of_inhabited {α : Type*} [subsingleton α] [inhabited α]
  (p : α → Prop) : (∃ x, p x) ↔ p (arbitrary α) :=
⟨λ h, let ⟨x, h⟩ := h in (subsingleton.elim x (arbitrary α) ▸ h), λ h, ⟨arbitrary α, h⟩⟩

the second is technically equivalent to subsingleton.mem_iff_nonempty.symm when the compiler expands the term out, but I haven't found the first one at all.

[Patrick Johnson]

I don't think the first one is in mathlib. Note that arbitrary α can be generalized to any x : α and then [inhabited α] is redundant:

lemma subsingleton.forall_iff {α : Type*} [subsingleton α]
  {p : α → Prop} {x : α} : (∀ y, p y) ↔ p x :=
⟨λ h, h x, λ h y, subsingleton.elim x y ▸ h⟩

lemma subsingleton.exists_iff {α : Type*} [subsingleton α]
  {p : α → Prop} {x : α} : (∃ y, p y) ↔ p x :=
subsingleton.mem_iff_nonempty.symm

[Kyle Miller]

@Patrick Johnson I think the point of formulating this with inhabited is that you can rewrite without creating any new goals, but your version could be useful if x were explicit.

[Eric Wieser]

Note that [inhabited X] [subsingleton X] is usually spelt [unique X]

[Violeta Hernández]

docs#unique.exists_iff and docs#unique.forall_iff