From 529d1ee79e5533f5bd13e39942c678004deb3609 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 22 Jan 2024 21:13:57 -0600
Subject: [PATCH 1/3] feat: add lemmas about preimages of intervals under order
 embeddings

Also use them for `Rat.cast`.
---
 Mathlib.lean                                  |  1 +
 Mathlib/Data/Rat/Cast/Order.lean              | 49 +++++++++---------
 .../Data/Set/Intervals/OrderEmbedding.lean    | 51 +++++++++++++++++++
 3 files changed, 77 insertions(+), 24 deletions(-)
 create mode 100644 Mathlib/Data/Set/Intervals/OrderEmbedding.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 9820164c78cf0..687def434f4d4 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1980,6 +1980,7 @@ import Mathlib.Data.Set.Intervals.Monoid
 import Mathlib.Data.Set.Intervals.Monotone
 import Mathlib.Data.Set.Intervals.OrdConnected
 import Mathlib.Data.Set.Intervals.OrdConnectedComponent
+import Mathlib.Data.Set.Intervals.OrderEmbedding
 import Mathlib.Data.Set.Intervals.OrderIso
 import Mathlib.Data.Set.Intervals.Pi
 import Mathlib.Data.Set.Intervals.ProjIcc
diff --git a/Mathlib/Data/Rat/Cast/Order.lean b/Mathlib/Data/Rat/Cast/Order.lean
index 6d6d58e8cac10..dca14071e4ef7 100644
--- a/Mathlib/Data/Rat/Cast/Order.lean
+++ b/Mathlib/Data/Rat/Cast/Order.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Data.Rat.Cast.CharZero
 import Mathlib.Data.Rat.Order
+import Mathlib.Data.Set.Intervals.OrderEmbedding
 import Mathlib.Algebra.Order.Field.Basic
 
 #align_import data.rat.cast from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
