feat(order/rel_iso): generalise several lemmas to assume only has_le …

…not preorder (#5858)

src/order/rel_iso.lean

@@ -491,24 +491,17 @@ end rel_iso
 
 namespace order_iso
 
+section has_le
+
+variables [has_le α] [has_le β] [has_le γ]
+
 /-- Reinterpret an order isomorphism as an order embedding. -/
-def to_order_embedding [has_le α] [has_le β] (e : α ≃o β) : α ↪o β :=
+def to_order_embedding (e : α ≃o β) : α ↪o β :=
 e.to_rel_embedding
 
-@[simp] lemma coe_to_order_embedding [has_le α] [has_le β] (e : α ≃o β) :
+@[simp] lemma coe_to_order_embedding (e : α ≃o β) :
   ⇑(e.to_order_embedding) = e := rfl
 
-variables [preorder α] [preorder β] [preorder γ]
-
-protected lemma monotone (e : α ≃o β) : monotone e := e.to_order_embedding.monotone
-
-protected lemma strict_mono (e : α ≃o β) : strict_mono e := e.to_order_embedding.strict_mono
-
-@[simp] lemma le_iff_le (e : α ≃o β) {x y : α} : e x ≤ e y ↔ x ≤ y := e.map_rel_iff
-
-@[simp] lemma lt_iff_lt (e : α ≃o β) {x y : α} : e x < e y ↔ x < y :=
-e.to_order_embedding.lt_iff_lt
-
 protected lemma bijective (e : α ≃o β) : bijective e := e.to_equiv.bijective
 protected lemma injective (e : α ≃o β) : injective e := e.to_equiv.injective
 protected lemma surjective (e : α ≃o β) : surjective e := e.to_equiv.surjective
@@ -542,8 +535,21 @@ lemma symm_injective : injective (symm : (α ≃o β) → (β ≃o α)) :=
 
 lemma trans_apply (e : α ≃o β) (e' : β ≃o γ) (x : α) : e.trans e' x = e' (e x) := rfl
 
+end has_le
+
 open set
 
+variables [preorder α] [preorder β] [preorder γ]
+
+protected lemma monotone (e : α ≃o β) : monotone e := e.to_order_embedding.monotone
+
+protected lemma strict_mono (e : α ≃o β) : strict_mono e := e.to_order_embedding.strict_mono
+
+@[simp] lemma le_iff_le (e : α ≃o β) {x y : α} : e x ≤ e y ↔ x ≤ y := e.map_rel_iff
+
+@[simp] lemma lt_iff_lt (e : α ≃o β) {x y : α} : e x < e y ↔ x < y :=
+e.to_order_embedding.lt_iff_lt
+
 @[simp] lemma preimage_Iic (e : α ≃o β) (b : β) : e ⁻¹' (Iic b) = Iic (e.symm b) :=
 by { ext x, simp [← e.le_iff_le] }