feat(Order/Hom/Basic): OrderEmbedding.id and OrderEmbedding.comp (leanprover-community#38555)

Define `OrderEmbedding.id` and `OrderEmbedding.comp`,
and add missing associativity lemmas for `OrderHom` and `OrderIso`.

Author: SnirBroshi

Mathlib/Order/Hom/Basic.lean

@@ -350,6 +350,9 @@ theorem id_comp (f : α →o β) : comp id f = f := by
   ext
   rfl
 
+theorem comp_assoc (f : γ →o δ) (g : β →o γ) (h : α →o β) : (f.comp g).comp h = f.comp (g.comp h) :=
+  rfl
+
 /-- Constant function bundled as an `OrderHom`. -/
 @[simps -fullyApplied]
 def const (α : Type*) [Preorder α] {β : Type*} [Preorder β] : β →o α →o β where
@@ -558,6 +561,49 @@ theorem RelEmbedding.orderEmbeddingOfLTEmbedding_apply [PartialOrder α] [Partia
 
 namespace OrderEmbedding
 
+section LE
+
+variable [LE α] [LE β] [LE γ] [LE δ]
+
+variable (α) in
+/-- Identity order embedding -/
+abbrev id : α ↪o α :=
+  RelEmbedding.refl (· ≤ ·)
+
+@[simp]
+theorem coe_id : ⇑(id α) = _root_.id :=
+  rfl
+
+@[simp]
+theorem id_toEmbedding : (id α).toEmbedding = Function.Embedding.refl α :=
+  rfl
+
+/-- Composition of two order embeddings is an order embedding -/
+abbrev comp (f : α ↪o β) (g : β ↪o γ) : α ↪o γ :=
+  RelEmbedding.trans f g
+
+@[simp]
+theorem coe_comp (f : α ↪o β) (g : β ↪o γ) : f.comp g = g ∘ f :=
+  rfl
+
+@[simp]
+theorem id_comp (f : α ↪o β) : (id α).comp f = f := by
+  ext
+  rfl
+
+@[simp]
+theorem comp_id (f : α ↪o β) : f.comp (id β) = f := by
+  ext
+  rfl
+
+theorem comp_assoc (f : α ↪o β) (g : β ↪o γ) (h : γ ↪o δ) :
+    (f.comp g).comp h = f.comp (g.comp h) :=
+  rfl
+
+end LE
+
+section Preorder
+
 variable [Preorder α] [Preorder β] (f : α ↪o β)
 
 /-- `<` is preserved by order embeddings of preorders. -/
@@ -658,6 +704,8 @@ def toOrderHom {X Y : Type*} [Preorder X] [Preorder Y] (f : X ↪o Y) : X →o Y
 @[simp, norm_cast]
 lemma coe_ofIsEmpty [IsEmpty α] : (ofIsEmpty : α ↪o β) = (isEmptyElim : α → β) := rfl
 
+end Preorder
+
 end OrderEmbedding
 
 section Disjoint
@@ -716,7 +764,7 @@ namespace OrderIso
 
 section LE
 
-variable [LE α] [LE β] [LE γ]
+variable [LE α] [LE β] [LE γ] [LE δ]
 
 instance : EquivLike (α ≃o β) α β :=
   inferInstance
@@ -851,6 +899,10 @@ theorem self_trans_symm (e : α ≃o β) : e.trans e.symm = OrderIso.refl α :=
 theorem symm_trans_self (e : α ≃o β) : e.symm.trans e = OrderIso.refl β :=
   RelIso.symm_trans_self e
 
+theorem trans_assoc (f : α ≃o β) (g : β ≃o γ) (h : γ ≃o δ) :
+    (f.trans g).trans h = f.trans (g.trans h) :=
+  rfl
+
 /-- An order isomorphism between the domains and codomains of two prosets of
 order homomorphisms gives an order isomorphism between the two function prosets. -/
 @[simps apply symm_apply]