feat(*): a few more theorems about unique and subsingleton (#2230)

* feat(*): a few more theorems about `unique` and `subsingleton`

* Fix compile, fix two non-terminate `simp`s

* Update src/topology/metric_space/antilipschitz.lean

This lemma will go to another PR

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: urkud

src/data/equiv/basic.lean

@@ -73,8 +73,8 @@ protected theorem bijective (f : α ≃ β) : bijective f :=
 @[simp] lemma range_eq_univ {α : Type*} {β : Type*} (e : α ≃ β) : set.range e = set.univ :=
 set.eq_univ_of_forall e.surjective
 
-protected theorem subsingleton (e : α ≃ β) : ∀ [subsingleton β], subsingleton α
-| ⟨H⟩ := ⟨λ a b, e.injective (H _ _)⟩
+protected theorem subsingleton (e : α ≃ β) [subsingleton β] : subsingleton α :=
+e.injective.comap_subsingleton
 
 protected def decidable_eq (e : α ≃ β) [H : decidable_eq β] : decidable_eq α
 | a b := decidable_of_iff _ e.injective.eq_iff
@@ -136,8 +136,7 @@ theorem right_inverse_symm (f : equiv α β) : function.right_inverse f.symm f :
 
 def equiv_congr {δ} (ab : α ≃ β) (cd : γ ≃ δ) : (α ≃ γ) ≃ (β ≃ δ) :=
 ⟨ λac, (ab.symm.trans ac).trans cd, λbd, ab.trans $ bd.trans $ cd.symm,
-  assume ac, begin simp [trans_assoc], rw [← trans_assoc], simp end,
-  assume ac, begin simp [trans_assoc], rw [← trans_assoc], simp end, ⟩
+  assume ac, by { ext x, simp }, assume ac, by { ext x, simp } ⟩
 
 def perm_congr {α : Type*} {β : Type*} (e : α ≃ β) : perm α ≃ perm β :=
 equiv_congr e e
@@ -560,7 +559,7 @@ def inhabited_of_equiv [inhabited β] (e : α ≃ β) : inhabited α :=
 ⟨e.symm (default _)⟩
 
 def unique_of_equiv (e : α ≃ β) (h : unique β) : unique α :=
-unique.of_surjective e.symm.surjective
+e.symm.surjective.unique
 
 def unique_congr (e : α ≃ β) : unique α ≃ unique β :=
 { to_fun := e.symm.unique_of_equiv,

src/data/set/basic.lean

@@ -1263,6 +1263,9 @@ lemma subsingleton.eq_empty_or_singleton (hs : s.subsingleton) :
   s = ∅ ∨ ∃ x, s = {x} :=
 s.eq_empty_or_nonempty.elim or.inl (λ ⟨x, hx⟩, or.inr ⟨x, hs.eq_singleton_of_mem hx⟩)
 
+lemma subsingleton_univ [subsingleton α] : (univ : set α).subsingleton :=
+λ x hx y hy, subsingleton.elim x y
+
 theorem univ_eq_true_false : univ = ({true, false} : set Prop) :=
 eq.symm $ eq_univ_of_forall $ classical.cases (by simp) (by simp)
 
@@ -1699,3 +1702,16 @@ ext $ λ ⟨x, hx⟩ , by simp [inclusion]
 end inclusion
 
 end set
+
+namespace subsingleton
+
+variables {α : Type*} [subsingleton α]
+
+lemma eq_univ_of_nonempty {s : set α} : s.nonempty → s = univ :=
+λ ⟨x, hx⟩, eq_univ_of_forall $ λ y, subsingleton.elim x y ▸ hx
+
+@[elab_as_eliminator]
+lemma set_cases {p : set α → Prop} (h0 : p ∅) (h1 : p univ) (s) : p s :=
+s.eq_empty_or_nonempty.elim (λ h, h.symm ▸ h0) $ λ h, (eq_univ_of_nonempty h).symm ▸ h1
+
+end subsingleton

src/logic/unique.lean

@@ -53,13 +53,32 @@ protected lemma subsingleton_unique' : ∀ (h₁ h₂ : unique α), h₁ = h₂
 instance subsingleton_unique : subsingleton (unique α) :=
 ⟨unique.subsingleton_unique'⟩
 
-def of_surjective {f : α → β} (hf : surjective f) [unique α] : unique β :=
+end unique
+
+namespace function
+
+variable {f : α → β}
+
+/-- If the domain of a surjective function is a singleton,
+then the codomain is a singleton as well. -/
+def surjective.unique (hf : surjective f) [unique α] : unique β :=
 { default := f (default _),
-  uniq := λ b,
-  begin
-    cases hf b with a ha,
-    subst ha,
-    exact congr_arg f (eq_default a)
-  end }
+  uniq := λ b, let ⟨a, ha⟩ := hf b in ha ▸ congr_arg f (unique.eq_default _) }
 
-end unique
+/-- If the codomain of an injective function is a subsingleton, then the domain
+is a subsingleton as well. -/
+lemma injective.comap_subsingleton (hf : injective f) [subsingleton β] :
+  subsingleton α :=
+⟨λ x y, hf $ subsingleton.elim _ _⟩
+
+end function
+
+lemma nonempty_unique_or_exists_ne (x : α) : nonempty (unique α) ∨ ∃ y, y ≠ x :=
+classical.by_cases or.inr
+  (λ h, or.inl ⟨{ default := x,
+    uniq := λ y, classical.by_contradiction $ λ hy, h ⟨y, hy⟩ }⟩)
+
+lemma subsingleton_or_exists_ne (x : α) : subsingleton α ∨ ∃ y, y ≠ x :=
+(nonempty_unique_or_exists_ne x).elim
+  (λ ⟨h⟩, or.inl $ @unique.subsingleton _ h)
+  or.inr

src/topology/basic.lean

@@ -134,6 +134,9 @@ by_cases
 lemma is_open_and : is_open {a | p₁ a} → is_open {a | p₂ a} → is_open {a | p₁ a ∧ p₂ a} :=
 is_open_inter
 
+@[simp] lemma subsingleton.is_open [subsingleton α] (s : set α) : is_open s :=
+subsingleton.set_cases is_open_empty is_open_univ s
+
 /-- A set is closed if its complement is open -/
 def is_closed (s : set α) : Prop := is_open (-s)
 
@@ -188,6 +191,9 @@ by rw [this]; exact is_closed_union (is_closed_compl_iff.mpr hp) hq
 lemma is_open_neg : is_closed {a | p a} → is_open {a | ¬ p a} :=
 is_open_compl_iff.mpr
 
+@[simp] lemma subsingleton.is_closed [subsingleton α] (s : set α) : is_closed s :=
+subsingleton.set_cases is_closed_empty is_closed_univ s
+
 /-- The interior of a set `s` is the largest open subset of `s`. -/
 def interior (s : set α) : set α := ⋃₀ {t | is_open t ∧ t ⊆ s}
 

src/topology/metric_space/antilipschitz.lean

@@ -96,6 +96,9 @@ begin
       rwa mul_comm } }
 end
 
+lemma of_subsingleton [subsingleton α] {K : ℝ≥0} : antilipschitz_with K f :=
+λ x y, by simp only [subsingleton.elim x y, edist_self, zero_le]
+
 end antilipschitz_with
 
 lemma lipschitz_with.to_inverse [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β}