feat(algebra/algebra/subalgebra): subalgebra.subsingleton (#4631)

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

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 α