@@ -98,51 +99,51 @@ theorem cast_abs {q : ℚ} : ((|q| : ℚ) : K) = |(q : K)| := by simp [abs_eq_ma
 open Set
 
 @[simp]
-theorem preimage_cast_Icc (a b : ℚ) : (↑) ⁻¹' Icc (a : K) b = Icc a b := by
-  ext x
-  simp
+theorem preimage_cast_Icc (a b : ℚ) : (↑) ⁻¹' Icc (a : K) b = Icc a b :=
+  castOrderEmbedding.preimage_Icc ..
 #align rat.preimage_cast_Icc Rat.preimage_cast_Icc
 
 @[simp]
-theorem preimage_cast_Ico (a b : ℚ) : (↑) ⁻¹' Ico (a : K) b = Ico a b := by
-  ext x
-  simp
+theorem preimage_cast_Ico (a b : ℚ) : (↑) ⁻¹' Ico (a : K) b = Ico a b :=
+  castOrderEmbedding.preimage_Ico ..
 #align rat.preimage_cast_Ico Rat.preimage_cast_Ico
 
 @[simp]
-theorem preimage_cast_Ioc (a b : ℚ) : (↑) ⁻¹' Ioc (a : K) b = Ioc a b := by
-  ext x
-  simp
+theorem preimage_cast_Ioc (a b : ℚ) : (↑) ⁻¹' Ioc (a : K) b = Ioc a b :=
+  castOrderEmbedding.preimage_Ioc a b
 #align rat.preimage_cast_Ioc Rat.preimage_cast_Ioc
 
 @[simp]
-theorem preimage_cast_Ioo (a b : ℚ) : (↑) ⁻¹' Ioo (a : K) b = Ioo a b := by
-  ext x
-  simp
+theorem preimage_cast_Ioo (a b : ℚ) : (↑) ⁻¹' Ioo (a : K) b = Ioo a b :=
+  castOrderEmbedding.preimage_Ioo a b
 #align rat.preimage_cast_Ioo Rat.preimage_cast_Ioo
 
 @[simp]
-theorem preimage_cast_Ici (a : ℚ) : (↑) ⁻¹' Ici (a : K) = Ici a := by
-  ext x
-  simp
+theorem preimage_cast_Ici (a : ℚ) : (↑) ⁻¹' Ici (a : K) = Ici a :=
+  castOrderEmbedding.preimage_Ici a
 #align rat.preimage_cast_Ici Rat.preimage_cast_Ici
 
 @[simp]
-theorem preimage_cast_Iic (a : ℚ) : (↑) ⁻¹' Iic (a : K) = Iic a := by
-  ext x
-  simp
+theorem preimage_cast_Iic (a : ℚ) : (↑) ⁻¹' Iic (a : K) = Iic a :=
+  castOrderEmbedding.preimage_Iic a
 #align rat.preimage_cast_Iic Rat.preimage_cast_Iic
 
 @[simp]
-theorem preimage_cast_Ioi (a : ℚ) : (↑) ⁻¹' Ioi (a : K) = Ioi a := by
-  ext x
-  simp
+theorem preimage_cast_Ioi (a : ℚ) : (↑) ⁻¹' Ioi (a : K) = Ioi a :=
+  castOrderEmbedding.preimage_Ioi a
 #align rat.preimage_cast_Ioi Rat.preimage_cast_Ioi
 
 @[simp]
-theorem preimage_cast_Iio (a : ℚ) : (↑) ⁻¹' Iio (a : K) = Iio a := by
-  ext x
-  simp
+theorem preimage_cast_Iio (a : ℚ) : (↑) ⁻¹' Iio (a : K) = Iio a :=
+  castOrderEmbedding.preimage_Iio a
 #align rat.preimage_cast_Iio Rat.preimage_cast_Iio
 
+@[simp]
+theorem preimage_cast_uIcc (a b : ℚ) : (↑) ⁻¹' uIcc (a : K) b = uIcc a b :=
+  (castOrderEmbedding (K := K)).preimage_uIcc a b
+
+@[simp]
+theorem preimage_cast_uIoc (a b : ℚ) : (↑) ⁻¹' uIoc (a : K) b = uIoc a b :=
+  (castOrderEmbedding (K := K)).preimage_uIoc a b
+
 end LinearOrderedField
diff --git a/Mathlib/Data/Set/Intervals/OrderEmbedding.lean b/Mathlib/Data/Set/Intervals/OrderEmbedding.lean
new file mode 100644
index 0000000000000..5ac9c3380ab6b
--- /dev/null
+++ b/Mathlib/Data/Set/Intervals/OrderEmbedding.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2024 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Data.Set.Intervals.Basic
+import Mathlib.Data.Set.Intervals.UnorderedInterval
+import Mathlib.Order.Hom.Basic
+
+/-!
+# Preimages of intervals under order embeddings
+
+In this file we prove that the preimage of an interval in the codomain under an `OrderEmbedding`
+is an interval in the domain.
+
+Note that similar statements about images require the range to be order-connected.
+-/
+
+open Set
+
+namespace OrderEmbedding
+
+variable {α β : Type*}
+
+section Preorder
+
+variable [Preorder α] [Preorder β] (e : α ↪o β) (x y : α)
+
+@[simp] theorem preimage_Ici : e ⁻¹' Ici (e x) = Ici x := ext fun _ ↦ e.le_iff_le
+@[simp] theorem preimage_Iic : e ⁻¹' Iic (e x) = Iic x := ext fun _ ↦ e.le_iff_le
+@[simp] theorem preimage_Ioi : e ⁻¹' Ioi (e x) = Ioi x := ext fun _ ↦ e.lt_iff_lt
+@[simp] theorem preimage_Iio : e ⁻¹' Iio (e x) = Iio x := ext fun _ ↦ e.lt_iff_lt
+
+@[simp] theorem preimage_Icc : e ⁻¹' Icc (e x) (e y) = Icc x y := by ext; simp
+@[simp] theorem preimage_Ico : e ⁻¹' Ico (e x) (e y) = Ico x y := by ext; simp
+@[simp] theorem preimage_Ioc : e ⁻¹' Ioc (e x) (e y) = Ioc x y := by ext; simp
+@[simp] theorem preimage_Ioo : e ⁻¹' Ioo (e x) (e y) = Ioo x y := by ext; simp
+
+end Preorder
+
+variable [LinearOrder α]
+
+@[simp] theorem preimage_uIcc [Lattice β] (e : α ↪o β) (x y : α) :
+    e ⁻¹' (uIcc (e x) (e y)) = uIcc x y := by
+  cases le_total x y <;> simp [*]
+
+@[simp] theorem preimage_uIoc [LinearOrder β] (e : α ↪o β) (x y : α) :
+    e ⁻¹' (uIoc (e x) (e y)) = uIoc x y := by
+  cases le_or_lt x y <;> simp [*]
+
+end OrderEmbedding

From d3acbb08d58c17a04c703160f16a8b1550e7fd58 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 22 Jan 2024 21:28:00 -0600
Subject: [PATCH 2/3] Add lemmas about images of intervals under
 `OrderEmbedding`s

---
 Mathlib/Data/Set/Intervals/OrdConnected.lean  | 52 +++++++++++++++----
 .../Data/Set/Intervals/OrderEmbedding.lean    |  1 -
 2 files changed, 42 insertions(+), 11 deletions(-)

diff --git a/Mathlib/Data/Set/Intervals/OrdConnected.lean b/Mathlib/Data/Set/Intervals/OrdConnected.lean
index aa9a7196c9cd4..afa19047837a2 100644
--- a/Mathlib/Data/Set/Intervals/OrdConnected.lean
+++ b/Mathlib/Data/Set/Intervals/OrdConnected.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
-import Mathlib.Data.Set.Intervals.UnorderedInterval
+import Mathlib.Data.Set.Intervals.OrderEmbedding
 import Mathlib.Data.Set.Lattice
 import Mathlib.Order.Antichain
 
@@ -21,8 +21,8 @@ In this file we prove that intersection of a family of `OrdConnected` sets is `O
 that all standard intervals are `OrdConnected`.
 -/
 
-open Interval
-
+open scoped Interval
+open Set
 open OrderDual (toDual ofDual)
 
 namespace Set
@@ -78,28 +78,60 @@ protected theorem Icc_subset (s : Set α) [hs : OrdConnected s] {x y} (hx : x 
   hs.out hx hy
 #align set.Icc_subset Set.Icc_subset
 
+end Preorder
+
+end Set
+
+namespace OrderEmbedding
+
+variable {α β : Type*} [Preorder α] [Preorder β]
+
+theorem image_Icc (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
+    e '' Icc x y = Icc (e x) (e y) := by
+  rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]
+
+theorem image_Ico (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
+    e '' Ico x y = Ico (e x) (e y) := by
+  rw [← e.preimage_Ico, image_preimage_eq_inter_range,
+    inter_eq_left.2 <| Ico_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
+
+theorem image_Ioc (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
+    e '' Ioc x y = Ioc (e x) (e y) := by
+  rw [← e.preimage_Ioc, image_preimage_eq_inter_range,
+    inter_eq_left.2 <| Ioc_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
+
+theorem image_Ioo (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
+    e '' Ioo x y = Ioo (e x) (e y) := by
+  rw [← e.preimage_Ioo, image_preimage_eq_inter_range,
+    inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
+
+end OrderEmbedding
+
+namespace Set
+
+section Preorder
+
+variable {α β : Type*} [Preorder α] [Preorder β] {s t : Set α}
+
 @[simp]
 lemma image_subtype_val_Icc {s : Set α} [OrdConnected s] (x y : s) :
     Subtype.val '' Icc x y = Icc x.1 y :=
-  (Subtype.image_preimage_val s (Icc x.1 y)).trans <| inter_eq_left.2 <| s.Icc_subset x.2 y.2
+  (OrderEmbedding.subtype (· ∈ s)).image_Icc (by simpa) x y
 
 @[simp]
 lemma image_subtype_val_Ico {s : Set α} [OrdConnected s] (x y : s) :
     Subtype.val '' Ico x y = Ico x.1 y :=
-  (Subtype.image_preimage_val s (Ico x.1 y)).trans <| inter_eq_left.2 <|
-    Ico_subset_Icc_self.trans <| s.Icc_subset x.2 y.2
+  (OrderEmbedding.subtype (· ∈ s)).image_Ico (by simpa) x y
 
 @[simp]
 lemma image_subtype_val_Ioc {s : Set α} [OrdConnected s] (x y : s) :
     Subtype.val '' Ioc x y = Ioc x.1 y :=
-  (Subtype.image_preimage_val s (Ioc x.1 y)).trans <| inter_eq_left.2 <|
-    Ioc_subset_Icc_self.trans <| s.Icc_subset x.2 y.2
+  (OrderEmbedding.subtype (· ∈ s)).image_Ioc (by simpa) x y
 
 @[simp]
 lemma image_subtype_val_Ioo {s : Set α} [OrdConnected s] (x y : s) :
     Subtype.val '' Ioo x y = Ioo x.1 y :=
-  (Subtype.image_preimage_val s (Ioo x.1 y)).trans <| inter_eq_left.2 <|
-    Ioo_subset_Icc_self.trans <| s.Icc_subset x.2 y.2
+  (OrderEmbedding.subtype (· ∈ s)).image_Ioo (by simpa) x y
 
 theorem OrdConnected.inter {s t : Set α} (hs : OrdConnected s) (ht : OrdConnected t) :
     OrdConnected (s ∩ t) :=
diff --git a/Mathlib/Data/Set/Intervals/OrderEmbedding.lean b/Mathlib/Data/Set/Intervals/OrderEmbedding.lean
index 5ac9c3380ab6b..11df3b15c67dd 100644
--- a/Mathlib/Data/Set/Intervals/OrderEmbedding.lean
+++ b/Mathlib/Data/Set/Intervals/OrderEmbedding.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Set.Intervals.UnorderedInterval
 import Mathlib.Order.Hom.Basic
 

From ca2ec616c11756697f8eb61098bce5d55bed6f87 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 22 Jan 2024 21:28:35 -0600
Subject: [PATCH 3/3] Fixup

---
 Mathlib/Data/Set/Intervals/OrderEmbedding.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Set/Intervals/OrderEmbedding.lean b/Mathlib/Data/Set/Intervals/OrderEmbedding.lean
index 5ac9c3380ab6b..11df3b15c67dd 100644
--- a/Mathlib/Data/Set/Intervals/OrderEmbedding.lean
+++ b/Mathlib/Data/Set/Intervals/OrderEmbedding.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Set.Intervals.UnorderedInterval
 import Mathlib.Order.Hom.Basic