refactor(order/rel_iso): move statements about intervals to data/set/intervals (#8150)

This means that we can talk about `rel_iso` without needing to transitively import `ordered_group`s

This PR takes advantage of this to define `order_iso.mul_(left|right)[']` to mirror `equiv.mul_(left|right)[']`.

Author: eric-wieser

src/algebra/ordered_field.lean

@@ -32,6 +32,20 @@ variable {α : Type*}
 section linear_ordered_field
 variables [linear_ordered_field α] {a b c d e : α}
 
+section
+
+/-- `equiv.mul_left'` as an order_iso. -/
+@[simps {simp_rhs := tt}]
+def order_iso.mul_left' (a : α) (ha : 0 < a) : α ≃o α :=
+{ map_rel_iff' := λ _ _, mul_le_mul_left ha, ..equiv.mul_left' a ha.ne' }
+
+/-- `equiv.mul_right'` as an order_iso. -/
+@[simps {simp_rhs := tt}]
+def order_iso.mul_right' (a : α) (ha : 0 < a) : α ≃o α :=
+{ map_rel_iff' := λ _ _, mul_le_mul_right ha, ..equiv.mul_right' a ha.ne' }
+
+end
+
 /-!
 ### Lemmas about pos, nonneg, nonpos, neg
 -/

src/algebra/ordered_group.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import algebra.ordered_monoid
+import order.rel_iso
 
 /-!
 # Ordered groups
@@ -564,10 +565,22 @@ alias le_sub_iff_add_le ↔ add_le_of_le_sub_right le_sub_right_of_add_le
 lemma div_le_iff_le_mul : a / c ≤ b ↔ a ≤ b * c :=
 by rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
 
+/-- `equiv.mul_right` as an order_iso. -/
+@[simps {simp_rhs := tt}]
+def order_iso.mul_right (a : α) : α ≃o α :=
+{ map_rel_iff' := λ _ _, mul_le_mul_iff_right a, ..equiv.mul_right a }
+
 end right
 
 section left
-variables [covariant_class α α (*) (≤)] [covariant_class α α (function.swap (*)) (≤)] {a b c : α}
+variables [covariant_class α α (*) (≤)]
+
+/-- `equiv.mul_left` as an order_iso. -/
+@[simps {simp_rhs := tt}]
+def order_iso.mul_left (a : α) : α ≃o α :=
+{ map_rel_iff' := λ _ _, mul_le_mul_iff_left a, ..equiv.mul_left a }
+
+variables [covariant_class α α (function.swap (*)) (≤)] {a b c : α}
 
 @[simp, to_additive]
 lemma div_le_div_iff_left (a : α) : a / b ≤ a / c ↔ c ≤ b :=

src/data/set/intervals/basic.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy
 -/
 import algebra.ordered_group
 import data.set.basic
+import order.rel_iso
 
 /-!
 # Intervals
@@ -1274,3 +1275,49 @@ end
 end linear_ordered_add_comm_group
 
 end set
+
+namespace order_iso
+variables {α β : Type*}
+
+open set
+
+section preorder
+variables [preorder α] [preorder β]
+
+@[simp] lemma preimage_Iic (e : α ≃o β) (b : β) : e ⁻¹' (Iic b) = Iic (e.symm b) :=
+by { ext x, simp [← e.le_iff_le] }
+
+@[simp] lemma preimage_Ici (e : α ≃o β) (b : β) : e ⁻¹' (Ici b) = Ici (e.symm b) :=
+by { ext x, simp [← e.le_iff_le] }
+
+@[simp] lemma preimage_Iio (e : α ≃o β) (b : β) : e ⁻¹' (Iio b) = Iio (e.symm b) :=
+by { ext x, simp [← e.lt_iff_lt] }
+
+@[simp] lemma preimage_Ioi (e : α ≃o β) (b : β) : e ⁻¹' (Ioi b) = Ioi (e.symm b) :=
+by { ext x, simp [← e.lt_iff_lt] }
+
+@[simp] lemma preimage_Icc (e : α ≃o β) (a b : β) : e ⁻¹' (Icc a b) = Icc (e.symm a) (e.symm b) :=
+by simp [← Ici_inter_Iic]
+
+@[simp] lemma preimage_Ico (e : α ≃o β) (a b : β) : e ⁻¹' (Ico a b) = Ico (e.symm a) (e.symm b) :=
+by simp [← Ici_inter_Iio]
+
+@[simp] lemma preimage_Ioc (e : α ≃o β) (a b : β) : e ⁻¹' (Ioc a b) = Ioc (e.symm a) (e.symm b) :=
+by simp [← Ioi_inter_Iic]
+
+@[simp] lemma preimage_Ioo (e : α ≃o β) (a b : β) : e ⁻¹' (Ioo a b) = Ioo (e.symm a) (e.symm b) :=
+by simp [← Ioi_inter_Iio]
+
+end preorder
+
+/-- Order isomorphism between `Iic (⊤ : α)` and `α` when `α` has a top element -/
+def Iic_top [order_top α] : set.Iic (⊤ : α) ≃o α :=
+{ map_rel_iff' := λ x y, by refl,
+  .. (@equiv.subtype_univ_equiv α (set.Iic (⊤ : α)) (λ x, le_top)), }
+
+/-- Order isomorphism between `Ici (⊥ : α)` and `α` when `α` has a bottom element -/
+def Ici_bot [order_bot α] : set.Ici (⊥ : α) ≃o α :=
+{ map_rel_iff' := λ x y, by refl,
+  .. (@equiv.subtype_univ_equiv α (set.Ici (⊥ : α)) (λ x, bot_le)) }
+
+end order_iso

src/order/rel_iso.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 import logic.embedding
 import order.rel_classes
-import data.set.intervals.basic
+import algebra.group.defs
 
 open function
 
@@ -602,30 +602,6 @@ protected lemma strict_mono (e : α ≃o β) : strict_mono e := e.to_order_embed
 @[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] }
-
-@[simp] lemma preimage_Ici (e : α ≃o β) (b : β) : e ⁻¹' (Ici b) = Ici (e.symm b) :=
-by { ext x, simp [← e.le_iff_le] }
-
-@[simp] lemma preimage_Iio (e : α ≃o β) (b : β) : e ⁻¹' (Iio b) = Iio (e.symm b) :=
-by { ext x, simp [← e.lt_iff_lt] }
-
-@[simp] lemma preimage_Ioi (e : α ≃o β) (b : β) : e ⁻¹' (Ioi b) = Ioi (e.symm b) :=
-by { ext x, simp [← e.lt_iff_lt] }
-
-@[simp] lemma preimage_Icc (e : α ≃o β) (a b : β) : e ⁻¹' (Icc a b) = Icc (e.symm a) (e.symm b) :=
-by simp [← Ici_inter_Iic]
-
-@[simp] lemma preimage_Ico (e : α ≃o β) (a b : β) : e ⁻¹' (Ico a b) = Ico (e.symm a) (e.symm b) :=
-by simp [← Ici_inter_Iio]
-
-@[simp] lemma preimage_Ioc (e : α ≃o β) (a b : β) : e ⁻¹' (Ioc a b) = Ioc (e.symm a) (e.symm b) :=
-by simp [← Ioi_inter_Iic]
-
-@[simp] lemma preimage_Ioo (e : α ≃o β) (a b : β) : e ⁻¹' (Ioo a b) = Ioo (e.symm a) (e.symm b) :=
-by simp [← Ioi_inter_Iio]
-
 /-- To show that `f : α → β`, `g : β → α` make up an order isomorphism of linear orders,
     it suffices to prove `cmp a (g b) = cmp (f a) b`. --/
 def of_cmp_eq_cmp {α β} [linear_order α] [linear_order β] (f : α → β) (g : β → α)
@@ -741,16 +717,6 @@ lemma order_iso.map_sup [semilattice_sup α] [semilattice_sup β]
   f (x ⊔ y) = f x ⊔ f y :=
 f.dual.map_inf x y
 
-/-- Order isomorphism between `Iic (⊤ : α)` and `α` when `α` has a top element -/
-def order_iso.Iic_top [order_top α] : set.Iic (⊤ : α) ≃o α :=
-{ map_rel_iff' := λ x y, by refl,
-  .. (@equiv.subtype_univ_equiv α (set.Iic (⊤ : α)) (λ x, le_top)), }
-
-/-- Order isomorphism between `Ici (⊥ : α)` and `α` when `α` has a bottom element -/
-def order_iso.Ici_bot [order_bot α] : set.Ici (⊥ : α) ≃o α :=
-{ map_rel_iff' := λ x y, by refl,
-  .. (@equiv.subtype_univ_equiv α (set.Ici (⊥ : α)) (λ x, bot_le)) }
-
 section bounded_lattice
 
 variables [bounded_lattice α]  [bounded_lattice β] (f : α ≃o β)