API for ExistsUnique

Here we review some of the API provided for ExistsUnique in Mathlib, and provide some additional tools. (Some of these might be suitable for upstreaming to Mathlib.)

existsUnique_of_exists_of_unique.{u_1} {α : Sort u_1} {p : α → Prop} (hex : ∃ x, p x)
  (hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x#check existsUnique_of_exists_of_unique

existsUnique_of_exists_of_unique.{u_1} {α : Sort u_1} {p : α → Prop} (hex : ∃ x, p x)
  (hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x

ExistsUnique.exists.{u_1} {α : Sort u_1} {p : α → Prop} : (∃! x, p x) → ∃ x, p x#check ExistsUnique.exists

ExistsUnique.exists.{u_1} {α : Sort u_1} {p : α → Prop} : (∃! x, p x) → ∃ x, p x

ExistsUnique.unique.{u_1} {α : Sort u_1} {p : α → Prop} (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂#check ExistsUnique.unique

ExistsUnique.unique.{u_1} {α : Sort u_1} {p : α → Prop} (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂

ExistsUnique.intro.{u_1} {α : Sort u_1} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ (y : α), p y → y = w) : ∃! x, p x#check ExistsUnique.intro

ExistsUnique.intro.{u_1} {α : Sort u_1} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ (y : α), p y → y = w) : ∃! x, p x

This implements the axiom of unique choice.

noncomputable def ExistsUnique.choose {α: Sort*} {p: α → Prop} (h : ∃! x, p x) : α := h.exists.choose

              theorem ExistsUnique.choose_spec {α: Sort*} {p: α → Prop} (h : ∃! x, p x) :
  p h.choose := h.exists.choose_spectheorem ExistsUnique.choose_eq {α: Sort*} {p: α → Prop} (h : ∃! x, p x) {x : α} (hx : p x) :
  h.choose = x := h.unique h.choose_spec hxtheorem ExistsUnique.choose_iff {α: Sort*} {p: α → Prop} (h : ∃! x, p x) (x : α):
  p x ↔ x = h.choose :=
  ⟨ byα:Sort u_1p:α → Proph:∃! x, p xx:α⊢ p x → x = h.choose intro hxα:Sort u_1p:α → Proph:∃! x, p xx:αhx:p x⊢ x = h.choose; exact (h.choose_eq hx).symmAll goals completed! 🐙, byα:Sort u_1p:α → Proph:∃! x, p xx:α⊢ x = h.choose → p x rintro rflα:Sort u_1p:α → Proph:∃! x, p x⊢ p h.choose; exact h.choose_specAll goals completed! 🐙 ⟩theorem ExistsUnique.choose_eq_choose {α: Sort*} {p: α → Prop} (h : ∃! x, p x) : Exists.choose h = h.choose := byα:Sort u_1p:α → Proph:∃! x, p x⊢ Exists.choose h = h.choose
  rw [←choose_iff]α:Sort u_1p:α → Proph:∃! x, p x⊢ p (Exists.choose h); exact (Exists.choose_spec h).1All goals completed! 🐙

An alternate form of the axiom of unique choice.

noncomputable def Subsingleton.choose {α: Sort*} [Subsingleton α] [hn: Nonempty α] : α := hn.some

theorem Subsingleton.choose_spec {α: Sort*} [hs: Subsingleton α] [Nonempty α] (x:α) : x = hs.choose := Subsingleton.elim _ _

The equivalence between ExistsUnique and Subsingleton/Nonempty does not require choice.

theorem ExistsUnique.iff_subsingleton_nonempty  {α: Sort*} {p: α → Prop} :
  (∃! x, p x) ↔ (Subsingleton {x // p x} ∧ Nonempty {x // p x}) := byα:Sort u_1p:α → Prop⊢ (∃! x, p x) ↔ Subsingleton { x // p x } ∧ Nonempty { x // p x }
  constructormpα:Sort u_1p:α → Prop⊢ (∃! x, p x) → Subsingleton { x // p x } ∧ Nonempty { x // p x }mprα:Sort u_1p:α → Prop⊢ Subsingleton { x // p x } ∧ Nonempty { x // p x } → ∃! x, p x
  ·mpα:Sort u_1p:α → Prop⊢ (∃! x, p x) → Subsingleton { x // p x } ∧ Nonempty { x // p x } intro hmpα:Sort u_1p:α → Proph:∃! x, p x⊢ Subsingleton { x // p x } ∧ Nonempty { x // p x }; obtain ⟨ x₀, hx₀ ⟩ := h.existsmpα:Sort u_1p:α → Proph:∃! x, p xx₀:αhx₀:p x₀⊢ Subsingleton { x // p x } ∧ Nonempty { x // p x }
    refine ⟨ ⟨ ?_ ⟩, ⟨ _, hx₀ ⟩⟩mpα:Sort u_1p:α → Proph:∃! x, p xx₀:αhx₀:p x₀⊢ ∀ (a b : { x // p x }), a = b
    intro ⟨ x, hx ⟩ ⟨ y, hy ⟩mpα:Sort u_1p:α → Proph:∃! x, p xx₀:αhx₀:p x₀x:αhx:p xy:αhy:p y⊢ ⟨x, hx⟩ = ⟨y, hy⟩
    exact (Subtype.mk.injEq _ _ _ _).symm ▸ (h.unique hx hy)All goals completed! 🐙
  intro ⟨ hsing, ⟨ x₀, hx₀ ⟩ ⟩mprα:Sort u_1p:α → Prophsing:Subsingleton { x // p x }x₀:αhx₀:p x₀⊢ ∃! x, p x
  apply ExistsUnique.intro _ hx₀mprα:Sort u_1p:α → Prophsing:Subsingleton { x // p x }x₀:αhx₀:p x₀⊢ ∀ (y : α), p y → y = x₀; intro y hymprα:Sort u_1p:α → Prophsing:Subsingleton { x // p x }x₀:αhx₀:p x₀y:αhy:p y⊢ y = x₀
  exact Subtype.mk.injEq _ _ _ _ ▸ (hsing.elim ⟨ _, hy ⟩ ⟨ _, hx₀ ⟩)All goals completed! 🐙

'ExistsUnique.iff_subsingleton_nonempty' depends on axioms: [propext]#print axioms ExistsUnique.iff_subsingleton_nonempty

'ExistsUnique.iff_subsingleton_nonempty' depends on axioms: [propext]