chore(order/rel_iso): rename order_embedding.of_map_rel_iff to `of_…

…map_le_iff` (#8839)

The old name comes from `rel_embedding`.

src/data/list/nodup_equiv_fin.lean

@@ -87,7 +87,7 @@ begin
   have : some hd = _ := hf 0,
   rw [eq_comm, list.nth_eq_some] at this,
   obtain ⟨w, h⟩ := this,
-  let f' : ℕ ↪o ℕ := order_embedding.of_map_rel_iff (λ i, f (i + 1) - (f 0 + 1))
+  let f' : ℕ ↪o ℕ := order_embedding.of_map_le_iff (λ i, f (i + 1) - (f 0 + 1))
     (λ a b, by simp [nat.sub_le_sub_right_iff, nat.succ_le_iff, nat.lt_succ_iff]),
   have : ∀ ix, tl.nth ix = (l'.drop (f 0 + 1)).nth (f' ix),
   { intro ix,
@@ -114,7 +114,7 @@ begin
       refine ⟨f.trans (order_embedding.of_strict_mono (+ 1) (λ _, by simp)), _⟩,
       simpa using hf },
     { obtain ⟨f, hf⟩ := IH,
-      refine ⟨order_embedding.of_map_rel_iff
+      refine ⟨order_embedding.of_map_le_iff
         (λ (ix : ℕ), if ix = 0 then 0 else (f ix.pred).succ) _, _⟩,
       { rintro ⟨_|a⟩ ⟨_|b⟩;
         simp [nat.succ_le_succ_iff] },
@@ -143,7 +143,7 @@ begin
       rw [nth_le_nth hi, eq_comm, nth_eq_some] at hf,
       obtain ⟨h, -⟩ := hf,
       exact h },
-    refine ⟨order_embedding.of_map_rel_iff (λ ix, ⟨f ix, h ix.is_lt⟩) _, _⟩,
+    refine ⟨order_embedding.of_map_le_iff (λ ix, ⟨f ix, h ix.is_lt⟩) _, _⟩,
     { simp },
     { intro i,
       apply option.some_injective,

src/order/rel_iso.lean

@@ -377,17 +377,17 @@ protected def dual : order_dual α ↪o order_dual β :=
 To define an order embedding from a partial order to a preorder it suffices to give a function
 together with a proof that it satisfies `f a ≤ f b ↔ a ≤ b`.
 -/
-def of_map_rel_iff {α β} [partial_order α] [preorder β] (f : α → β)
+def of_map_le_iff {α β} [partial_order α] [preorder β] (f : α → β)
   (hf : ∀ a b, f a ≤ f b ↔ a ≤ b) : α ↪o β :=
 rel_embedding.of_map_rel_iff f hf
 
-@[simp] lemma coe_of_map_rel_iff {α β} [partial_order α] [preorder β] {f : α → β} (h) :
-  ⇑(of_map_rel_iff f h) = f := rfl
+@[simp] lemma coe_of_map_le_iff {α β} [partial_order α] [preorder β] {f : α → β} (h) :
+  ⇑(of_map_le_iff f h) = f := rfl
 
 /-- A strictly monotone map from a linear order is an order embedding. --/
 def of_strict_mono {α β} [linear_order α] [preorder β] (f : α → β)
   (h : strict_mono f) : α ↪o β :=
-of_map_rel_iff f (λ _ _, h.le_iff_le)
+of_map_le_iff f (λ _ _, h.le_iff_le)
 
 @[simp] lemma coe_of_strict_mono {α β} [linear_order α] [preorder β] {f : α → β}
   (h : strict_mono f) : ⇑(of_strict_mono f h) = f := rfl