From 0aa6aed99743ca5c58c7dda085a71328fafa7175 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 2 Nov 2020 14:44:02 +0000
Subject: [PATCH] chore(order/basic): move `strict_mono_coe`to `subtype` NS
 (#4870)

Also add `subtype.mono_coe`
---
 src/order/basic.lean                          |  6 +++++-
 src/order/conditionally_complete_lattice.lean | 16 ++++++++--------
 2 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/order/basic.lean b/src/order/basic.lean
index 3cfd352996eb7..757e75014897d 100644
--- a/src/order/basic.lean
+++ b/src/order/basic.lean
@@ -399,7 +399,11 @@ partial_order.lift subtype.val subtype.val_injective
 instance subtype.linear_order {α} [linear_order α] (p : α → Prop) : linear_order (subtype p) :=
 linear_order.lift subtype.val subtype.val_injective
 
-lemma strict_mono_coe [preorder α] (t : set α) : strict_mono (coe : (subtype t) → α) := λ x y, id
+lemma subtype.mono_coe [preorder α] (t : set α) : monotone (coe : (subtype t) → α) :=
+λ x y, id
+
+lemma subtype.strict_mono_coe [preorder α] (t : set α) : strict_mono (coe : (subtype t) → α) :=
+λ x y, id
 
 instance prod.has_le (α : Type u) (β : Type v) [has_le α] [has_le β] : has_le (α × β) :=
 ⟨λp q, p.1 ≤ q.1 ∧ p.2 ≤ q.2⟩
diff --git a/src/order/conditionally_complete_lattice.lean b/src/order/conditionally_complete_lattice.lean
index d9f1d2651e679..54e748440d9f3 100644
--- a/src/order/conditionally_complete_lattice.lean
+++ b/src/order/conditionally_complete_lattice.lean
@@ -848,22 +848,22 @@ noncomputable def subset_conditionally_complete_linear_order [inhabited s]
     rintros t c h_bdd hct,
     -- The following would be a more natural way to finish, but gives a "deep recursion" error:
     -- simpa [subset_Sup_of_within (h_Sup t)] using (strict_mono_coe s).monotone.le_cSup_image hct h_bdd,
-    have := (strict_mono_coe s).monotone.le_cSup_image hct h_bdd,
+    have := (subtype.mono_coe s).le_cSup_image hct h_bdd,
     rwa subset_Sup_of_within s (h_Sup ⟨c, hct⟩ h_bdd) at this,
   end,
   cSup_le := begin
     rintros t B ht hB,
-    have := (strict_mono_coe s).monotone.cSup_image_le ht hB,
+    have := (subtype.mono_coe s).cSup_image_le ht hB,
     rwa subset_Sup_of_within s (h_Sup ht ⟨B, hB⟩) at this,
   end,
   le_cInf := begin
     intros t B ht hB,
-    have := (strict_mono_coe s).monotone.le_cInf_image ht hB,
+    have := (subtype.mono_coe s).le_cInf_image ht hB,
     rwa subset_Inf_of_within s (h_Inf ht ⟨B, hB⟩) at this,
   end,
   cInf_le := begin
     rintros t c h_bdd hct,
-    have := (strict_mono_coe s).monotone.cInf_image_le hct h_bdd,
+    have := (subtype.mono_coe s).cInf_image_le hct h_bdd,
     rwa subset_Inf_of_within s (h_Inf ⟨c, hct⟩ h_bdd) at this,
   end,
   ..subset_has_Sup s,
@@ -882,8 +882,8 @@ begin
   obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht,
   obtain ⟨B, hB⟩ : ∃ B, B ∈ upper_bounds t := h_bdd,
   refine hs c.2 B.2 ⟨_, _⟩,
-  { exact (strict_mono_coe s).monotone.le_cSup_image hct ⟨B, hB⟩ },
-  { exact (strict_mono_coe s).monotone.cSup_image_le ⟨c, hct⟩ hB },
+  { exact (subtype.mono_coe s).le_cSup_image hct ⟨B, hB⟩ },
+  { exact (subtype.mono_coe s).cSup_image_le ⟨c, hct⟩ hB },
 end
 
 /-- The `Inf` function on a nonempty `ord_connected` set `s` in a conditionally complete linear
@@ -895,8 +895,8 @@ begin
   obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht,
   obtain ⟨B, hB⟩ : ∃ B, B ∈ lower_bounds t := h_bdd,
   refine hs B.2 c.2 ⟨_, _⟩,
-  { exact (strict_mono_coe s).monotone.le_cInf_image ⟨c, hct⟩ hB },
-  { exact (strict_mono_coe s).monotone.cInf_image_le hct ⟨B, hB⟩ },
+  { exact (subtype.mono_coe s).le_cInf_image ⟨c, hct⟩ hB },
+  { exact (subtype.mono_coe s).cInf_image_le hct ⟨B, hB⟩ },
 end
 
 /-- A nonempty `ord_connected` set in a conditionally complete linear order is naturally a