feat(order/preorder_hom): preorder_hom_eq_id (#8135)

From LTE

Author: jcommelin

src/order/preorder_hom.lean

@@ -65,6 +65,15 @@ by { ext, refl }
 def subtype.val (p : α → Prop) : subtype p →ₘ α :=
 ⟨subtype.val, λ x y h, h⟩
 
+-- TODO[gh-6025]: make this a global instance once safe to do so
+/-- There is a unique monotone map from a subsingleton to itself. -/
+local attribute [instance]
+def unique [subsingleton α] : unique (α →ₘ α) :=
+{ default := preorder_hom.id, uniq := λ a, ext _ _ (subsingleton.elim _ _) }
+
+lemma preorder_hom_eq_id [subsingleton α] (g : α →ₘ α) : g = preorder_hom.id :=
+subsingleton.elim _ _
+
 /-- The preorder structure of `α →ₘ β` is pointwise inequality: `f ≤ g ↔ ∀ a, f a ≤ g a`. -/
 instance : preorder (α →ₘ β) :=
 preorder.lift preorder_hom.to_fun