From 82ff1e561b6018ed5b6cb5cda6d3a76fb99c174f Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Sat, 17 Oct 2020 18:25:57 +0000
Subject: [PATCH] feat(algebra/algebra/subalgebra): subalgebra.subsingleton
 (#4631)

---
 src/algebra/algebra/subalgebra.lean | 10 ++++++++++
 src/order/bounded_lattice.lean      |  6 +++++-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/algebra/algebra/subalgebra.lean b/src/algebra/algebra/subalgebra.lean
index 18e1a54463683..1c406eec30af5 100644
--- a/src/algebra/algebra/subalgebra.lean
+++ b/src/algebra/algebra/subalgebra.lean
@@ -376,6 +376,7 @@ bot_equiv_of_injective (ring_hom.injective _)
 end algebra
 
 namespace subalgebra
+open algebra
 
 variables {R : Type u} {A : Type v}
 variables [comm_semiring R] [semiring A] [algebra R A]
@@ -384,6 +385,15 @@ variables (S : subalgebra R A)
 lemma range_val : S.val.range = S :=
 ext $ set.ext_iff.1 $ S.val.coe_range.trans subtype.range_val
 
+instance : unique (subalgebra R R) :=
+{ uniq :=
+  begin
+    intro S,
+    refine le_antisymm (λ r hr, _) bot_le,
+    simp only [set.mem_range, coe_bot, id.map_eq_self, exists_apply_eq_apply, default],
+  end
+  .. algebra.inhabited }
+
 end subalgebra
 
 section nat
diff --git a/src/order/bounded_lattice.lean b/src/order/bounded_lattice.lean
index 187f7f3fdf7ab..60c85bdccfe32 100644
--- a/src/order/bounded_lattice.lean
+++ b/src/order/bounded_lattice.lean
@@ -392,9 +392,13 @@ lemma eq_top_of_bot_eq_top {α : Type*} [bounded_lattice α] (hα : (⊥ : α) =
   x = (⊤ : α) :=
 eq_top_mono bot_le hα
 
+lemma subsingleton_of_top_le_bot {α : Type*} [bounded_lattice α] (h : (⊤ : α) ≤ (⊥ : α)) :
+  subsingleton α :=
+⟨λ a b, le_antisymm (le_trans le_top $ le_trans h bot_le) (le_trans le_top $ le_trans h bot_le)⟩
+
 lemma subsingleton_of_bot_eq_top {α : Type*} [bounded_lattice α] (hα : (⊥ : α) = (⊤ : α)) :
   subsingleton α :=
-⟨λ a b, by rw [eq_bot_of_bot_eq_top hα a, eq_bot_of_bot_eq_top hα b]⟩
+subsingleton_of_top_le_bot (ge_of_eq hα)
 
 /-- Attach `⊥` to a type. -/
 def with_bot (α : Type*) := option α