diff --git a/src/algebra/big_operators/order.lean b/src/algebra/big_operators/order.lean
index f52200dda4fd0..32c2a01fe1fac 100644
--- a/src/algebra/big_operators/order.lean
+++ b/src/algebra/big_operators/order.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 
 import algebra.order.absolute_value
+import algebra.order.ring.with_top
 import algebra.big_operators.basic
 
 /-!
diff --git a/src/algebra/euclidean_domain.lean b/src/algebra/euclidean_domain.lean
index f749980d318ee..66d1029e516fe 100644
--- a/src/algebra/euclidean_domain.lean
+++ b/src/algebra/euclidean_domain.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Louis Carlin, Mario Carneiro
 -/
 import algebra.field.basic
+import algebra.ring.basic
 
 /-!
 # Euclidean domains
diff --git a/src/algebra/gcd_monoid/basic.lean b/src/algebra/gcd_monoid/basic.lean
index 838aa8c26747d..dd86e1f6505ed 100644
--- a/src/algebra/gcd_monoid/basic.lean
+++ b/src/algebra/gcd_monoid/basic.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Jens Wagemaker
 
 import algebra.associated
 import algebra.group_power.lemmas
+import algebra.ring.regular
 
 /-!
 # Monoids with normalization functions, `gcd`, and `lcm`
diff --git a/src/algebra/group/pi.lean b/src/algebra/group/pi.lean
index 928b96d6bbdb1..660b2e9330ede 100644
--- a/src/algebra/group/pi.lean
+++ b/src/algebra/group/pi.lean
@@ -3,10 +3,10 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
+import logic.pairwise
 import algebra.hom.group_instances
 import data.pi.algebra
 import data.set.function
-import data.set.pairwise
 import tactic.pi_instances
 
 /-!
diff --git a/src/algebra/group_power/order.lean b/src/algebra/group_power/order.lean
index 6f956fa2609f1..7e73bf03d23d3 100644
--- a/src/algebra/group_power/order.lean
+++ b/src/algebra/group_power/order.lean
@@ -3,7 +3,7 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
-import algebra.order.ring
+import algebra.order.ring.abs
 import algebra.group_power.ring
 import data.set.intervals.basic
 
diff --git a/src/algebra/order/field/basic.lean b/src/algebra/order/field/basic.lean
index d506377e6ace4..49814708ba682 100644
--- a/src/algebra/order/field/basic.lean
+++ b/src/algebra/order/field/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
-import order.bounds
+import order.bounds.order_iso
 import algebra.order.field.defs
 
 /-!
diff --git a/src/algebra/order/field/defs.lean b/src/algebra/order/field/defs.lean
index 57d0fc760dc02..eb69c7617c671 100644
--- a/src/algebra/order/field/defs.lean
+++ b/src/algebra/order/field/defs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
 import algebra.field.basic
-import algebra.order.ring
+import algebra.order.ring.basic
 
 /-!
 # Linear ordered (semi)fields
diff --git a/src/algebra/order/floor.lean b/src/algebra/order/floor.lean
index 6fa9faf9f118d..540c85d284517 100644
--- a/src/algebra/order/floor.lean
+++ b/src/algebra/order/floor.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kevin Kappelmann
 -/
 import data.int.lemmas
+import data.set.intervals.group
 import tactic.abel
 import tactic.linarith
 import tactic.positivity
diff --git a/src/algebra/order/group/abs.lean b/src/algebra/order/group/abs.lean
new file mode 100644
index 0000000000000..05d4c10b3a9f5
--- /dev/null
+++ b/src/algebra/order/group/abs.lean
@@ -0,0 +1,281 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+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.abs
+import algebra.order.group.basic
+import algebra.order.monoid.canonical
+
+/-!
+# Absolute values in ordered groups.
+-/
+
+variables {α : Type*}
+open function
+
+section covariant_add_le
+
+section has_neg
+
+/-- `abs a` is the absolute value of `a`. -/
+@[to_additive "`abs a` is the absolute value of `a`",
+  priority 100] -- see Note [lower instance priority]
+instance has_inv.to_has_abs [has_inv α] [has_sup α] : has_abs α := ⟨λ a, a ⊔ a⁻¹⟩
+
+@[to_additive] lemma abs_eq_sup_inv [has_inv α] [has_sup α] (a : α) : |a| = a ⊔ a⁻¹ := rfl
+
+variables [has_neg α] [linear_order α] {a b: α}
+
+lemma abs_eq_max_neg : abs a = max a (-a) :=
+rfl
+
+lemma abs_choice (x : α) : |x| = x ∨ |x| = -x := max_choice _ _
+
+lemma abs_le' : |a| ≤ b ↔ a ≤ b ∧ -a ≤ b := max_le_iff
+
+lemma le_abs : a ≤ |b| ↔ a ≤ b ∨ a ≤ -b := le_max_iff
+
+lemma le_abs_self (a : α) : a ≤ |a| := le_max_left _ _
+
+lemma neg_le_abs_self (a : α) : -a ≤ |a| := le_max_right _ _
+
+lemma lt_abs : a < |b| ↔ a < b ∨ a < -b := lt_max_iff
+
+theorem abs_le_abs (h₀ : a ≤ b) (h₁ : -a ≤ b) : |a| ≤ |b| :=
+(abs_le'.2 ⟨h₀, h₁⟩).trans (le_abs_self b)
+
+lemma abs_by_cases (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) : P (|a|) :=
+sup_ind _ _ h1 h2
+
+end has_neg
+
+section add_group
+variables [add_group α] [linear_order α]
+
+@[simp] lemma abs_neg (a : α) : | -a| = |a| :=
+begin
+  rw [abs_eq_max_neg, max_comm, neg_neg, abs_eq_max_neg]
+end
+
+lemma eq_or_eq_neg_of_abs_eq {a b : α} (h : |a| = b) : a = b ∨ a = -b :=
+by simpa only [← h, eq_comm, eq_neg_iff_eq_neg] using abs_choice a
+
+lemma abs_eq_abs {a b : α} : |a| = |b| ↔ a = b ∨ a = -b :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { obtain rfl | rfl := eq_or_eq_neg_of_abs_eq h;
+    simpa only [neg_eq_iff_neg_eq, neg_inj, or.comm, @eq_comm _ (-b)] using abs_choice b },
+  { cases h; simp only [h, abs_neg] },
+end
+
+lemma abs_sub_comm (a b : α) : |a - b| = |b - a| :=
+calc  |a - b| = | - (b - a)| : congr_arg _ (neg_sub b a).symm
+          ... = |b - a|      : abs_neg (b - a)
+
+variables [covariant_class α α (+) (≤)] {a b c : α}
+
+lemma abs_of_nonneg (h : 0 ≤ a) : |a| = a :=
+max_eq_left $ (neg_nonpos.2 h).trans h
+
+lemma abs_of_pos (h : 0 < a) : |a| = a :=
+abs_of_nonneg h.le
+
+lemma abs_of_nonpos (h : a ≤ 0) : |a| = -a :=
+max_eq_right $ h.trans (neg_nonneg.2 h)
+
+lemma abs_of_neg (h : a < 0) : |a| = -a :=
+abs_of_nonpos h.le
+
+lemma abs_le_abs_of_nonneg (ha : 0 ≤ a) (hab : a ≤ b) : |a| ≤ |b| :=
+by rwa [abs_of_nonneg ha, abs_of_nonneg (ha.trans hab)]
+
+@[simp] lemma abs_zero : |0| = (0:α) :=
+abs_of_nonneg le_rfl
+
+@[simp] lemma abs_pos : 0 < |a| ↔ a ≠ 0 :=
+begin
+  rcases lt_trichotomy a 0 with (ha|rfl|ha),
+  { simp [abs_of_neg ha, neg_pos, ha.ne, ha] },
+  { simp },
+  { simp [abs_of_pos ha, ha, ha.ne.symm] }
+end
+
+lemma abs_pos_of_pos (h : 0 < a) : 0 < |a| := abs_pos.2 h.ne.symm
+
+lemma abs_pos_of_neg (h : a < 0) : 0 < |a| := abs_pos.2 h.ne
+
+lemma neg_abs_le_self (a : α) : -|a| ≤ a :=
+begin
+  cases le_total 0 a with h h,
+  { calc -|a| = - a   : congr_arg (has_neg.neg) (abs_of_nonneg h)
+            ... ≤ 0     : neg_nonpos.mpr h
+            ... ≤ a     : h },
+  { calc -|a| = - - a : congr_arg (has_neg.neg) (abs_of_nonpos h)
+            ... ≤ a     : (neg_neg a).le }
+end
+
+lemma add_abs_nonneg (a : α) : 0 ≤ a + |a| :=
+begin
+  rw ←add_right_neg a,
+  apply add_le_add_left,
+  exact (neg_le_abs_self a),
+end
+
+lemma neg_abs_le_neg (a : α) : -|a| ≤ -a :=
+by simpa using neg_abs_le_self (-a)
+
+@[simp] lemma abs_nonneg (a : α) : 0 ≤ |a| :=
+(le_total 0 a).elim (λ h, h.trans (le_abs_self a)) (λ h, (neg_nonneg.2 h).trans $ neg_le_abs_self a)
+
+@[simp] lemma abs_abs (a : α) : | |a| | = |a| :=
+abs_of_nonneg $ abs_nonneg a
+
+@[simp] lemma abs_eq_zero : |a| = 0 ↔ a = 0 :=
+decidable.not_iff_not.1 $ ne_comm.trans $ (abs_nonneg a).lt_iff_ne.symm.trans abs_pos
+
+@[simp] lemma abs_nonpos_iff {a : α} : |a| ≤ 0 ↔ a = 0 :=
+(abs_nonneg a).le_iff_eq.trans abs_eq_zero
+
+variable [covariant_class α α (swap (+)) (≤)]
+
+lemma abs_le_abs_of_nonpos (ha : a ≤ 0) (hab : b ≤ a) : |a| ≤ |b| :=
+by { rw [abs_of_nonpos ha, abs_of_nonpos (hab.trans ha)], exact neg_le_neg_iff.mpr hab }
+
+lemma abs_lt : |a| < b ↔ - b < a ∧ a < b :=
+max_lt_iff.trans $ and.comm.trans $ by rw [neg_lt]
+
+lemma neg_lt_of_abs_lt (h : |a| < b) : -b < a := (abs_lt.mp h).1
+
+lemma lt_of_abs_lt (h : |a| < b) : a < b := (abs_lt.mp h).2
+
+lemma max_sub_min_eq_abs' (a b : α) : max a b - min a b = |a - b| :=
+begin
+  cases le_total a b with ab ba,
+  { rw [max_eq_right ab, min_eq_left ab, abs_of_nonpos, neg_sub], rwa sub_nonpos },
+  { rw [max_eq_left ba, min_eq_right ba, abs_of_nonneg], rwa sub_nonneg }
+end
+
+lemma max_sub_min_eq_abs (a b : α) : max a b - min a b = |b - a| :=
+by { rw abs_sub_comm, exact max_sub_min_eq_abs' _ _ }
+
+end add_group
+
+end covariant_add_le
+
+section linear_ordered_add_comm_group
+
+variables [linear_ordered_add_comm_group α] {a b c d : α}
+
+lemma abs_le : |a| ≤ b ↔ - b ≤ a ∧ a ≤ b := by rw [abs_le', and.comm, neg_le]
+
+lemma le_abs' : a ≤ |b| ↔ b ≤ -a ∨ a ≤ b := by rw [le_abs, or.comm, le_neg]
+
+lemma neg_le_of_abs_le (h : |a| ≤ b) : -b ≤ a := (abs_le.mp h).1
+
+lemma le_of_abs_le (h : |a| ≤ b) : a ≤ b := (abs_le.mp h).2
+
+@[to_additive] lemma apply_abs_le_mul_of_one_le' {β : Type*} [mul_one_class β] [preorder β]
+  [covariant_class β β (*) (≤)] [covariant_class β β (swap (*)) (≤)] {f : α → β} {a : α}
+  (h₁ : 1 ≤ f a) (h₂ : 1 ≤ f (-a)) :
+  f (|a|) ≤ f a * f (-a) :=
+(le_total a 0).by_cases (λ ha, (abs_of_nonpos ha).symm ▸ le_mul_of_one_le_left' h₁)
+  (λ ha, (abs_of_nonneg ha).symm ▸ le_mul_of_one_le_right' h₂)
+
+@[to_additive] lemma apply_abs_le_mul_of_one_le {β : Type*} [mul_one_class β] [preorder β]
+  [covariant_class β β (*) (≤)] [covariant_class β β (swap (*)) (≤)] {f : α → β}
+  (h : ∀ x, 1 ≤ f x) (a : α) :
+  f (|a|) ≤ f a * f (-a) :=
+apply_abs_le_mul_of_one_le' (h _) (h _)
+
+/--
+The **triangle inequality** in `linear_ordered_add_comm_group`s.
+-/
+lemma abs_add (a b : α) : |a + b| ≤ |a| + |b| :=
+abs_le.2 ⟨(neg_add (|a|) (|b|)).symm ▸
+  add_le_add (neg_le.2 $ neg_le_abs_self _) (neg_le.2 $ neg_le_abs_self _),
+  add_le_add (le_abs_self _) (le_abs_self _)⟩
+
+lemma abs_add' (a b : α) : |a| ≤ |b| + |b + a| :=
+by simpa using abs_add (-b) (b + a)
+
+theorem abs_sub (a b : α) :
+  |a - b| ≤ |a| + |b| :=
+by { rw [sub_eq_add_neg, ←abs_neg b], exact abs_add a _ }
+
+lemma abs_sub_le_iff : |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c :=
+by rw [abs_le, neg_le_sub_iff_le_add, sub_le_iff_le_add', and_comm, sub_le_iff_le_add']
+
+lemma abs_sub_lt_iff : |a - b| < c ↔ a - b < c ∧ b - a < c :=
+by rw [abs_lt, neg_lt_sub_iff_lt_add', sub_lt_iff_lt_add', and_comm, sub_lt_iff_lt_add']
+
+lemma sub_le_of_abs_sub_le_left (h : |a - b| ≤ c) : b - c ≤ a :=
+sub_le_comm.1 $ (abs_sub_le_iff.1 h).2
+
+lemma sub_le_of_abs_sub_le_right (h : |a - b| ≤ c) : a - c ≤ b :=
+sub_le_of_abs_sub_le_left (abs_sub_comm a b ▸ h)
+
+lemma sub_lt_of_abs_sub_lt_left (h : |a - b| < c) : b - c < a :=
+sub_lt_comm.1 $ (abs_sub_lt_iff.1 h).2
+
+lemma sub_lt_of_abs_sub_lt_right (h : |a - b| < c) : a - c < b :=
+sub_lt_of_abs_sub_lt_left (abs_sub_comm a b ▸ h)
+
+lemma abs_sub_abs_le_abs_sub (a b : α) : |a| - |b| ≤ |a - b| :=
+sub_le_iff_le_add.2 $
+calc |a| = |a - b + b|     : by rw [sub_add_cancel]
+       ... ≤ |a - b| + |b| : abs_add _ _
+
+lemma abs_abs_sub_abs_le_abs_sub (a b : α) : | |a| - |b| | ≤ |a - b| :=
+abs_sub_le_iff.2 ⟨abs_sub_abs_le_abs_sub _ _, by rw abs_sub_comm; apply abs_sub_abs_le_abs_sub⟩
+
+lemma abs_eq (hb : 0 ≤ b) : |a| = b ↔ a = b ∨ a = -b :=
+begin
+  refine ⟨eq_or_eq_neg_of_abs_eq, _⟩,
+  rintro (rfl|rfl); simp only [abs_neg, abs_of_nonneg hb]
+end
+
+lemma abs_le_max_abs_abs (hab : a ≤ b) (hbc : b ≤ c) : |b| ≤ max (|a|) (|c|) :=
+abs_le'.2
+  ⟨by simp [hbc.trans (le_abs_self c)],
+   by simp [(neg_le_neg_iff.mpr hab).trans (neg_le_abs_self a)]⟩
+
+lemma min_abs_abs_le_abs_max : min (|a|) (|b|) ≤ |max a b| :=
+(le_total a b).elim
+  (λ h, (min_le_right _ _).trans_eq $ congr_arg _ (max_eq_right h).symm)
+  (λ h, (min_le_left _ _).trans_eq $ congr_arg _ (max_eq_left h).symm)
+
+lemma min_abs_abs_le_abs_min : min (|a|) (|b|) ≤ |min a b| :=
+(le_total a b).elim
+  (λ h, (min_le_left _ _).trans_eq $ congr_arg _ (min_eq_left h).symm)
+  (λ h, (min_le_right _ _).trans_eq $ congr_arg _ (min_eq_right h).symm)
+
+lemma abs_max_le_max_abs_abs : |max a b| ≤ max (|a|) (|b|) :=
+(le_total a b).elim
+  (λ h, (congr_arg _ $ max_eq_right h).trans_le $ le_max_right _ _)
+  (λ h, (congr_arg _ $ max_eq_left h).trans_le $ le_max_left _ _)
+
+lemma abs_min_le_max_abs_abs : |min a b| ≤ max (|a|) (|b|) :=
+(le_total a b).elim
+  (λ h, (congr_arg _ $ min_eq_left h).trans_le $ le_max_left _ _)
+  (λ h, (congr_arg _ $ min_eq_right h).trans_le $ le_max_right _ _)
+
+lemma eq_of_abs_sub_eq_zero {a b : α} (h : |a - b| = 0) : a = b :=
+sub_eq_zero.1 $ abs_eq_zero.1 h
+
+lemma abs_sub_le (a b c : α) : |a - c| ≤ |a - b| + |b - c| :=
+calc
+    |a - c| = |a - b + (b - c)|     : by rw [sub_add_sub_cancel]
+            ... ≤ |a - b| + |b - c| : abs_add _ _
+
+lemma abs_add_three (a b c : α) : |a + b + c| ≤ |a| + |b| + |c| :=
+(abs_add _ _).trans (add_le_add_right (abs_add _ _) _)
+
+lemma dist_bdd_within_interval {a b lb ub : α} (hal : lb ≤ a) (hau : a ≤ ub)
+      (hbl : lb ≤ b) (hbu : b ≤ ub) : |a - b| ≤ ub - lb :=
+abs_sub_le_iff.2 ⟨sub_le_sub hau hbl, sub_le_sub hbu hal⟩
+
+lemma eq_of_abs_sub_nonpos (h : |a - b| ≤ 0) : a = b :=
+eq_of_abs_sub_eq_zero (le_antisymm h (abs_nonneg (a - b)))
+
+end linear_ordered_add_comm_group
diff --git a/src/algebra/order/group/basic.lean b/src/algebra/order/group/basic.lean
index 124b332a1a080..cb1a67e54c780 100644
--- a/src/algebra/order/group/basic.lean
+++ b/src/algebra/order/group/basic.lean
@@ -3,13 +3,8 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 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.abs
 import algebra.order.sub.basic
-import algebra.order.monoid.min_max
-import algebra.order.monoid.prod
-import algebra.order.monoid.units
 import algebra.order.monoid.order_dual
-import algebra.order.monoid.with_top
 
 /-!
 # Ordered groups
@@ -50,14 +45,6 @@ instance ordered_comm_group.to_covariant_class_left_le (α : Type u) [ordered_co
 example (α : Type u) [ordered_add_comm_group α] : covariant_class α α (swap (+)) (<) :=
 add_right_cancel_semigroup.covariant_swap_add_lt_of_covariant_swap_add_le α
 
-/--The units of an ordered commutative monoid form an ordered commutative group. -/
-@[to_additive "The units of an ordered commutative additive monoid form an ordered commutative
-additive group."]
-instance units.ordered_comm_group [ordered_comm_monoid α] : ordered_comm_group αˣ :=
-{ mul_le_mul_left := λ a b h c, (mul_le_mul_left' (h : (a : α) ≤ b) _ :  (c : α) * a ≤ c * b),
-  .. units.partial_order,
-  .. units.comm_group }
-
 @[priority 100, to_additive]    -- see Note [lower instance priority]
 instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u)
   [s : ordered_comm_group α] :
@@ -65,11 +52,6 @@ instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u)
 { le_of_mul_le_mul_left := λ a b c, (mul_le_mul_iff_left a).mp,
   ..s }
 
-@[priority 100, to_additive] -- See note [lower instance priority]
-instance group.has_exists_mul_of_le (α : Type u) [group α] [has_le α] : has_exists_mul_of_le α :=
-⟨λ a b hab, ⟨a⁻¹ * b, (mul_inv_cancel_left _ _).symm⟩⟩
-
-
 @[to_additive] instance [ordered_comm_group α] : ordered_comm_group αᵒᵈ :=
 { .. order_dual.ordered_comm_monoid, .. order_dual.group }
 
@@ -562,6 +544,7 @@ by rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
 instance add_group.to_has_ordered_sub {α : Type*} [add_group α] [has_le α]
   [covariant_class α α (swap (+)) (≤)] : has_ordered_sub α :=
 ⟨λ a b c, sub_le_iff_le_add⟩
+
 /-- `equiv.mul_right` as an `order_iso`. See also `order_embedding.mul_right`. -/
 @[to_additive "`equiv.add_right` as an `order_iso`. See also `order_embedding.add_right`.",
   simps to_equiv apply {simp_rhs := tt}]
@@ -808,36 +791,8 @@ begin
   exact div_le_inv_mul_iff,
 end
 
-@[simp, to_additive] lemma max_one_div_max_inv_one_eq_self (a : α) :
-  max a 1 / max a⁻¹ 1 = a :=
-by { rcases le_total a 1 with h|h; simp [h] }
-
-alias max_zero_sub_max_neg_zero_eq_self ← max_zero_sub_eq_self
-
 end variable_names
 
-section densely_ordered
-variables [densely_ordered α] {a b c : α}
-
-@[to_additive]
-lemma le_of_forall_lt_one_mul_le (h : ∀ ε < 1, a * ε ≤ b) : a ≤ b :=
-@le_of_forall_one_lt_le_mul αᵒᵈ _ _ _ _ _ _ _ _ h
-
-@[to_additive]
-lemma le_of_forall_one_lt_div_le (h : ∀ ε : α, 1 < ε → a / ε ≤ b) : a ≤ b :=
-le_of_forall_lt_one_mul_le $ λ ε ε1,
-  by simpa only [div_eq_mul_inv, inv_inv]  using h ε⁻¹ (left.one_lt_inv_iff.2 ε1)
-
-@[to_additive]
-lemma le_iff_forall_one_lt_le_mul : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε :=
-⟨λ h ε ε_pos, le_mul_of_le_of_one_le h ε_pos.le, le_of_forall_one_lt_le_mul⟩
-
-@[to_additive]
-lemma le_iff_forall_lt_one_mul_le : a ≤ b ↔ ∀ ε < 1, a * ε ≤ b :=
-@le_iff_forall_one_lt_le_mul αᵒᵈ _ _ _ _ _ _
-
-end densely_ordered
-
 end linear_order
 
 /-!
@@ -899,30 +854,6 @@ lemma linear_ordered_comm_group.mul_lt_mul_left'
   (a b : α) (h : a < b) (c : α) : c * a < c * b :=
 mul_lt_mul_left' h c
 
-@[to_additive min_neg_neg]
-lemma min_inv_inv' (a b : α) : min (a⁻¹) (b⁻¹) = (max a b)⁻¹ :=
-eq.symm $ @monotone.map_max α αᵒᵈ _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
-
-@[to_additive max_neg_neg]
-lemma max_inv_inv' (a b : α) : max (a⁻¹) (b⁻¹) = (min a b)⁻¹ :=
-eq.symm $ @monotone.map_min α αᵒᵈ _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
-
-@[to_additive min_sub_sub_right]
-lemma min_div_div_right' (a b c : α) : min (a / c) (b / c) = min a b / c :=
-by simpa only [div_eq_mul_inv] using min_mul_mul_right a b (c⁻¹)
-
-@[to_additive max_sub_sub_right]
-lemma max_div_div_right' (a b c : α) : max (a / c) (b / c) = max a b / c :=
-by simpa only [div_eq_mul_inv] using max_mul_mul_right a b (c⁻¹)
-
-@[to_additive min_sub_sub_left]
-lemma min_div_div_left' (a b c : α) : min (a / b) (a / c) = a / max b c :=
-by simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']
-
-@[to_additive max_sub_sub_left]
-lemma max_div_div_left' (a b c : α) : max (a / b) (a / c) = a / min b c :=
-by simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']
-
 @[to_additive eq_zero_of_neg_eq]
 lemma eq_one_of_inv_eq' (h : a⁻¹ = a) : a = 1 :=
 match lt_trichotomy a 1 with
@@ -961,312 +892,6 @@ instance linear_ordered_comm_group.to_no_min_order [nontrivial α] : no_min_orde
 
 end linear_ordered_comm_group
 
-section covariant_add_le
-
-section has_neg
-
-/-- `abs a` is the absolute value of `a`. -/
-@[to_additive "`abs a` is the absolute value of `a`",
-  priority 100] -- see Note [lower instance priority]
-instance has_inv.to_has_abs [has_inv α] [has_sup α] : has_abs α := ⟨λ a, a ⊔ a⁻¹⟩
-
-@[to_additive] lemma abs_eq_sup_inv [has_inv α] [has_sup α] (a : α) : |a| = a ⊔ a⁻¹ := rfl
-
-variables [has_neg α] [linear_order α] {a b: α}
-
-lemma abs_eq_max_neg : abs a = max a (-a) :=
-rfl
-
-lemma abs_choice (x : α) : |x| = x ∨ |x| = -x := max_choice _ _
-
-lemma abs_le' : |a| ≤ b ↔ a ≤ b ∧ -a ≤ b := max_le_iff
-
-lemma le_abs : a ≤ |b| ↔ a ≤ b ∨ a ≤ -b := le_max_iff
-
-lemma le_abs_self (a : α) : a ≤ |a| := le_max_left _ _
-
-lemma neg_le_abs_self (a : α) : -a ≤ |a| := le_max_right _ _
-
-lemma lt_abs : a < |b| ↔ a < b ∨ a < -b := lt_max_iff
-
-theorem abs_le_abs (h₀ : a ≤ b) (h₁ : -a ≤ b) : |a| ≤ |b| :=
-(abs_le'.2 ⟨h₀, h₁⟩).trans (le_abs_self b)
-
-lemma abs_by_cases (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) : P (|a|) :=
-sup_ind _ _ h1 h2
-
-end has_neg
-
-section add_group
-variables [add_group α] [linear_order α]
-
-@[simp] lemma abs_neg (a : α) : | -a| = |a| :=
-begin
-  rw [abs_eq_max_neg, max_comm, neg_neg, abs_eq_max_neg]
-end
-
-lemma eq_or_eq_neg_of_abs_eq {a b : α} (h : |a| = b) : a = b ∨ a = -b :=
-by simpa only [← h, eq_comm, eq_neg_iff_eq_neg] using abs_choice a
-
-lemma abs_eq_abs {a b : α} : |a| = |b| ↔ a = b ∨ a = -b :=
-begin
-  refine ⟨λ h, _, λ h, _⟩,
-  { obtain rfl | rfl := eq_or_eq_neg_of_abs_eq h;
-    simpa only [neg_eq_iff_neg_eq, neg_inj, or.comm, @eq_comm _ (-b)] using abs_choice b },
-  { cases h; simp only [h, abs_neg] },
-end
-
-lemma abs_sub_comm (a b : α) : |a - b| = |b - a| :=
-calc  |a - b| = | - (b - a)| : congr_arg _ (neg_sub b a).symm
-          ... = |b - a|      : abs_neg (b - a)
-
-variables [covariant_class α α (+) (≤)] {a b c : α}
-
-lemma abs_of_nonneg (h : 0 ≤ a) : |a| = a :=
-max_eq_left $ (neg_nonpos.2 h).trans h
-
-lemma abs_of_pos (h : 0 < a) : |a| = a :=
-abs_of_nonneg h.le
-
-lemma abs_of_nonpos (h : a ≤ 0) : |a| = -a :=
-max_eq_right $ h.trans (neg_nonneg.2 h)
-
-lemma abs_of_neg (h : a < 0) : |a| = -a :=
-abs_of_nonpos h.le
-
-lemma abs_le_abs_of_nonneg (ha : 0 ≤ a) (hab : a ≤ b) : |a| ≤ |b| :=
-by rwa [abs_of_nonneg ha, abs_of_nonneg (ha.trans hab)]
-
-@[simp] lemma abs_zero : |0| = (0:α) :=
-abs_of_nonneg le_rfl
-
-@[simp] lemma abs_pos : 0 < |a| ↔ a ≠ 0 :=
-begin
-  rcases lt_trichotomy a 0 with (ha|rfl|ha),
-  { simp [abs_of_neg ha, neg_pos, ha.ne, ha] },
-  { simp },
-  { simp [abs_of_pos ha, ha, ha.ne.symm] }
-end
-
-lemma abs_pos_of_pos (h : 0 < a) : 0 < |a| := abs_pos.2 h.ne.symm
-
-lemma abs_pos_of_neg (h : a < 0) : 0 < |a| := abs_pos.2 h.ne
-
-lemma neg_abs_le_self (a : α) : -|a| ≤ a :=
-begin
-  cases le_total 0 a with h h,
-  { calc -|a| = - a   : congr_arg (has_neg.neg) (abs_of_nonneg h)
-            ... ≤ 0     : neg_nonpos.mpr h
-            ... ≤ a     : h },
-  { calc -|a| = - - a : congr_arg (has_neg.neg) (abs_of_nonpos h)
-            ... ≤ a     : (neg_neg a).le }
-end
-
-lemma add_abs_nonneg (a : α) : 0 ≤ a + |a| :=
-begin
-  rw ←add_right_neg a,
-  apply add_le_add_left,
-  exact (neg_le_abs_self a),
-end
-
-lemma neg_abs_le_neg (a : α) : -|a| ≤ -a :=
-by simpa using neg_abs_le_self (-a)
-
-@[simp] lemma abs_nonneg (a : α) : 0 ≤ |a| :=
-(le_total 0 a).elim (λ h, h.trans (le_abs_self a)) (λ h, (neg_nonneg.2 h).trans $ neg_le_abs_self a)
-
-@[simp] lemma abs_abs (a : α) : | |a| | = |a| :=
-abs_of_nonneg $ abs_nonneg a
-
-@[simp] lemma abs_eq_zero : |a| = 0 ↔ a = 0 :=
-decidable.not_iff_not.1 $ ne_comm.trans $ (abs_nonneg a).lt_iff_ne.symm.trans abs_pos
-
-@[simp] lemma abs_nonpos_iff {a : α} : |a| ≤ 0 ↔ a = 0 :=
-(abs_nonneg a).le_iff_eq.trans abs_eq_zero
-
-variable [covariant_class α α (swap (+)) (≤)]
-
-lemma abs_le_abs_of_nonpos (ha : a ≤ 0) (hab : b ≤ a) : |a| ≤ |b| :=
-by { rw [abs_of_nonpos ha, abs_of_nonpos (hab.trans ha)], exact neg_le_neg_iff.mpr hab }
-
-lemma abs_lt : |a| < b ↔ - b < a ∧ a < b :=
-max_lt_iff.trans $ and.comm.trans $ by rw [neg_lt]
-
-lemma neg_lt_of_abs_lt (h : |a| < b) : -b < a := (abs_lt.mp h).1
-
-lemma lt_of_abs_lt (h : |a| < b) : a < b := (abs_lt.mp h).2
-
-lemma max_sub_min_eq_abs' (a b : α) : max a b - min a b = |a - b| :=
-begin
-  cases le_total a b with ab ba,
-  { rw [max_eq_right ab, min_eq_left ab, abs_of_nonpos, neg_sub], rwa sub_nonpos },
-  { rw [max_eq_left ba, min_eq_right ba, abs_of_nonneg], rwa sub_nonneg }
-end
-
-lemma max_sub_min_eq_abs (a b : α) : max a b - min a b = |b - a| :=
-by { rw abs_sub_comm, exact max_sub_min_eq_abs' _ _ }
-
-end add_group
-
-end covariant_add_le
-
-section linear_ordered_add_comm_group
-
-variables [linear_ordered_add_comm_group α] {a b c d : α}
-
-lemma abs_le : |a| ≤ b ↔ - b ≤ a ∧ a ≤ b := by rw [abs_le', and.comm, neg_le]
-
-lemma le_abs' : a ≤ |b| ↔ b ≤ -a ∨ a ≤ b := by rw [le_abs, or.comm, le_neg]
-
-lemma neg_le_of_abs_le (h : |a| ≤ b) : -b ≤ a := (abs_le.mp h).1
-
-lemma le_of_abs_le (h : |a| ≤ b) : a ≤ b := (abs_le.mp h).2
-
-@[to_additive] lemma apply_abs_le_mul_of_one_le' {β : Type*} [mul_one_class β] [preorder β]
-  [covariant_class β β (*) (≤)] [covariant_class β β (swap (*)) (≤)] {f : α → β} {a : α}
-  (h₁ : 1 ≤ f a) (h₂ : 1 ≤ f (-a)) :
-  f (|a|) ≤ f a * f (-a) :=
-(le_total a 0).by_cases (λ ha, (abs_of_nonpos ha).symm ▸ le_mul_of_one_le_left' h₁)
-  (λ ha, (abs_of_nonneg ha).symm ▸ le_mul_of_one_le_right' h₂)
-
-@[to_additive] lemma apply_abs_le_mul_of_one_le {β : Type*} [mul_one_class β] [preorder β]
-  [covariant_class β β (*) (≤)] [covariant_class β β (swap (*)) (≤)] {f : α → β}
-  (h : ∀ x, 1 ≤ f x) (a : α) :
-  f (|a|) ≤ f a * f (-a) :=
-apply_abs_le_mul_of_one_le' (h _) (h _)
-
-/--
-The **triangle inequality** in `linear_ordered_add_comm_group`s.
--/
-lemma abs_add (a b : α) : |a + b| ≤ |a| + |b| :=
-abs_le.2 ⟨(neg_add (|a|) (|b|)).symm ▸
-  add_le_add (neg_le.2 $ neg_le_abs_self _) (neg_le.2 $ neg_le_abs_self _),
-  add_le_add (le_abs_self _) (le_abs_self _)⟩
-
-lemma abs_add' (a b : α) : |a| ≤ |b| + |b + a| :=
-by simpa using abs_add (-b) (b + a)
-
-theorem abs_sub (a b : α) :
-  |a - b| ≤ |a| + |b| :=
-by { rw [sub_eq_add_neg, ←abs_neg b], exact abs_add a _ }
-
-lemma abs_sub_le_iff : |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c :=
-by rw [abs_le, neg_le_sub_iff_le_add, sub_le_iff_le_add', and_comm, sub_le_iff_le_add']
-
-lemma abs_sub_lt_iff : |a - b| < c ↔ a - b < c ∧ b - a < c :=
-by rw [abs_lt, neg_lt_sub_iff_lt_add', sub_lt_iff_lt_add', and_comm, sub_lt_iff_lt_add']
-
-lemma sub_le_of_abs_sub_le_left (h : |a - b| ≤ c) : b - c ≤ a :=
-sub_le_comm.1 $ (abs_sub_le_iff.1 h).2
-
-lemma sub_le_of_abs_sub_le_right (h : |a - b| ≤ c) : a - c ≤ b :=
-sub_le_of_abs_sub_le_left (abs_sub_comm a b ▸ h)
-
-lemma sub_lt_of_abs_sub_lt_left (h : |a - b| < c) : b - c < a :=
-sub_lt_comm.1 $ (abs_sub_lt_iff.1 h).2
-
-lemma sub_lt_of_abs_sub_lt_right (h : |a - b| < c) : a - c < b :=
-sub_lt_of_abs_sub_lt_left (abs_sub_comm a b ▸ h)
-
-lemma abs_sub_abs_le_abs_sub (a b : α) : |a| - |b| ≤ |a - b| :=
-sub_le_iff_le_add.2 $
-calc |a| = |a - b + b|     : by rw [sub_add_cancel]
-       ... ≤ |a - b| + |b| : abs_add _ _
-
-lemma abs_abs_sub_abs_le_abs_sub (a b : α) : | |a| - |b| | ≤ |a - b| :=
-abs_sub_le_iff.2 ⟨abs_sub_abs_le_abs_sub _ _, by rw abs_sub_comm; apply abs_sub_abs_le_abs_sub⟩
-
-lemma abs_eq (hb : 0 ≤ b) : |a| = b ↔ a = b ∨ a = -b :=
-begin
-  refine ⟨eq_or_eq_neg_of_abs_eq, _⟩,
-  rintro (rfl|rfl); simp only [abs_neg, abs_of_nonneg hb]
-end
-
-lemma abs_le_max_abs_abs (hab : a ≤ b) (hbc : b ≤ c) : |b| ≤ max (|a|) (|c|) :=
-abs_le'.2
-  ⟨by simp [hbc.trans (le_abs_self c)],
-   by simp [(neg_le_neg_iff.mpr hab).trans (neg_le_abs_self a)]⟩
-
-lemma min_abs_abs_le_abs_max : min (|a|) (|b|) ≤ |max a b| :=
-(le_total a b).elim
-  (λ h, (min_le_right _ _).trans_eq $ congr_arg _ (max_eq_right h).symm)
-  (λ h, (min_le_left _ _).trans_eq $ congr_arg _ (max_eq_left h).symm)
-
-lemma min_abs_abs_le_abs_min : min (|a|) (|b|) ≤ |min a b| :=
-(le_total a b).elim
-  (λ h, (min_le_left _ _).trans_eq $ congr_arg _ (min_eq_left h).symm)
-  (λ h, (min_le_right _ _).trans_eq $ congr_arg _ (min_eq_right h).symm)
-
-lemma abs_max_le_max_abs_abs : |max a b| ≤ max (|a|) (|b|) :=
-(le_total a b).elim
-  (λ h, (congr_arg _ $ max_eq_right h).trans_le $ le_max_right _ _)
-  (λ h, (congr_arg _ $ max_eq_left h).trans_le $ le_max_left _ _)
-
-lemma abs_min_le_max_abs_abs : |min a b| ≤ max (|a|) (|b|) :=
-(le_total a b).elim
-  (λ h, (congr_arg _ $ min_eq_left h).trans_le $ le_max_left _ _)
-  (λ h, (congr_arg _ $ min_eq_right h).trans_le $ le_max_right _ _)
-
-lemma eq_of_abs_sub_eq_zero {a b : α} (h : |a - b| = 0) : a = b :=
-sub_eq_zero.1 $ abs_eq_zero.1 h
-
-lemma abs_sub_le (a b c : α) : |a - c| ≤ |a - b| + |b - c| :=
-calc
-    |a - c| = |a - b + (b - c)|     : by rw [sub_add_sub_cancel]
-            ... ≤ |a - b| + |b - c| : abs_add _ _
-
-lemma abs_add_three (a b c : α) : |a + b + c| ≤ |a| + |b| + |c| :=
-(abs_add _ _).trans (add_le_add_right (abs_add _ _) _)
-
-lemma dist_bdd_within_interval {a b lb ub : α} (hal : lb ≤ a) (hau : a ≤ ub)
-      (hbl : lb ≤ b) (hbu : b ≤ ub) : |a - b| ≤ ub - lb :=
-abs_sub_le_iff.2 ⟨sub_le_sub hau hbl, sub_le_sub hbu hal⟩
-
-lemma eq_of_abs_sub_nonpos (h : |a - b| ≤ 0) : a = b :=
-eq_of_abs_sub_eq_zero (le_antisymm h (abs_nonneg (a - b)))
-
-lemma max_sub_max_le_max (a b c d : α) : max a b - max c d ≤ max (a - c) (b - d) :=
-begin
-  simp only [sub_le_iff_le_add, max_le_iff], split,
-  calc a = a - c + c : (sub_add_cancel a c).symm
-  ... ≤ max (a - c) (b - d) + max c d : add_le_add (le_max_left _ _) (le_max_left _ _),
-  calc b = b - d + d : (sub_add_cancel b d).symm
-  ... ≤ max (a - c) (b - d) + max c d : add_le_add (le_max_right _ _) (le_max_right _ _)
-end
-
-lemma abs_max_sub_max_le_max (a b c d : α) : |max a b - max c d| ≤ max (|a - c|) (|b - d|) :=
-begin
-  refine abs_sub_le_iff.2 ⟨_, _⟩,
-  { exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _)) },
-  { rw [abs_sub_comm a c, abs_sub_comm b d],
-    exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _)) }
-end
-
-lemma abs_min_sub_min_le_max (a b c d : α) : |min a b - min c d| ≤ max (|a - c|) (|b - d|) :=
-by simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm]
-  using abs_max_sub_max_le_max (-a) (-b) (-c) (-d)
-
-lemma abs_max_sub_max_le_abs (a b c : α) : |max a c - max b c| ≤ |a - b| :=
-by simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg _)]
-  using abs_max_sub_max_le_max a c b c
-
-instance with_top.linear_ordered_add_comm_group_with_top :
-  linear_ordered_add_comm_group_with_top (with_top α) :=
-{ neg            := option.map (λ a : α, -a),
-  neg_top        := @option.map_none _ _ (λ a : α, -a),
-  add_neg_cancel := begin
-    rintro (a | a) ha,
-    { exact (ha rfl).elim },
-    { exact with_top.coe_add.symm.trans (with_top.coe_eq_coe.2 (add_neg_self a)) }
-  end,
-  .. with_top.linear_ordered_add_comm_monoid_with_top,
-  .. option.nontrivial }
-
-@[simp, norm_cast]
-lemma with_top.coe_neg (a : α) : ((-a : α) : with_top α) = -a := rfl
-
-end linear_ordered_add_comm_group
-
 namespace add_comm_group
 
 /-- A collection of elements in an `add_comm_group` designated as "non-negative".
@@ -1329,17 +954,6 @@ def mk_of_positive_cone {α : Type*} [add_comm_group α] (C : total_positive_con
 
 end linear_ordered_add_comm_group
 
-namespace prod
-
-variables {G H : Type*}
-
-@[to_additive]
-instance [ordered_comm_group G] [ordered_comm_group H] :
-  ordered_comm_group (G × H) :=
-{ .. prod.comm_group, .. prod.partial_order G H, .. prod.ordered_cancel_comm_monoid }
-
-end prod
-
 section norm_num_lemmas
 /- The following lemmas are stated so that the `norm_num` tactic can use them with the
 expected signatures.  -/
diff --git a/src/algebra/order/group/bounds.lean b/src/algebra/order/group/bounds.lean
new file mode 100644
index 0000000000000..3f42c06822f28
--- /dev/null
+++ b/src/algebra/order/group/bounds.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Yury Kudryashov
+-/
+import order.bounds.basic
+import algebra.order.group.basic
+
+/-!
+# Least upper bound and the greatest lower bound in linear ordered additive commutative groups
+-/
+
+variables {α : Type*}
+
+section linear_ordered_add_comm_group
+
+variables [linear_ordered_add_comm_group α] {s : set α} {a ε : α}
+
+lemma is_glb.exists_between_self_add (h : is_glb s a) (hε : 0 < ε) :
+  ∃ b ∈ s, a ≤ b ∧ b < a + ε :=
+h.exists_between $ lt_add_of_pos_right _ hε
+
+lemma is_glb.exists_between_self_add' (h : is_glb s a) (h₂ : a ∉ s) (hε : 0 < ε) :
+  ∃ b ∈ s, a < b ∧ b < a + ε :=
+h.exists_between' h₂ $ lt_add_of_pos_right _ hε
+
+lemma is_lub.exists_between_sub_self  (h : is_lub s a) (hε : 0 < ε) : ∃ b ∈ s, a - ε < b ∧ b ≤ a :=
+h.exists_between $ sub_lt_self _ hε
+
+lemma is_lub.exists_between_sub_self' (h : is_lub s a) (h₂ : a ∉ s) (hε : 0 < ε) :
+  ∃ b ∈ s, a - ε < b ∧ b < a :=
+h.exists_between' h₂ $ sub_lt_self _ hε
+
+end linear_ordered_add_comm_group
diff --git a/src/algebra/order/group/densely_ordered.lean b/src/algebra/order/group/densely_ordered.lean
new file mode 100644
index 0000000000000..cedc235ee20c2
--- /dev/null
+++ b/src/algebra/order/group/densely_ordered.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+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.order.group.basic
+import algebra.order.monoid.canonical
+
+/-!
+# Lemmas about densely linearly ordered groups.
+-/
+
+variables {α : Type*}
+
+section densely_ordered
+variables [group α] [linear_order α]
+variables [covariant_class α α (*) (≤)]
+variables [densely_ordered α] {a b c : α}
+
+@[to_additive]
+lemma le_of_forall_lt_one_mul_le (h : ∀ ε < 1, a * ε ≤ b) : a ≤ b :=
+@le_of_forall_one_lt_le_mul αᵒᵈ _ _ _ _ _ _ _ _ h
+
+@[to_additive]
+lemma le_of_forall_one_lt_div_le (h : ∀ ε : α, 1 < ε → a / ε ≤ b) : a ≤ b :=
+le_of_forall_lt_one_mul_le $ λ ε ε1,
+  by simpa only [div_eq_mul_inv, inv_inv]  using h ε⁻¹ (left.one_lt_inv_iff.2 ε1)
+
+@[to_additive]
+lemma le_iff_forall_one_lt_le_mul : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε :=
+⟨λ h ε ε_pos, le_mul_of_le_of_one_le h ε_pos.le, le_of_forall_one_lt_le_mul⟩
+
+@[to_additive]
+lemma le_iff_forall_lt_one_mul_le : a ≤ b ↔ ∀ ε < 1, a * ε ≤ b :=
+@le_iff_forall_one_lt_le_mul αᵒᵈ _ _ _ _ _ _
+
+end densely_ordered
diff --git a/src/algebra/order/group/min_max.lean b/src/algebra/order/group/min_max.lean
new file mode 100644
index 0000000000000..adefb7abbb2ca
--- /dev/null
+++ b/src/algebra/order/group/min_max.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+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.order.group.abs
+import algebra.order.monoid.min_max
+
+/-!
+# `min` and `max` in linearly ordered groups.
+-/
+
+section
+variables {α : Type*} [group α] [linear_order α] [covariant_class α α (*) (≤)]
+
+@[simp, to_additive] lemma max_one_div_max_inv_one_eq_self (a : α) :
+  max a 1 / max a⁻¹ 1 = a :=
+by { rcases le_total a 1 with h|h; simp [h] }
+
+alias max_zero_sub_max_neg_zero_eq_self ← max_zero_sub_eq_self
+
+end
+
+section linear_ordered_comm_group
+variables {α : Type*} [linear_ordered_comm_group α] {a b c : α}
+
+@[to_additive min_neg_neg]
+lemma min_inv_inv' (a b : α) : min (a⁻¹) (b⁻¹) = (max a b)⁻¹ :=
+eq.symm $ @monotone.map_max α αᵒᵈ _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
+
+@[to_additive max_neg_neg]
+lemma max_inv_inv' (a b : α) : max (a⁻¹) (b⁻¹) = (min a b)⁻¹ :=
+eq.symm $ @monotone.map_min α αᵒᵈ _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
+
+@[to_additive min_sub_sub_right]
+lemma min_div_div_right' (a b c : α) : min (a / c) (b / c) = min a b / c :=
+by simpa only [div_eq_mul_inv] using min_mul_mul_right a b (c⁻¹)
+
+@[to_additive max_sub_sub_right]
+lemma max_div_div_right' (a b c : α) : max (a / c) (b / c) = max a b / c :=
+by simpa only [div_eq_mul_inv] using max_mul_mul_right a b (c⁻¹)
+
+@[to_additive min_sub_sub_left]
+lemma min_div_div_left' (a b c : α) : min (a / b) (a / c) = a / max b c :=
+by simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']
+
+@[to_additive max_sub_sub_left]
+lemma max_div_div_left' (a b c : α) : max (a / b) (a / c) = a / min b c :=
+by simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']
+
+end linear_ordered_comm_group
+
+section linear_ordered_add_comm_group
+variables {α : Type*} [linear_ordered_add_comm_group α] {a b c : α}
+
+lemma max_sub_max_le_max (a b c d : α) : max a b - max c d ≤ max (a - c) (b - d) :=
+begin
+  simp only [sub_le_iff_le_add, max_le_iff], split,
+  calc a = a - c + c : (sub_add_cancel a c).symm
+  ... ≤ max (a - c) (b - d) + max c d : add_le_add (le_max_left _ _) (le_max_left _ _),
+  calc b = b - d + d : (sub_add_cancel b d).symm
+  ... ≤ max (a - c) (b - d) + max c d : add_le_add (le_max_right _ _) (le_max_right _ _)
+end
+
+lemma abs_max_sub_max_le_max (a b c d : α) : |max a b - max c d| ≤ max (|a - c|) (|b - d|) :=
+begin
+  refine abs_sub_le_iff.2 ⟨_, _⟩,
+  { exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _)) },
+  { rw [abs_sub_comm a c, abs_sub_comm b d],
+    exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _)) }
+end
+
+lemma abs_min_sub_min_le_max (a b c d : α) : |min a b - min c d| ≤ max (|a - c|) (|b - d|) :=
+by simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm]
+  using abs_max_sub_max_le_max (-a) (-b) (-c) (-d)
+
+lemma abs_max_sub_max_le_abs (a b c : α) : |max a c - max b c| ≤ |a - b| :=
+by simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg _)]
+  using abs_max_sub_max_le_max a c b c
+
+end linear_ordered_add_comm_group
diff --git a/src/algebra/order/group/prod.lean b/src/algebra/order/group/prod.lean
new file mode 100644
index 0000000000000..2912a9e4474d1
--- /dev/null
+++ b/src/algebra/order/group/prod.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+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.order.group.basic
+import algebra.order.monoid.prod
+
+/-!
+# Products of ordered commutative groups.
+-/
+
+variable {α : Type*}
+
+namespace prod
+
+variables {G H : Type*}
+
+@[to_additive]
+instance [ordered_comm_group G] [ordered_comm_group H] :
+  ordered_comm_group (G × H) :=
+{ .. prod.comm_group, .. prod.partial_order G H, .. prod.ordered_cancel_comm_monoid }
+
+end prod
diff --git a/src/algebra/order/group/units.lean b/src/algebra/order/group/units.lean
new file mode 100644
index 0000000000000..7a83791187aaf
--- /dev/null
+++ b/src/algebra/order/group/units.lean
@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+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.order.group.basic
+import algebra.order.monoid.units
+
+/-!
+# Adjoining a top element to a `linear_ordered_add_comm_group_with_top`.
+-/
+
+variable {α : Type*}
+
+/-- The units of an ordered commutative monoid form an ordered commutative group. -/
+@[to_additive "The units of an ordered commutative additive monoid form an ordered commutative
+additive group."]
+instance units.ordered_comm_group [ordered_comm_monoid α] : ordered_comm_group αˣ :=
+{ mul_le_mul_left := λ a b h c, (mul_le_mul_left' (h : (a : α) ≤ b) _ :  (c : α) * a ≤ c * b),
+  .. units.partial_order,
+  .. units.comm_group }
diff --git a/src/algebra/order/group/with_top.lean b/src/algebra/order/group/with_top.lean
new file mode 100644
index 0000000000000..012955c4aa09c
--- /dev/null
+++ b/src/algebra/order/group/with_top.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+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.order.group.basic
+import algebra.order.monoid.with_top
+
+/-!
+# Adjoining a top element to a `linear_ordered_add_comm_group_with_top`.
+-/
+
+variable {α : Type*}
+
+section linear_ordered_add_comm_group
+variables [linear_ordered_add_comm_group α] {a b c d : α}
+
+instance with_top.linear_ordered_add_comm_group_with_top :
+  linear_ordered_add_comm_group_with_top (with_top α) :=
+{ neg            := option.map (λ a : α, -a),
+  neg_top        := @option.map_none _ _ (λ a : α, -a),
+  add_neg_cancel := begin
+    rintro (a | a) ha,
+    { exact (ha rfl).elim },
+    { exact with_top.coe_add.symm.trans (with_top.coe_eq_coe.2 (add_neg_self a)) }
+  end,
+  .. with_top.linear_ordered_add_comm_monoid_with_top,
+  .. option.nontrivial }
+
+@[simp, norm_cast]
+lemma with_top.coe_neg (a : α) : ((-a : α) : with_top α) = -a := rfl
+
+end linear_ordered_add_comm_group
diff --git a/src/algebra/order/hom/ring.lean b/src/algebra/order/hom/ring.lean
index 2f86a97b9bb63..12b15382e7496 100644
--- a/src/algebra/order/hom/ring.lean
+++ b/src/algebra/order/hom/ring.lean
@@ -5,7 +5,7 @@ Authors: Alex J. Best, Yaël Dillies
 -/
 import algebra.order.archimedean
 import algebra.order.hom.monoid
-import algebra.order.ring
+import algebra.order.ring.basic
 import algebra.ring.equiv
 
 /-!
diff --git a/src/algebra/order/invertible.lean b/src/algebra/order/invertible.lean
index bc3687733354b..e2677da2e6068 100644
--- a/src/algebra/order/invertible.lean
+++ b/src/algebra/order/invertible.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
-import algebra.order.ring
+import algebra.order.ring.basic
 import algebra.invertible
 
 /-!
diff --git a/src/algebra/order/lattice_group.lean b/src/algebra/order/lattice_group.lean
index 05fc3f40c9749..2a18a28a237f6 100644
--- a/src/algebra/order/lattice_group.lean
+++ b/src/algebra/order/lattice_group.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 -/
 import algebra.group_power.basic -- Needed for squares
-import algebra.order.group.basic
+import algebra.order.group.abs
 import tactic.nth_rewrite
 
 /-!
diff --git a/src/algebra/order/monoid/canonical.lean b/src/algebra/order/monoid/canonical.lean
index 91cf2101371ba..f84882b55b98f 100644
--- a/src/algebra/order/monoid/canonical.lean
+++ b/src/algebra/order/monoid/canonical.lean
@@ -33,6 +33,10 @@ export has_exists_mul_of_le (exists_mul_of_le)
 
 export has_exists_add_of_le (exists_add_of_le)
 
+@[priority 100, to_additive] -- See note [lower instance priority]
+instance group.has_exists_mul_of_le (α : Type u) [group α] [has_le α] : has_exists_mul_of_le α :=
+⟨λ a b hab, ⟨a⁻¹ * b, (mul_inv_cancel_left _ _).symm⟩⟩
+
 section mul_one_class
 variables [mul_one_class α] [preorder α] [contravariant_class α α (*) (<)] [has_exists_mul_of_le α]
   {a b : α}
diff --git a/src/algebra/order/nonneg/ring.lean b/src/algebra/order/nonneg/ring.lean
index bad80c132a9c7..ff60acf5db16d 100644
--- a/src/algebra/order/nonneg/ring.lean
+++ b/src/algebra/order/nonneg/ring.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import algebra.order.ring
+import algebra.order.ring.basic
 import order.complete_lattice_intervals
 import order.lattice_intervals
 
diff --git a/src/algebra/order/pi.lean b/src/algebra/order/pi.lean
index 4fec41bd73187..0086c3a5d5e38 100644
--- a/src/algebra/order/pi.lean
+++ b/src/algebra/order/pi.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
-import algebra.order.ring
+import algebra.order.ring.basic
 import algebra.ring.pi
 import tactic.positivity
 
diff --git a/src/algebra/order/positive/ring.lean b/src/algebra/order/positive/ring.lean
index a4fbe05a928d8..944a0ae69aafe 100644
--- a/src/algebra/order/positive/ring.lean
+++ b/src/algebra/order/positive/ring.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import algebra.order.ring
+import algebra.order.ring.basic
 
 /-!
 # Algebraic structures on the set of positive numbers
diff --git a/src/algebra/order/ring/abs.lean b/src/algebra/order/ring/abs.lean
new file mode 100644
index 0000000000000..246d43deaed4f
--- /dev/null
+++ b/src/algebra/order/ring/abs.lean
@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+-/
+
+import algebra.order.ring.basic
+import algebra.ring.divisibility
+import algebra.order.group.abs
+
+/-!
+# Absolute values in linear ordered rings.
+-/
+
+variables {α : Type*}
+
+section linear_ordered_ring
+variables [linear_ordered_ring α] {a b c : α}
+
+@[simp] lemma abs_one : |(1 : α)| = 1 := abs_of_pos zero_lt_one
+@[simp] lemma abs_two : |(2 : α)| = 2 := abs_of_pos zero_lt_two
+
+lemma abs_mul (a b : α) : |a * b| = |a| * |b| :=
+begin
+  rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))],
+  cases le_total a 0 with ha ha; cases le_total b 0 with hb hb;
+    simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, eq_self_iff_true,
+      neg_mul, mul_neg, neg_neg, *]
+end
+
+/-- `abs` as a `monoid_with_zero_hom`. -/
+def abs_hom : α →*₀ α := ⟨abs, abs_zero, abs_one, abs_mul⟩
+
+@[simp] lemma abs_mul_abs_self (a : α) : |a| * |a| = a * a :=
+abs_by_cases (λ x, x * x = a * a) rfl (neg_mul_neg a a)
+
+@[simp] lemma abs_mul_self (a : α) : |a * a| = a * a :=
+by rw [abs_mul, abs_mul_abs_self]
+
+@[simp] lemma abs_eq_self : |a| = a ↔ 0 ≤ a := by simp [abs_eq_max_neg]
+
+@[simp] lemma abs_eq_neg_self : |a| = -a ↔ a ≤ 0 := by simp [abs_eq_max_neg]
+
+/-- For an element `a` of a linear ordered ring, either `abs a = a` and `0 ≤ a`,
+    or `abs a = -a` and `a < 0`.
+    Use cases on this lemma to automate linarith in inequalities -/
+lemma abs_cases (a : α) : (|a| = a ∧ 0 ≤ a) ∨ (|a| = -a ∧ a < 0) :=
+begin
+  by_cases 0 ≤ a,
+  { left,
+    exact ⟨abs_eq_self.mpr h, h⟩ },
+  { right,
+    push_neg at h,
+    exact ⟨abs_eq_neg_self.mpr (le_of_lt h), h⟩ }
+end
+
+@[simp] lemma max_zero_add_max_neg_zero_eq_abs_self (a : α) :
+  max a 0 + max (-a) 0 = |a| :=
+begin
+  symmetry,
+  rcases le_total 0 a with ha|ha;
+  simp [ha],
+end
+
+lemma abs_eq_iff_mul_self_eq : |a| = |b| ↔ a * a = b * b :=
+begin
+  rw [← abs_mul_abs_self, ← abs_mul_abs_self b],
+  exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm,
+end
+
+lemma abs_lt_iff_mul_self_lt : |a| < |b| ↔ a * a < b * b :=
+begin
+  rw [← abs_mul_abs_self, ← abs_mul_abs_self b],
+  exact mul_self_lt_mul_self_iff (abs_nonneg a) (abs_nonneg b)
+end
+
+lemma abs_le_iff_mul_self_le : |a| ≤ |b| ↔ a * a ≤ b * b :=
+begin
+  rw [← abs_mul_abs_self, ← abs_mul_abs_self b],
+  exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)
+end
+
+lemma abs_le_one_iff_mul_self_le_one : |a| ≤ 1 ↔ a * a ≤ 1 :=
+by simpa only [abs_one, one_mul] using @abs_le_iff_mul_self_le α _ a 1
+
+end linear_ordered_ring
+
+section linear_ordered_comm_ring
+
+variables [linear_ordered_comm_ring α] {a b c d : α}
+
+lemma abs_sub_sq (a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b :=
+begin
+  rw abs_mul_abs_self,
+  simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg,
+    mul_one, mul_neg, neg_add_rev, neg_neg],
+end
+
+end linear_ordered_comm_ring
+
+section
+variables [ring α] [linear_order α] {a b : α}
+
+@[simp] lemma abs_dvd (a b : α) : |a| ∣ b ↔ a ∣ b :=
+by { cases abs_choice a with h h; simp only [h, neg_dvd] }
+
+lemma abs_dvd_self (a : α) : |a| ∣ a :=
+(abs_dvd a a).mpr (dvd_refl a)
+
+@[simp] lemma dvd_abs (a b : α) : a ∣ |b| ↔ a ∣ b :=
+by { cases abs_choice b with h h; simp only [h, dvd_neg] }
+
+lemma self_dvd_abs (a : α) : a ∣ |a| :=
+(dvd_abs a a).mpr (dvd_refl a)
+
+lemma abs_dvd_abs (a b : α) : |a| ∣ |b| ↔ a ∣ b :=
+(abs_dvd _ _).trans (dvd_abs _ _)
+
+end
diff --git a/src/algebra/order/ring.lean b/src/algebra/order/ring/basic.lean
similarity index 75%
rename from src/algebra/order/ring.lean
rename to src/algebra/order/ring/basic.lean
index c785ba65fec11..69cc1d4372506 100644
--- a/src/algebra/order/ring.lean
+++ b/src/algebra/order/ring/basic.lean
@@ -3,12 +3,9 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
-import algebra.char_zero.defs
-import algebra.ring.divisibility
-import algebra.hom.ring
+import order.min_max
 import algebra.order.group.basic
-import algebra.order.sub.canonical
-import algebra.order.ring_lemmas
+import algebra.order.ring.lemmas
 
 /-!
 # Ordered rings and semirings
@@ -93,23 +90,13 @@ immediate predecessors and what conditions are added to each of them.
   - `linear_ordered_ring` & commutativity of multiplication
   - `linear_ordered_comm_semiring` & additive inverses
   - `is_domain` & linear order structure
-* `canonically_ordered_comm_semiring`
-  - `canonically_ordered_add_monoid` & multiplication & `*` respects `≤` & no zero divisors
-  - `comm_semiring` & `a ≤ b ↔ ∃ c, b = a + c` & no zero divisors
 
-## TODO
-
-We're still missing some typeclasses, like
-* `canonically_ordered_semiring`
-They have yet to come up in practice.
 -/
 
 open function
 
 set_option old_structure_cmd true
 
-open function
-
 universe u
 variables {α : Type u} {β : Type*}
 
@@ -197,13 +184,6 @@ monotone and multiplication by a positive number is strictly monotone. -/
 @[protect_proj]
 class linear_ordered_comm_ring (α : Type u) extends linear_ordered_ring α, comm_monoid α
 
-/-- A canonically ordered commutative semiring is an ordered, commutative semiring in which `a ≤ b`
-iff there exists `c` with `b = a + c`. This is satisfied by the natural numbers, for example, but
-not the integers or other ordered groups. -/
-@[protect_proj]
-class canonically_ordered_comm_semiring (α : Type*) extends
-  canonically_ordered_add_monoid α, comm_semiring α :=
-(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0)
 
 section ordered_semiring
 variables [ordered_semiring α] {a b c d : α}
@@ -560,42 +540,8 @@ order_embedding.of_strict_mono coe nat.strict_mono_cast
 instance strict_ordered_semiring.to_no_max_order : no_max_order α :=
 ⟨λ a, ⟨a + 1, lt_add_of_pos_right _ one_pos⟩⟩
 
-/-- Note this is not an instance as `char_zero` implies `nontrivial`, and this would risk forming a
-loop. -/
-lemma strict_ordered_semiring.to_char_zero : char_zero α := ⟨nat.strict_mono_cast.injective⟩
-
 end nontrivial
 
-section has_exists_add_of_le
-variables [has_exists_add_of_le α]
-
-/-- Binary **rearrangement inequality**. -/
-lemma mul_add_mul_le_mul_add_mul (hab : a ≤ b) (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d :=
-begin
-  obtain ⟨b, rfl⟩ := exists_add_of_le hab,
-  obtain ⟨d, rfl⟩ := exists_add_of_le hcd,
-  rw [mul_add, add_right_comm, mul_add, ←add_assoc],
-  exact add_le_add_left (mul_le_mul_of_nonneg_right hab $ (le_add_iff_nonneg_right _).1 hcd) _,
-end
-
-/-- Binary **rearrangement inequality**. -/
-lemma mul_add_mul_le_mul_add_mul' (hba : b ≤ a) (hdc : d ≤ c) : a • d + b • c ≤ a • c + b • d :=
-by { rw [add_comm (a • d), add_comm (a • c)], exact mul_add_mul_le_mul_add_mul hba hdc }
-
-/-- Binary strict **rearrangement inequality**. -/
-lemma mul_add_mul_lt_mul_add_mul (hab : a < b) (hcd : c < d) : a * d + b * c < a * c + b * d :=
-begin
-  obtain ⟨b, rfl⟩ := exists_add_of_le hab.le,
-  obtain ⟨d, rfl⟩ := exists_add_of_le hcd.le,
-  rw [mul_add, add_right_comm, mul_add, ←add_assoc],
-  exact add_lt_add_left (mul_lt_mul_of_pos_right hab $ (lt_add_iff_pos_right _).1 hcd) _,
-end
-
-/-- Binary **rearrangement inequality**. -/
-lemma mul_add_mul_lt_mul_add_mul' (hba : b < a) (hdc : d < c) : a • d + b • c < a • c + b • d :=
-by { rw [add_comm (a • d), add_comm (a • c)], exact mul_add_mul_lt_mul_add_mul hba hdc }
-
-end has_exists_add_of_le
 end strict_ordered_semiring
 
 section strict_ordered_comm_semiring
@@ -823,10 +769,6 @@ have ∀ {u : αˣ}, ↑u < (0 : α) → ↑u⁻¹ < (0 : α) := λ u h,
   neg_of_mul_pos_right (by exact (u.mul_inv.symm ▸ zero_lt_one)) h.le,
 ⟨this, this⟩
 
-@[priority 100] -- see Note [lower instance priority]
-instance linear_ordered_semiring.to_char_zero : char_zero α :=
-strict_ordered_semiring.to_char_zero
-
 lemma cmp_mul_pos_left (ha : 0 < a) (b c : α) : cmp (a * b) (a * c) = cmp b c :=
 (strict_mono_mul_left_of_pos ha).cmp_map_eq b c
 
@@ -892,26 +834,6 @@ instance linear_ordered_ring.is_domain : is_domain α :=
     end,
   .. ‹linear_ordered_ring α› }
 
-@[simp] lemma abs_one : |(1 : α)| = 1 := abs_of_pos zero_lt_one
-@[simp] lemma abs_two : |(2 : α)| = 2 := abs_of_pos zero_lt_two
-
-lemma abs_mul (a b : α) : |a * b| = |a| * |b| :=
-begin
-  rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))],
-  cases le_total a 0 with ha ha; cases le_total b 0 with hb hb;
-    simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, eq_self_iff_true,
-      neg_mul, mul_neg, neg_neg, *]
-end
-
-/-- `abs` as a `monoid_with_zero_hom`. -/
-def abs_hom : α →*₀ α := ⟨abs, abs_zero, abs_one, abs_mul⟩
-
-@[simp] lemma abs_mul_abs_self (a : α) : |a| * |a| = a * a :=
-abs_by_cases (λ x, x * x = a * a) rfl (neg_mul_neg a a)
-
-@[simp] lemma abs_mul_self (a : α) : |a * a| = a * a :=
-by rw [abs_mul, abs_mul_abs_self]
-
 lemma mul_pos_iff : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 :=
 ⟨pos_and_pos_or_neg_and_neg_of_mul_pos,
   λ h, h.elim (and_imp.2 mul_pos) (and_imp.2 mul_pos_of_neg_of_neg)⟩
@@ -933,7 +855,7 @@ lemma mul_nonpos_iff : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤
 by rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff, neg_nonneg, neg_nonpos]
 
 lemma mul_self_nonneg (a : α) : 0 ≤ a * a :=
-abs_mul_self a ▸ abs_nonneg _
+(le_total 0 a).elim (λ h, mul_nonneg h h) (λ h, mul_nonneg_of_nonpos_of_nonpos h h)
 
 @[simp] lemma neg_le_self_iff : -a ≤ a ↔ 0 ≤ a :=
 by simp [neg_le_iff_add_nonneg, ← two_mul, mul_nonneg_iff, zero_le_one, (@zero_lt_two α _ _).not_le]
@@ -951,31 +873,6 @@ calc a < -a ↔ -(-a) < -a : by rw neg_neg
 ... ↔ 0 < -a : neg_lt_self_iff
 ... ↔ a < 0 : neg_pos
 
-@[simp] lemma abs_eq_self : |a| = a ↔ 0 ≤ a := by simp [abs_eq_max_neg]
-
-@[simp] lemma abs_eq_neg_self : |a| = -a ↔ a ≤ 0 := by simp [abs_eq_max_neg]
-
-/-- For an element `a` of a linear ordered ring, either `abs a = a` and `0 ≤ a`,
-    or `abs a = -a` and `a < 0`.
-    Use cases on this lemma to automate linarith in inequalities -/
-lemma abs_cases (a : α) : (|a| = a ∧ 0 ≤ a) ∨ (|a| = -a ∧ a < 0) :=
-begin
-  by_cases 0 ≤ a,
-  { left,
-    exact ⟨abs_eq_self.mpr h, h⟩ },
-  { right,
-    push_neg at h,
-    exact ⟨abs_eq_neg_self.mpr (le_of_lt h), h⟩ }
-end
-
-@[simp] lemma max_zero_add_max_neg_zero_eq_abs_self (a : α) :
-  max a 0 + max (-a) 0 = |a| :=
-begin
-  symmetry,
-  rcases le_total 0 a with ha|ha;
-  simp [ha],
-end
-
 lemma neg_one_lt_zero : -1 < (0:α) := neg_lt_zero.2 zero_lt_one
 
 @[simp] lemma mul_le_mul_left_of_neg {a b c : α} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a :=
@@ -1015,10 +912,9 @@ begin
 end
 
 lemma mul_self_le_mul_self_of_le_of_neg_le {x y : α} (h₁ : x ≤ y) (h₂ : -x ≤ y) : x * x ≤ y * y :=
-begin
-  rw [← abs_mul_abs_self x],
-  exact mul_self_le_mul_self (abs_nonneg x) (abs_le.2 ⟨neg_le.2 h₂, h₁⟩)
-end
+(le_total 0 x).elim (λ h, mul_le_mul h₁ h₁ h (h.trans h₁))
+  (λ h, le_of_eq_of_le (neg_mul_neg x x).symm
+    (mul_le_mul h₂ h₂ (neg_nonneg.mpr h) ((neg_nonneg.mpr h).trans h₂)))
 
 lemma nonneg_of_mul_nonpos_left {a b : α} (h : a * b ≤ 0) (hb : b < 0) : 0 ≤ a :=
 le_of_not_gt (λ ha, absurd h (mul_pos_of_neg_of_neg ha hb).not_le)
@@ -1045,27 +941,6 @@ by rw [add_eq_zero_iff', mul_self_eq_zero, mul_self_eq_zero]; apply mul_self_non
 lemma eq_zero_of_mul_self_add_mul_self_eq_zero (h : a * a + b * b = 0) : a = 0 :=
 (mul_self_add_mul_self_eq_zero.mp h).left
 
-lemma abs_eq_iff_mul_self_eq : |a| = |b| ↔ a * a = b * b :=
-begin
-  rw [← abs_mul_abs_self, ← abs_mul_abs_self b],
-  exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm,
-end
-
-lemma abs_lt_iff_mul_self_lt : |a| < |b| ↔ a * a < b * b :=
-begin
-  rw [← abs_mul_abs_self, ← abs_mul_abs_self b],
-  exact mul_self_lt_mul_self_iff (abs_nonneg a) (abs_nonneg b)
-end
-
-lemma abs_le_iff_mul_self_le : |a| ≤ |b| ↔ a * a ≤ b * b :=
-begin
-  rw [← abs_mul_abs_self, ← abs_mul_abs_self b],
-  exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)
-end
-
-lemma abs_le_one_iff_mul_self_le_one : |a| ≤ 1 ↔ a * a ≤ 1 :=
-by simpa only [abs_one, one_mul] using @abs_le_iff_mul_self_le α _ a 1
-
 end linear_ordered_ring
 
 @[priority 100] -- see Note [lower instance priority]
@@ -1092,33 +967,7 @@ max_le
   (by simpa [mul_comm, max_comm] using ba)
   (by simpa [mul_comm, max_comm] using cd)
 
-lemma abs_sub_sq (a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b :=
-begin
-  rw abs_mul_abs_self,
-  simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg,
-    mul_one, mul_neg, neg_add_rev, neg_neg],
-end
-
 end linear_ordered_comm_ring
-section
-variables [ring α] [linear_order α] {a b : α}
-
-@[simp] lemma abs_dvd (a b : α) : |a| ∣ b ↔ a ∣ b :=
-by { cases abs_choice a with h h; simp only [h, neg_dvd] }
-
-lemma abs_dvd_self (a : α) : |a| ∣ a :=
-(abs_dvd a a).mpr (dvd_refl a)
-
-@[simp] lemma dvd_abs (a b : α) : a ∣ |b| ↔ a ∣ b :=
-by { cases abs_choice b with h h; simp only [h, dvd_neg] }
-
-lemma self_dvd_abs (a : α) : a ∣ |a| :=
-(dvd_abs a a).mpr (dvd_refl a)
-
-lemma abs_dvd_abs (a b : α) : |a| ∣ |b| ↔ a ∣ b :=
-(abs_dvd _ _).trans (dvd_abs _ _)
-
-end
 
 namespace function.injective
 
@@ -1358,329 +1207,3 @@ def mk_of_positive_cone {α : Type*} [ring α] (C : total_positive_cone α) :
   ..linear_ordered_add_comm_group.mk_of_positive_cone C.to_total_positive_cone, }
 
 end linear_ordered_ring
-
-namespace canonically_ordered_comm_semiring
-variables [canonically_ordered_comm_semiring α] {a b : α}
-
-@[priority 100] -- see Note [lower instance priority]
-instance to_no_zero_divisors : no_zero_divisors α :=
-⟨canonically_ordered_comm_semiring.eq_zero_or_eq_zero_of_mul_eq_zero⟩
-
-@[priority 100] -- see Note [lower instance priority]
-instance to_covariant_mul_le : covariant_class α α (*) (≤) :=
-begin
-  refine ⟨λ a b c h, _⟩,
-  rcases exists_add_of_le h with ⟨c, rfl⟩,
-  rw mul_add,
-  apply self_le_add_right
-end
-
-@[priority 100] -- see Note [lower instance priority]
-instance to_ordered_comm_semiring : ordered_comm_semiring α :=
-{ zero_le_one := zero_le _,
-  mul_le_mul_of_nonneg_left := λ a b c h _, mul_le_mul_left' h _,
-  mul_le_mul_of_nonneg_right := λ a b c h _, mul_le_mul_right' h _,
-  ..‹canonically_ordered_comm_semiring α› }
-
-@[simp] lemma mul_pos : 0 < a * b ↔ (0 < a) ∧ (0 < b) :=
-by simp only [pos_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
-
-
-end canonically_ordered_comm_semiring
-
-instance ne_zero.bit1 [canonically_ordered_comm_semiring α] [nontrivial α]
-  {x : α} : ne_zero (bit1 x) :=
-⟨mt (λ h, le_iff_exists_add'.2 ⟨_, h.symm⟩) zero_lt_one.not_le⟩
-
-section sub
-
-variables [canonically_ordered_comm_semiring α] {a b c : α}
-variables [has_sub α] [has_ordered_sub α]
-
-variables [is_total α (≤)]
-
-namespace add_le_cancellable
-protected lemma mul_tsub (h : add_le_cancellable (a * c)) :
-  a * (b - c) = a * b - a * c :=
-begin
-  cases total_of (≤) b c with hbc hcb,
-  { rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)] },
-  { apply h.eq_tsub_of_add_eq, rw [← mul_add, tsub_add_cancel_of_le hcb] }
-end
-
-protected lemma tsub_mul (h : add_le_cancellable (b * c)) : (a - b) * c = a * c - b * c :=
-by { simp only [mul_comm _ c] at *, exact h.mul_tsub }
-
-end add_le_cancellable
-
-variables [contravariant_class α α (+) (≤)]
-
-lemma mul_tsub (a b c : α) : a * (b - c) = a * b - a * c :=
-contravariant.add_le_cancellable.mul_tsub
-
-lemma tsub_mul (a b c : α) : (a - b) * c = a * c - b * c :=
-contravariant.add_le_cancellable.tsub_mul
-
-end sub
-
-/-! ### Structures involving `*` and `0` on `with_top` and `with_bot`
-
-The main results of this section are `with_top.canonically_ordered_comm_semiring` and
-`with_bot.comm_monoid_with_zero`.
--/
-
-namespace with_top
-
-instance [nonempty α] : nontrivial (with_top α) := option.nontrivial
-
-variable [decidable_eq α]
-
-section has_mul
-
-variables [has_zero α] [has_mul α]
-
-instance : mul_zero_class (with_top α) :=
-{ zero := 0,
-  mul := λ m n, if m = 0 ∨ n = 0 then 0 else m.bind (λa, n.bind $ λb, ↑(a * b)),
-  zero_mul := assume a, if_pos $ or.inl rfl,
-  mul_zero := assume a, if_pos $ or.inr rfl }
-
-lemma mul_def {a b : with_top α} :
-  a * b = if a = 0 ∨ b = 0 then 0 else a.bind (λa, b.bind $ λb, ↑(a * b)) := rfl
-
-@[simp] lemma mul_top {a : with_top α} (h : a ≠ 0) : a * ⊤ = ⊤ :=
-by cases a; simp [mul_def, h]; refl
-
-@[simp] lemma top_mul {a : with_top α} (h : a ≠ 0) : ⊤ * a = ⊤ :=
-by cases a; simp [mul_def, h]; refl
-
-@[simp] lemma top_mul_top : (⊤ * ⊤ : with_top α) = ⊤ :=
-top_mul top_ne_zero
-
-end has_mul
-
-section mul_zero_class
-
-variables [mul_zero_class α]
-
-@[norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_top α) = a * b :=
-decidable.by_cases (assume : a = 0, by simp [this]) $ assume ha,
-decidable.by_cases (assume : b = 0, by simp [this]) $ assume hb,
-by { simp [*, mul_def], refl }
-
-lemma mul_coe {b : α} (hb : b ≠ 0) : ∀{a : with_top α}, a * b = a.bind (λa:α, ↑(a * b))
-| none     := show (if (⊤:with_top α) = 0 ∨ (b:with_top α) = 0 then 0 else ⊤ : with_top α) = ⊤,
-    by simp [hb]
-| (some a) := show ↑a * ↑b = ↑(a * b), from coe_mul.symm
-
-@[simp] lemma mul_eq_top_iff {a b : with_top α} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
-begin
-  cases a; cases b; simp only [none_eq_top, some_eq_coe],
-  { simp [← coe_mul] },
-  { by_cases hb : b = 0; simp [hb] },
-  { by_cases ha : a = 0; simp [ha] },
-  { simp [← coe_mul] }
-end
-
-lemma mul_lt_top [preorder α] {a b : with_top α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b < ⊤ :=
-begin
-  lift a to α using ha,
-  lift b to α using hb,
-  simp only [← coe_mul, coe_lt_top]
-end
-
-@[simp] lemma untop'_zero_mul (a b : with_top α) : (a * b).untop' 0 = a.untop' 0 * b.untop' 0 :=
-begin
-  by_cases ha : a = 0, { rw [ha, zero_mul, ← coe_zero, untop'_coe, zero_mul] },
-  by_cases hb : b = 0, { rw [hb, mul_zero, ← coe_zero, untop'_coe, mul_zero] },
-  induction a using with_top.rec_top_coe, { rw [top_mul hb, untop'_top, zero_mul] },
-  induction b using with_top.rec_top_coe, { rw [mul_top ha, untop'_top, mul_zero] },
-  rw [← coe_mul, untop'_coe, untop'_coe, untop'_coe]
-end
-
-end mul_zero_class
-
-/-- `nontrivial α` is needed here as otherwise we have `1 * ⊤ = ⊤` but also `0 * ⊤ = 0`. -/
-instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_top α) :=
-{ mul := (*),
-  one := 1,
-  zero := 0,
-  one_mul := λ a, match a with
-  | ⊤       := mul_top (mt coe_eq_coe.1 one_ne_zero)
-  | (a : α) := by rw [← coe_one, ← coe_mul, one_mul]
-  end,
-  mul_one := λ a, match a with
-  | ⊤       := top_mul (mt coe_eq_coe.1 one_ne_zero)
-  | (a : α) := by rw [← coe_one, ← coe_mul, mul_one]
-  end,
-  .. with_top.mul_zero_class }
-
-/-- A version of `with_top.map` for `monoid_with_zero_hom`s. -/
-@[simps { fully_applied := ff }] protected def _root_.monoid_with_zero_hom.with_top_map
-  {R S : Type*} [mul_zero_one_class R] [decidable_eq R] [nontrivial R]
-  [mul_zero_one_class S] [decidable_eq S] [nontrivial S] (f : R →*₀ S) (hf : function.injective f) :
-  with_top R →*₀ with_top S :=
-{ to_fun := with_top.map f,
-  map_mul' := λ x y,
-    begin
-      have : ∀ z, map f z = 0 ↔ z = 0,
-        from λ z, (option.map_injective hf).eq_iff' f.to_zero_hom.with_top_map.map_zero,
-      rcases eq_or_ne x 0 with rfl|hx, { simp },
-      rcases eq_or_ne y 0 with rfl|hy, { simp },
-      induction x using with_top.rec_top_coe, { simp [hy, this] },
-      induction y using with_top.rec_top_coe,
-      { have : (f x : with_top S) ≠ 0, by simpa [hf.eq_iff' (map_zero f)] using hx,
-        simp [hx, this] },
-      simp [← coe_mul]
-    end,
-  .. f.to_zero_hom.with_top_map, .. f.to_monoid_hom.to_one_hom.with_top_map }
-
-instance [mul_zero_class α] [no_zero_divisors α] : no_zero_divisors (with_top α) :=
-⟨λ a b, by cases a; cases b; dsimp [mul_def]; split_ifs;
-  simp [*, none_eq_top, some_eq_coe, mul_eq_zero] at *⟩
-
-instance [semigroup_with_zero α] [no_zero_divisors α] : semigroup_with_zero (with_top α) :=
-{ mul := (*),
-  zero := 0,
-  mul_assoc := λ a b c, begin
-    rcases eq_or_ne a 0 with rfl|ha, { simp only [zero_mul] },
-    rcases eq_or_ne b 0 with rfl|hb, { simp only [zero_mul, mul_zero] },
-    rcases eq_or_ne c 0 with rfl|hc, { simp only [mul_zero] },
-    induction a using with_top.rec_top_coe, { simp [hb, hc] },
-    induction b using with_top.rec_top_coe, { simp [ha, hc] },
-    induction c using with_top.rec_top_coe, { simp [ha, hb] },
-    simp only [← coe_mul, mul_assoc]
-  end,
-  .. with_top.mul_zero_class }
-
-instance [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] : monoid_with_zero (with_top α) :=
-{ .. with_top.mul_zero_one_class, .. with_top.semigroup_with_zero }
-
-instance [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
-  comm_monoid_with_zero (with_top α) :=
-{ mul := (*),
-  zero := 0,
-  mul_comm := λ a b,
-    by simp only [or_comm, mul_def, option.bind_comm a b, mul_comm],
-  .. with_top.monoid_with_zero }
-
-variables [canonically_ordered_comm_semiring α]
-
-private lemma distrib' (a b c : with_top α) : (a + b) * c = a * c + b * c :=
-begin
-  induction c using with_top.rec_top_coe,
-  { by_cases ha : a = 0; simp [ha] },
-  { by_cases hc : c = 0, { simp [hc] },
-    simp [mul_coe hc], cases a; cases b,
-    repeat { refl <|> exact congr_arg some (add_mul _ _ _) } }
-end
-
-/-- This instance requires `canonically_ordered_comm_semiring` as it is the smallest class
-that derives from both `non_assoc_non_unital_semiring` and `canonically_ordered_add_monoid`, both
-of which are required for distributivity. -/
-instance [nontrivial α] : comm_semiring (with_top α) :=
-{ right_distrib   := distrib',
-  left_distrib    := λ a b c, by { rw [mul_comm, distrib', mul_comm b, mul_comm c], refl },
-  .. with_top.add_comm_monoid_with_one, .. with_top.comm_monoid_with_zero }
-
-instance [nontrivial α] : canonically_ordered_comm_semiring (with_top α) :=
-{ .. with_top.comm_semiring,
-  .. with_top.canonically_ordered_add_monoid,
-  .. with_top.no_zero_divisors, }
-
-/-- A version of `with_top.map` for `ring_hom`s. -/
-@[simps { fully_applied := ff }] protected def _root_.ring_hom.with_top_map
-  {R S : Type*} [canonically_ordered_comm_semiring R] [decidable_eq R] [nontrivial R]
-  [canonically_ordered_comm_semiring S] [decidable_eq S] [nontrivial S]
-  (f : R →+* S) (hf : function.injective f) :
-  with_top R →+* with_top S :=
-{ to_fun := with_top.map f,
-  .. f.to_monoid_with_zero_hom.with_top_map hf, .. f.to_add_monoid_hom.with_top_map }
-
-end with_top
-
-namespace with_bot
-
-instance [nonempty α] : nontrivial (with_bot α) := option.nontrivial
-
-variable [decidable_eq α]
-
-section has_mul
-
-variables [has_zero α] [has_mul α]
-
-instance : mul_zero_class (with_bot α) :=
-with_top.mul_zero_class
-
-lemma mul_def {a b : with_bot α} :
-  a * b = if a = 0 ∨ b = 0 then 0 else a.bind (λa, b.bind $ λb, ↑(a * b)) := rfl
-
-@[simp] lemma mul_bot {a : with_bot α} (h : a ≠ 0) : a * ⊥ = ⊥ :=
-with_top.mul_top h
-
-@[simp] lemma bot_mul {a : with_bot α} (h : a ≠ 0) : ⊥ * a = ⊥ :=
-with_top.top_mul h
-
-@[simp] lemma bot_mul_bot : (⊥ * ⊥ : with_bot α) = ⊥ :=
-with_top.top_mul_top
-
-end has_mul
-
-section mul_zero_class
-
-variables [mul_zero_class α]
-
-@[norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_bot α) = a * b :=
-decidable.by_cases (assume : a = 0, by simp [this]) $ assume ha,
-decidable.by_cases (assume : b = 0, by simp [this]) $ assume hb,
-by { simp [*, mul_def], refl }
-
-lemma mul_coe {b : α} (hb : b ≠ 0) {a : with_bot α} : a * b = a.bind (λa:α, ↑(a * b)) :=
-with_top.mul_coe hb
-
-@[simp] lemma mul_eq_bot_iff {a b : with_bot α} : a * b = ⊥ ↔ (a ≠ 0 ∧ b = ⊥) ∨ (a = ⊥ ∧ b ≠ 0) :=
-with_top.mul_eq_top_iff
-
-lemma bot_lt_mul [preorder α] {a b : with_bot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b :=
-begin
-  lift a to α using ne_bot_of_gt ha,
-  lift b to α using ne_bot_of_gt hb,
-  simp only [← coe_mul, bot_lt_coe],
-end
-
-end mul_zero_class
-
-/-- `nontrivial α` is needed here as otherwise we have `1 * ⊥ = ⊥` but also `= 0 * ⊥ = 0`. -/
-instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_bot α) :=
-with_top.mul_zero_one_class
-
-instance [mul_zero_class α] [no_zero_divisors α] : no_zero_divisors (with_bot α) :=
-with_top.no_zero_divisors
-
-instance [semigroup_with_zero α] [no_zero_divisors α] : semigroup_with_zero (with_bot α) :=
-with_top.semigroup_with_zero
-
-instance [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] : monoid_with_zero (with_bot α) :=
-with_top.monoid_with_zero
-
-instance [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
-  comm_monoid_with_zero (with_bot α) :=
-with_top.comm_monoid_with_zero
-
-instance [canonically_ordered_comm_semiring α] [nontrivial α] : comm_semiring (with_bot α) :=
-with_top.comm_semiring
-
-instance [canonically_ordered_comm_semiring α] [nontrivial α] : pos_mul_mono (with_bot α) :=
-pos_mul_mono_iff_covariant_pos.2 ⟨begin
-    rintros ⟨x, x0⟩ a b h, simp only [subtype.coe_mk],
-    lift x to α using x0.ne_bot,
-    induction a using with_bot.rec_bot_coe, { simp_rw [mul_bot x0.ne.symm, bot_le] },
-    induction b using with_bot.rec_bot_coe, { exact absurd h (bot_lt_coe a).not_le },
-    simp only [← coe_mul, coe_le_coe] at *,
-    exact mul_le_mul_left' h x,
-  end ⟩
-
-instance [canonically_ordered_comm_semiring α] [nontrivial α] : mul_pos_mono (with_bot α) :=
-pos_mul_mono_iff_mul_pos_mono.mp infer_instance
-
-end with_bot
diff --git a/src/algebra/order/ring/canonical.lean b/src/algebra/order/ring/canonical.lean
new file mode 100644
index 0000000000000..3701a2c241283
--- /dev/null
+++ b/src/algebra/order/ring/canonical.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+-/
+import algebra.order.ring.basic
+import algebra.order.sub.canonical
+
+/-!
+# Canoncially ordered rings and semirings.
+
+* `canonically_ordered_comm_semiring`
+  - `canonically_ordered_add_monoid` & multiplication & `*` respects `≤` & no zero divisors
+  - `comm_semiring` & `a ≤ b ↔ ∃ c, b = a + c` & no zero divisors
+
+## TODO
+
+We're still missing some typeclasses, like
+* `canonically_ordered_semiring`
+They have yet to come up in practice.
+-/
+
+open function
+
+set_option old_structure_cmd true
+
+universe u
+variables {α : Type u} {β : Type*}
+
+
+/-- A canonically ordered commutative semiring is an ordered, commutative semiring in which `a ≤ b`
+iff there exists `c` with `b = a + c`. This is satisfied by the natural numbers, for example, but
+not the integers or other ordered groups. -/
+@[protect_proj]
+class canonically_ordered_comm_semiring (α : Type*) extends
+  canonically_ordered_add_monoid α, comm_semiring α :=
+(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0)
+
+section strict_ordered_semiring
+variables [strict_ordered_semiring α] {a b c d : α}
+
+section has_exists_add_of_le
+variables [has_exists_add_of_le α]
+
+/-- Binary **rearrangement inequality**. -/
+lemma mul_add_mul_le_mul_add_mul (hab : a ≤ b) (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d :=
+begin
+  obtain ⟨b, rfl⟩ := exists_add_of_le hab,
+  obtain ⟨d, rfl⟩ := exists_add_of_le hcd,
+  rw [mul_add, add_right_comm, mul_add, ←add_assoc],
+  exact add_le_add_left (mul_le_mul_of_nonneg_right hab $ (le_add_iff_nonneg_right _).1 hcd) _,
+end
+
+/-- Binary **rearrangement inequality**. -/
+lemma mul_add_mul_le_mul_add_mul' (hba : b ≤ a) (hdc : d ≤ c) : a • d + b • c ≤ a • c + b • d :=
+by { rw [add_comm (a • d), add_comm (a • c)], exact mul_add_mul_le_mul_add_mul hba hdc }
+
+/-- Binary strict **rearrangement inequality**. -/
+lemma mul_add_mul_lt_mul_add_mul (hab : a < b) (hcd : c < d) : a * d + b * c < a * c + b * d :=
+begin
+  obtain ⟨b, rfl⟩ := exists_add_of_le hab.le,
+  obtain ⟨d, rfl⟩ := exists_add_of_le hcd.le,
+  rw [mul_add, add_right_comm, mul_add, ←add_assoc],
+  exact add_lt_add_left (mul_lt_mul_of_pos_right hab $ (lt_add_iff_pos_right _).1 hcd) _,
+end
+
+/-- Binary **rearrangement inequality**. -/
+lemma mul_add_mul_lt_mul_add_mul' (hba : b < a) (hdc : d < c) : a • d + b • c < a • c + b • d :=
+by { rw [add_comm (a • d), add_comm (a • c)], exact mul_add_mul_lt_mul_add_mul hba hdc }
+
+end has_exists_add_of_le
+
+end strict_ordered_semiring
+
+namespace canonically_ordered_comm_semiring
+variables [canonically_ordered_comm_semiring α] {a b : α}
+
+@[priority 100] -- see Note [lower instance priority]
+instance to_no_zero_divisors : no_zero_divisors α :=
+⟨canonically_ordered_comm_semiring.eq_zero_or_eq_zero_of_mul_eq_zero⟩
+
+@[priority 100] -- see Note [lower instance priority]
+instance to_covariant_mul_le : covariant_class α α (*) (≤) :=
+begin
+  refine ⟨λ a b c h, _⟩,
+  rcases exists_add_of_le h with ⟨c, rfl⟩,
+  rw mul_add,
+  apply self_le_add_right
+end
+
+@[priority 100] -- see Note [lower instance priority]
+instance to_ordered_comm_semiring : ordered_comm_semiring α :=
+{ zero_le_one := zero_le _,
+  mul_le_mul_of_nonneg_left := λ a b c h _, mul_le_mul_left' h _,
+  mul_le_mul_of_nonneg_right := λ a b c h _, mul_le_mul_right' h _,
+  ..‹canonically_ordered_comm_semiring α› }
+
+@[simp] lemma mul_pos : 0 < a * b ↔ (0 < a) ∧ (0 < b) :=
+by simp only [pos_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
+
+
+end canonically_ordered_comm_semiring
+
+section sub
+
+variables [canonically_ordered_comm_semiring α] {a b c : α}
+variables [has_sub α] [has_ordered_sub α]
+
+variables [is_total α (≤)]
+
+namespace add_le_cancellable
+protected lemma mul_tsub (h : add_le_cancellable (a * c)) :
+  a * (b - c) = a * b - a * c :=
+begin
+  cases total_of (≤) b c with hbc hcb,
+  { rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)] },
+  { apply h.eq_tsub_of_add_eq, rw [← mul_add, tsub_add_cancel_of_le hcb] }
+end
+
+protected lemma tsub_mul (h : add_le_cancellable (b * c)) : (a - b) * c = a * c - b * c :=
+by { simp only [mul_comm _ c] at *, exact h.mul_tsub }
+
+end add_le_cancellable
+
+variables [contravariant_class α α (+) (≤)]
+
+lemma mul_tsub (a b c : α) : a * (b - c) = a * b - a * c :=
+contravariant.add_le_cancellable.mul_tsub
+
+lemma tsub_mul (a b c : α) : (a - b) * c = a * c - b * c :=
+contravariant.add_le_cancellable.tsub_mul
+
+end sub
diff --git a/src/algebra/order/ring_lemmas.lean b/src/algebra/order/ring/lemmas.lean
similarity index 100%
rename from src/algebra/order/ring_lemmas.lean
rename to src/algebra/order/ring/lemmas.lean
diff --git a/src/algebra/order/ring/nontrivial.lean b/src/algebra/order/ring/nontrivial.lean
new file mode 100644
index 0000000000000..cb5d70b0cd9bf
--- /dev/null
+++ b/src/algebra/order/ring/nontrivial.lean
@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+-/
+import algebra.char_zero.defs
+import algebra.order.ring.basic
+
+/-!
+# Nontrivial strict ordered semirings (and hence linear ordered semirings) are characteristic zero.
+-/
+
+variables {α : Type*}
+
+section strict_ordered_semiring
+variables [strict_ordered_semiring α] [nontrivial α]
+
+/-- Note this is not an instance as `char_zero` implies `nontrivial`, and this would risk forming a
+loop. -/
+lemma strict_ordered_semiring.to_char_zero : char_zero α := ⟨nat.strict_mono_cast.injective⟩
+
+end strict_ordered_semiring
+
+section linear_ordered_semiring
+variables [linear_ordered_semiring α]
+
+@[priority 100] -- see Note [lower instance priority]
+instance linear_ordered_semiring.to_char_zero : char_zero α :=
+strict_ordered_semiring.to_char_zero
+
+end linear_ordered_semiring
diff --git a/src/algebra/order/ring/with_top.lean b/src/algebra/order/ring/with_top.lean
new file mode 100644
index 0000000000000..5483f53ec6f3f
--- /dev/null
+++ b/src/algebra/order/ring/with_top.lean
@@ -0,0 +1,272 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+-/
+import algebra.hom.ring
+import algebra.order.monoid.with_top
+import algebra.order.ring.canonical
+
+/-! # Structures involving `*` and `0` on `with_top` and `with_bot`
+
+The main results of this section are `with_top.canonically_ordered_comm_semiring` and
+`with_bot.comm_monoid_with_zero`.
+-/
+
+variables {α : Type*}
+
+namespace with_top
+
+instance [nonempty α] : nontrivial (with_top α) := option.nontrivial
+
+variable [decidable_eq α]
+
+section has_mul
+
+variables [has_zero α] [has_mul α]
+
+instance : mul_zero_class (with_top α) :=
+{ zero := 0,
+  mul := λ m n, if m = 0 ∨ n = 0 then 0 else m.bind (λa, n.bind $ λb, ↑(a * b)),
+  zero_mul := assume a, if_pos $ or.inl rfl,
+  mul_zero := assume a, if_pos $ or.inr rfl }
+
+lemma mul_def {a b : with_top α} :
+  a * b = if a = 0 ∨ b = 0 then 0 else a.bind (λa, b.bind $ λb, ↑(a * b)) := rfl
+
+@[simp] lemma mul_top {a : with_top α} (h : a ≠ 0) : a * ⊤ = ⊤ :=
+by cases a; simp [mul_def, h]; refl
+
+@[simp] lemma top_mul {a : with_top α} (h : a ≠ 0) : ⊤ * a = ⊤ :=
+by cases a; simp [mul_def, h]; refl
+
+@[simp] lemma top_mul_top : (⊤ * ⊤ : with_top α) = ⊤ :=
+top_mul top_ne_zero
+
+end has_mul
+
+section mul_zero_class
+
+variables [mul_zero_class α]
+
+@[norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_top α) = a * b :=
+decidable.by_cases (assume : a = 0, by simp [this]) $ assume ha,
+decidable.by_cases (assume : b = 0, by simp [this]) $ assume hb,
+by { simp [*, mul_def], refl }
+
+lemma mul_coe {b : α} (hb : b ≠ 0) : ∀{a : with_top α}, a * b = a.bind (λa:α, ↑(a * b))
+| none     := show (if (⊤:with_top α) = 0 ∨ (b:with_top α) = 0 then 0 else ⊤ : with_top α) = ⊤,
+    by simp [hb]
+| (some a) := show ↑a * ↑b = ↑(a * b), from coe_mul.symm
+
+@[simp] lemma mul_eq_top_iff {a b : with_top α} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
+begin
+  cases a; cases b; simp only [none_eq_top, some_eq_coe],
+  { simp [← coe_mul] },
+  { by_cases hb : b = 0; simp [hb] },
+  { by_cases ha : a = 0; simp [ha] },
+  { simp [← coe_mul] }
+end
+
+lemma mul_lt_top [preorder α] {a b : with_top α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b < ⊤ :=
+begin
+  lift a to α using ha,
+  lift b to α using hb,
+  simp only [← coe_mul, coe_lt_top]
+end
+
+@[simp] lemma untop'_zero_mul (a b : with_top α) : (a * b).untop' 0 = a.untop' 0 * b.untop' 0 :=
+begin
+  by_cases ha : a = 0, { rw [ha, zero_mul, ← coe_zero, untop'_coe, zero_mul] },
+  by_cases hb : b = 0, { rw [hb, mul_zero, ← coe_zero, untop'_coe, mul_zero] },
+  induction a using with_top.rec_top_coe, { rw [top_mul hb, untop'_top, zero_mul] },
+  induction b using with_top.rec_top_coe, { rw [mul_top ha, untop'_top, mul_zero] },
+  rw [← coe_mul, untop'_coe, untop'_coe, untop'_coe]
+end
+
+end mul_zero_class
+
+/-- `nontrivial α` is needed here as otherwise we have `1 * ⊤ = ⊤` but also `0 * ⊤ = 0`. -/
+instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_top α) :=
+{ mul := (*),
+  one := 1,
+  zero := 0,
+  one_mul := λ a, match a with
+  | ⊤       := mul_top (mt coe_eq_coe.1 one_ne_zero)
+  | (a : α) := by rw [← coe_one, ← coe_mul, one_mul]
+  end,
+  mul_one := λ a, match a with
+  | ⊤       := top_mul (mt coe_eq_coe.1 one_ne_zero)
+  | (a : α) := by rw [← coe_one, ← coe_mul, mul_one]
+  end,
+  .. with_top.mul_zero_class }
+
+/-- A version of `with_top.map` for `monoid_with_zero_hom`s. -/
+@[simps { fully_applied := ff }] protected def _root_.monoid_with_zero_hom.with_top_map
+  {R S : Type*} [mul_zero_one_class R] [decidable_eq R] [nontrivial R]
+  [mul_zero_one_class S] [decidable_eq S] [nontrivial S] (f : R →*₀ S) (hf : function.injective f) :
+  with_top R →*₀ with_top S :=
+{ to_fun := with_top.map f,
+  map_mul' := λ x y,
+    begin
+      have : ∀ z, map f z = 0 ↔ z = 0,
+        from λ z, (option.map_injective hf).eq_iff' f.to_zero_hom.with_top_map.map_zero,
+      rcases eq_or_ne x 0 with rfl|hx, { simp },
+      rcases eq_or_ne y 0 with rfl|hy, { simp },
+      induction x using with_top.rec_top_coe, { simp [hy, this] },
+      induction y using with_top.rec_top_coe,
+      { have : (f x : with_top S) ≠ 0, by simpa [hf.eq_iff' (map_zero f)] using hx,
+        simp [hx, this] },
+      simp [← coe_mul]
+    end,
+  .. f.to_zero_hom.with_top_map, .. f.to_monoid_hom.to_one_hom.with_top_map }
+
+instance [mul_zero_class α] [no_zero_divisors α] : no_zero_divisors (with_top α) :=
+⟨λ a b, by cases a; cases b; dsimp [mul_def]; split_ifs;
+  simp [*, none_eq_top, some_eq_coe, mul_eq_zero] at *⟩
+
+instance [semigroup_with_zero α] [no_zero_divisors α] : semigroup_with_zero (with_top α) :=
+{ mul := (*),
+  zero := 0,
+  mul_assoc := λ a b c, begin
+    rcases eq_or_ne a 0 with rfl|ha, { simp only [zero_mul] },
+    rcases eq_or_ne b 0 with rfl|hb, { simp only [zero_mul, mul_zero] },
+    rcases eq_or_ne c 0 with rfl|hc, { simp only [mul_zero] },
+    induction a using with_top.rec_top_coe, { simp [hb, hc] },
+    induction b using with_top.rec_top_coe, { simp [ha, hc] },
+    induction c using with_top.rec_top_coe, { simp [ha, hb] },
+    simp only [← coe_mul, mul_assoc]
+  end,
+  .. with_top.mul_zero_class }
+
+instance [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] : monoid_with_zero (with_top α) :=
+{ .. with_top.mul_zero_one_class, .. with_top.semigroup_with_zero }
+
+instance [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
+  comm_monoid_with_zero (with_top α) :=
+{ mul := (*),
+  zero := 0,
+  mul_comm := λ a b,
+    by simp only [or_comm, mul_def, option.bind_comm a b, mul_comm],
+  .. with_top.monoid_with_zero }
+
+variables [canonically_ordered_comm_semiring α]
+
+private lemma distrib' (a b c : with_top α) : (a + b) * c = a * c + b * c :=
+begin
+  induction c using with_top.rec_top_coe,
+  { by_cases ha : a = 0; simp [ha] },
+  { by_cases hc : c = 0, { simp [hc] },
+    simp [mul_coe hc], cases a; cases b,
+    repeat { refl <|> exact congr_arg some (add_mul _ _ _) } }
+end
+
+/-- This instance requires `canonically_ordered_comm_semiring` as it is the smallest class
+that derives from both `non_assoc_non_unital_semiring` and `canonically_ordered_add_monoid`, both
+of which are required for distributivity. -/
+instance [nontrivial α] : comm_semiring (with_top α) :=
+{ right_distrib   := distrib',
+  left_distrib    := λ a b c, by { rw [mul_comm, distrib', mul_comm b, mul_comm c], refl },
+  .. with_top.add_comm_monoid_with_one, .. with_top.comm_monoid_with_zero }
+
+instance [nontrivial α] : canonically_ordered_comm_semiring (with_top α) :=
+{ .. with_top.comm_semiring,
+  .. with_top.canonically_ordered_add_monoid,
+  .. with_top.no_zero_divisors, }
+
+/-- A version of `with_top.map` for `ring_hom`s. -/
+@[simps { fully_applied := ff }] protected def _root_.ring_hom.with_top_map
+  {R S : Type*} [canonically_ordered_comm_semiring R] [decidable_eq R] [nontrivial R]
+  [canonically_ordered_comm_semiring S] [decidable_eq S] [nontrivial S]
+  (f : R →+* S) (hf : function.injective f) :
+  with_top R →+* with_top S :=
+{ to_fun := with_top.map f,
+  .. f.to_monoid_with_zero_hom.with_top_map hf, .. f.to_add_monoid_hom.with_top_map }
+
+end with_top
+
+namespace with_bot
+
+instance [nonempty α] : nontrivial (with_bot α) := option.nontrivial
+
+variable [decidable_eq α]
+
+section has_mul
+
+variables [has_zero α] [has_mul α]
+
+instance : mul_zero_class (with_bot α) :=
+with_top.mul_zero_class
+
+lemma mul_def {a b : with_bot α} :
+  a * b = if a = 0 ∨ b = 0 then 0 else a.bind (λa, b.bind $ λb, ↑(a * b)) := rfl
+
+@[simp] lemma mul_bot {a : with_bot α} (h : a ≠ 0) : a * ⊥ = ⊥ :=
+with_top.mul_top h
+
+@[simp] lemma bot_mul {a : with_bot α} (h : a ≠ 0) : ⊥ * a = ⊥ :=
+with_top.top_mul h
+
+@[simp] lemma bot_mul_bot : (⊥ * ⊥ : with_bot α) = ⊥ :=
+with_top.top_mul_top
+
+end has_mul
+
+section mul_zero_class
+
+variables [mul_zero_class α]
+
+@[norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_bot α) = a * b :=
+decidable.by_cases (assume : a = 0, by simp [this]) $ assume ha,
+decidable.by_cases (assume : b = 0, by simp [this]) $ assume hb,
+by { simp [*, mul_def], refl }
+
+lemma mul_coe {b : α} (hb : b ≠ 0) {a : with_bot α} : a * b = a.bind (λa:α, ↑(a * b)) :=
+with_top.mul_coe hb
+
+@[simp] lemma mul_eq_bot_iff {a b : with_bot α} : a * b = ⊥ ↔ (a ≠ 0 ∧ b = ⊥) ∨ (a = ⊥ ∧ b ≠ 0) :=
+with_top.mul_eq_top_iff
+
+lemma bot_lt_mul [preorder α] {a b : with_bot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b :=
+begin
+  lift a to α using ne_bot_of_gt ha,
+  lift b to α using ne_bot_of_gt hb,
+  simp only [← coe_mul, bot_lt_coe],
+end
+
+end mul_zero_class
+
+/-- `nontrivial α` is needed here as otherwise we have `1 * ⊥ = ⊥` but also `= 0 * ⊥ = 0`. -/
+instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_bot α) :=
+with_top.mul_zero_one_class
+
+instance [mul_zero_class α] [no_zero_divisors α] : no_zero_divisors (with_bot α) :=
+with_top.no_zero_divisors
+
+instance [semigroup_with_zero α] [no_zero_divisors α] : semigroup_with_zero (with_bot α) :=
+with_top.semigroup_with_zero
+
+instance [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] : monoid_with_zero (with_bot α) :=
+with_top.monoid_with_zero
+
+instance [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
+  comm_monoid_with_zero (with_bot α) :=
+with_top.comm_monoid_with_zero
+
+instance [canonically_ordered_comm_semiring α] [nontrivial α] : comm_semiring (with_bot α) :=
+with_top.comm_semiring
+
+instance [canonically_ordered_comm_semiring α] [nontrivial α] : pos_mul_mono (with_bot α) :=
+pos_mul_mono_iff_covariant_pos.2 ⟨begin
+    rintros ⟨x, x0⟩ a b h, simp only [subtype.coe_mk],
+    lift x to α using x0.ne_bot,
+    induction a using with_bot.rec_bot_coe, { simp_rw [mul_bot x0.ne.symm, bot_le] },
+    induction b using with_bot.rec_bot_coe, { exact absurd h (bot_lt_coe a).not_le },
+    simp only [← coe_mul, coe_le_coe] at *,
+    exact mul_le_mul_left' h x,
+  end ⟩
+
+instance [canonically_ordered_comm_semiring α] [nontrivial α] : mul_pos_mono (with_bot α) :=
+pos_mul_mono_iff_mul_pos_mono.mp infer_instance
+
+end with_bot
diff --git a/src/algebra/order/smul.lean b/src/algebra/order/smul.lean
index 3662e67bcf030..bbf5d6f9f1934 100644
--- a/src/algebra/order/smul.lean
+++ b/src/algebra/order/smul.lean
@@ -5,6 +5,7 @@ Authors: Frédéric Dupuis
 -/
 import algebra.module.pi
 import algebra.module.prod
+import algebra.order.monoid.prod
 import algebra.order.field.basic
 import algebra.order.pi
 import data.set.pointwise.basic
diff --git a/src/algebra/order/upper_lower.lean b/src/algebra/order/upper_lower.lean
index 5461252fee576..a4db7dcc24c4e 100644
--- a/src/algebra/order/upper_lower.lean
+++ b/src/algebra/order/upper_lower.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import algebra.order.group.basic
+import data.set.pointwise.basic
 import order.upper_lower
 
 /-!
diff --git a/src/algebra/order/with_zero.lean b/src/algebra/order/with_zero.lean
index 306173382fae1..724f603462641 100644
--- a/src/algebra/order/with_zero.lean
+++ b/src/algebra/order/with_zero.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Johan Commelin, Patrick Massot
 -/
 import algebra.order.group.type_tags
+import algebra.order.group.units
 import algebra.order.monoid.with_zero
 
 /-!
diff --git a/src/algebra/ring/prod.lean b/src/algebra/ring/prod.lean
index 41946099d8546..ba6f707971621 100644
--- a/src/algebra/ring/prod.lean
+++ b/src/algebra/ring/prod.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Chris Hughes, Mario Carneiro, Yury Kudryashov
 -/
 import algebra.group.prod
+import algebra.order.group.prod
 import algebra.ring.basic
 import algebra.ring.equiv
 
diff --git a/src/algebra/tropical/basic.lean b/src/algebra/tropical/basic.lean
index 419b1fc1af7c0..7f38d50e8e516 100644
--- a/src/algebra/tropical/basic.lean
+++ b/src/algebra/tropical/basic.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
 import algebra.group_power.order
+import algebra.order.group.min_max
+import algebra.order.monoid.with_top
 import algebra.smul_with_zero
 
 /-!
diff --git a/src/analysis/convex/between.lean b/src/analysis/convex/between.lean
index 8e0d36f93d523..caacc8c276eba 100644
--- a/src/analysis/convex/between.lean
+++ b/src/analysis/convex/between.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
+import data.set.intervals.group
 import analysis.convex.segment
 import linear_algebra.affine_space.finite_dimensional
 import tactic.field_simp
diff --git a/src/category_theory/differential_object.lean b/src/category_theory/differential_object.lean
index c349aeffaa04b..96de5d3b8a33d 100644
--- a/src/category_theory/differential_object.lean
+++ b/src/category_theory/differential_object.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import data.int.basic
 import category_theory.shift
 import category_theory.concrete_category.basic
 
diff --git a/src/category_theory/essentially_small.lean b/src/category_theory/essentially_small.lean
index ac75784a0a4b7..df2db56995524 100644
--- a/src/category_theory/essentially_small.lean
+++ b/src/category_theory/essentially_small.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import logic.small
+import logic.small.basic
 import category_theory.category.ulift
 import category_theory.skeletal
 
diff --git a/src/category_theory/limits/shapes/zero_morphisms.lean b/src/category_theory/limits/shapes/zero_morphisms.lean
index 00d1e6267f0ed..c99d2118ad41f 100644
--- a/src/category_theory/limits/shapes/zero_morphisms.lean
+++ b/src/category_theory/limits/shapes/zero_morphisms.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import data.pi.algebra
 import category_theory.limits.shapes.products
 import category_theory.limits.shapes.images
 import category_theory.isomorphism_classes
diff --git a/src/category_theory/triangulated/basic.lean b/src/category_theory/triangulated/basic.lean
index 74cc8523e7cf1..7cfece83be0f9 100644
--- a/src/category_theory/triangulated/basic.lean
+++ b/src/category_theory/triangulated/basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Luke Kershaw. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Kershaw
 -/
+import data.int.basic
 import category_theory.shift
 
 /-!
diff --git a/src/combinatorics/simple_graph/regularity/energy.lean b/src/combinatorics/simple_graph/regularity/energy.lean
index 63c70714dcec0..f70869c4fcffa 100644
--- a/src/combinatorics/simple_graph/regularity/energy.lean
+++ b/src/combinatorics/simple_graph/regularity/energy.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import algebra.big_operators.order
+import algebra.module.basic
 import combinatorics.simple_graph.density
 
 /-!
diff --git a/src/data/countable/small.lean b/src/data/countable/small.lean
index 7629e4784ead6..1e56f957ebe68 100644
--- a/src/data/countable/small.lean
+++ b/src/data/countable/small.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import data.countable.basic
-import logic.small
+import logic.small.basic
 
 /-!
 # All countable types are small.
diff --git a/src/data/enat/basic.lean b/src/data/enat/basic.lean
index 57281a0c66d00..9f24442e9be3f 100644
--- a/src/data/enat/basic.lean
+++ b/src/data/enat/basic.lean
@@ -5,7 +5,9 @@ Authors: Yury Kudryashov
 -/
 import data.nat.lattice
 import data.nat.succ_pred
+import algebra.char_zero
 import algebra.order.sub.with_top
+import algebra.order.ring.with_top
 
 /-!
 # Definition and basic properties of extended natural numbers
diff --git a/src/data/fin/succ_pred.lean b/src/data/fin/succ_pred.lean
index 85b2168310baa..fc3be9dc186ba 100644
--- a/src/data/fin/succ_pred.lean
+++ b/src/data/fin/succ_pred.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Eric Rodriguez. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
+import data.fin.basic
 import order.succ_pred.basic
 
 /-!
diff --git a/src/data/fintype/small.lean b/src/data/fintype/small.lean
index 3c08b81c13615..eabfa28a0233a 100644
--- a/src/data/fintype/small.lean
+++ b/src/data/fintype/small.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import data.fintype.basic
-import logic.small
+import logic.small.basic
 
 /-!
 # All finite types are small.
diff --git a/src/data/hash_map.lean b/src/data/hash_map.lean
index 60f9ec9b3f180..60fc6db2edf09 100644
--- a/src/data/hash_map.lean
+++ b/src/data/hash_map.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 import data.array.lemmas
 import data.list.join
 import data.list.range
-import data.pnat.basic
+import data.pnat.defs
 
 /-!
 # Hash maps
diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean
index fae5806802eec..75bac92ff5fa6 100644
--- a/src/data/int/basic.lean
+++ b/src/data/int/basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
-import algebra.ring.basic
 import data.nat.basic
 
 /-!
diff --git a/src/data/int/order.lean b/src/data/int/order.lean
index a8cbe356b64cc..845d233b30994 100644
--- a/src/data/int/order.lean
+++ b/src/data/int/order.lean
@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 import data.int.basic
-import algebra.order.ring
+import algebra.order.ring.abs
+import algebra.order.ring.nontrivial
+import algebra.char_zero.defs
 
 /-!
 # Order instances on the integers
diff --git a/src/data/int/succ_pred.lean b/src/data/int/succ_pred.lean
index 0a550ca214380..81033c99a2655 100644
--- a/src/data/int/succ_pred.lean
+++ b/src/data/int/succ_pred.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import data.int.basic
+import data.int.order
 import data.nat.succ_pred
 
 /-!
diff --git a/src/data/list/lattice.lean b/src/data/list/lattice.lean
index 2264b65c121c2..e7c2b28cc3ea0 100644
--- a/src/data/list/lattice.lean
+++ b/src/data/list/lattice.lean
@@ -6,6 +6,7 @@ Scott Morrison
 -/
 import data.list.count
 import data.list.infix
+import algebra.order.monoid.min_max
 
 /-!
 # Lattice structure of lists
diff --git a/src/data/list/min_max.lean b/src/data/list/min_max.lean
index 8d9273bdce64b..1efda65f65006 100644
--- a/src/data/list/min_max.lean
+++ b/src/data/list/min_max.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Minchao Wu, Chris Hughes, Mantas Bakšys
 -/
 import data.list.basic
+import algebra.order.monoid.with_top
+
 /-!
 # Minimum and maximum of lists
 
diff --git a/src/data/list/zip.lean b/src/data/list/zip.lean
index 19ce67b061c94..77f80acfa9d92 100644
--- a/src/data/list/zip.lean
+++ b/src/data/list/zip.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kenny Lau
 -/
 import data.list.big_operators
+import algebra.order.group.min_max
 
 /-!
 # zip & unzip
diff --git a/src/data/nat/cast.lean b/src/data/nat/cast.lean
index 1e0f65a26a731..1000ad4d08a0e 100644
--- a/src/data/nat/cast.lean
+++ b/src/data/nat/cast.lean
@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.nat.order
-import algebra.order.ring
+import algebra.order.group.abs
+import algebra.group.prod
+import algebra.hom.ring
+import algebra.order.monoid.with_top
 
 /-!
 # Cast of natural numbers (additional theorems)
diff --git a/src/data/nat/order.lean b/src/data/nat/order.lean
index 67c4f7731bb65..9b3dc61b2b4ae 100644
--- a/src/data/nat/order.lean
+++ b/src/data/nat/order.lean
@@ -3,7 +3,8 @@ Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights r
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
-import algebra.order.ring
+import algebra.ring.divisibility
+import algebra.order.ring.canonical
 import algebra.order.with_zero
 import data.nat.basic
 
diff --git a/src/data/nat/pairing.lean b/src/data/nat/pairing.lean
index 0923cc48e7400..d2d9efdcd57e2 100644
--- a/src/data/nat/pairing.lean
+++ b/src/data/nat/pairing.lean
@@ -5,6 +5,8 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 import data.nat.sqrt
 import data.set.lattice
+import algebra.order.monoid.prod
+import algebra.order.group.min_max
 
 /-!
 #  Naturals pairing function
diff --git a/src/data/nat/part_enat.lean b/src/data/nat/part_enat.lean
index a615464a49d9c..305b0e17db444 100644
--- a/src/data/nat/part_enat.lean
+++ b/src/data/nat/part_enat.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
+import order.well_founded
 import algebra.hom.equiv
 import data.part
 import data.enat.basic
diff --git a/src/data/nat/succ_pred.lean b/src/data/nat/succ_pred.lean
index 47ef60b006391..f07c8d8b6bbb4 100644
--- a/src/data/nat/succ_pred.lean
+++ b/src/data/nat/succ_pred.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import data.fin.basic
 import order.succ_pred.basic
 
 /-!
diff --git a/src/data/nat/with_bot.lean b/src/data/nat/with_bot.lean
index 3e463ba9cb49a..aef96fd0f05de 100644
--- a/src/data/nat/with_bot.lean
+++ b/src/data/nat/with_bot.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import data.nat.order
-import algebra.order.group.basic
+import algebra.order.monoid.with_top
+
 /-!
 # `with_bot ℕ`
 
diff --git a/src/data/ordmap/ordset.lean b/src/data/ordmap/ordset.lean
index 6a92db28afd7f..6b23c1b79c2be 100644
--- a/src/data/ordmap/ordset.lean
+++ b/src/data/ordmap/ordset.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.ordmap.ordnode
-import algebra.order.ring
+import algebra.order.ring.basic
 import data.nat.dist
 import tactic.linarith
 
diff --git a/src/data/pi/lex.lean b/src/data/pi/lex.lean
index 927c30bba3fc6..692a93c700abc 100644
--- a/src/data/pi/lex.lean
+++ b/src/data/pi/lex.lean
@@ -5,8 +5,10 @@ Authors: Chris Hughes
 -/
 import order.well_founded
 import algebra.group.pi
+import algebra.order.group.basic
 import order.min_max
 
+
 /-!
 # Lexicographic order on Pi types
 
diff --git a/src/data/pnat/basic.lean b/src/data/pnat/basic.lean
index 0063d607c90a4..1d597d356a0a8 100644
--- a/src/data/pnat/basic.lean
+++ b/src/data/pnat/basic.lean
@@ -3,39 +3,29 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Neil Strickland
 -/
+import data.pnat.defs
 import data.nat.order
 import algebra.order.positive.ring
 
 /-!
 # The positive natural numbers
 
-This file defines the type `ℕ+` or `pnat`, the subtype of natural numbers that are positive.
+This file develops the type `ℕ+` or `pnat`, the subtype of natural numbers that are positive.
+It is defined in `data.pnat.defs`, but most of the development is deferred to here so
+that `data.pnat.defs` can have very few imports.
 -/
 
-/-- `ℕ+` is the type of positive natural numbers. It is defined as a subtype,
-  and the VM representation of `ℕ+` is the same as `ℕ` because the proof
-  is not stored. -/
-@[derive [decidable_eq, add_left_cancel_semigroup, add_right_cancel_semigroup, add_comm_semigroup,
-  linear_ordered_cancel_comm_monoid, linear_order, has_add, has_mul, has_one, distrib]]
-def pnat := {n : ℕ // 0 < n}
-notation `ℕ+` := pnat
-
-instance coe_pnat_nat : has_coe ℕ+ ℕ := ⟨subtype.val⟩
-instance : has_repr ℕ+ := ⟨λ n, repr n.1⟩
+attribute [derive [add_left_cancel_semigroup, add_right_cancel_semigroup, add_comm_semigroup,
+  linear_ordered_cancel_comm_monoid, has_add, has_mul, distrib]] pnat
 
 namespace pnat
 
-/-- Predecessor of a `ℕ+`, as a `ℕ`. -/
-def nat_pred (i : ℕ+) : ℕ := i - 1
-
 @[simp] lemma one_add_nat_pred (n : ℕ+) : 1 + n.nat_pred = n :=
 by rw [nat_pred, add_tsub_cancel_iff_le.mpr $ show 1 ≤ (n : ℕ), from n.2]
 
 @[simp] lemma nat_pred_add_one (n : ℕ+) : n.nat_pred + 1 = n :=
 (add_comm _ _).trans n.one_add_nat_pred
 
-@[simp] lemma nat_pred_eq_pred {n : ℕ} (h : 0 < n) : nat_pred (⟨n, h⟩ : ℕ+) = n.pred := rfl
-
 @[mono] lemma nat_pred_strict_mono : strict_mono nat_pred := λ m n h, nat.pred_lt_pred m.2.ne' h
 @[mono] lemma nat_pred_monotone : monotone nat_pred := nat_pred_strict_mono.monotone
 lemma nat_pred_injective : function.injective nat_pred := nat_pred_strict_mono.injective
@@ -52,15 +42,6 @@ end pnat
 
 namespace nat
 
-/-- Convert a natural number to a positive natural number. The
-  positivity assumption is inferred by `dec_trivial`. -/
-def to_pnat (n : ℕ) (h : 0 < n . tactic.exact_dec_trivial) : ℕ+ := ⟨n, h⟩
-
-/-- Write a successor as an element of `ℕ+`. -/
-def succ_pnat (n : ℕ) : ℕ+ := ⟨succ n, succ_pos n⟩
-
-@[simp] theorem succ_pnat_coe (n : ℕ) : (succ_pnat n : ℕ) = succ n := rfl
-
 @[mono] theorem succ_pnat_strict_mono : strict_mono succ_pnat := λ m n, nat.succ_lt_succ
 
 @[mono] theorem succ_pnat_mono : monotone succ_pnat := succ_pnat_strict_mono.monotone
@@ -76,20 +57,6 @@ theorem succ_pnat_injective : function.injective succ_pnat := succ_pnat_strict_m
 @[simp] theorem succ_pnat_inj {n m : ℕ} : succ_pnat n = succ_pnat m ↔ n = m :=
 succ_pnat_injective.eq_iff
 
-@[simp] theorem nat_pred_succ_pnat (n : ℕ) : n.succ_pnat.nat_pred = n := rfl
-
-@[simp] theorem _root_.pnat.succ_pnat_nat_pred (n : ℕ+) : n.nat_pred.succ_pnat = n :=
-subtype.eq $ succ_pred_eq_of_pos n.2
-
-/-- Convert a natural number to a pnat. `n+1` is mapped to itself,
-  and `0` becomes `1`. -/
-def to_pnat' (n : ℕ) : ℕ+ := succ_pnat (pred n)
-
-@[simp] theorem to_pnat'_coe : ∀ (n : ℕ),
- ((to_pnat' n) : ℕ) = ite (0 < n) n 1
-| 0 := rfl
-| (m + 1) := by {rw [if_pos (succ_pos m)], refl}
-
 end nat
 
 namespace pnat
@@ -102,26 +69,8 @@ open nat
  subtraction, division and powers.
 -/
 
-@[simp] lemma mk_le_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
-  (⟨n, hn⟩ : ℕ+) ≤ ⟨k, hk⟩ ↔ n ≤ k := iff.rfl
-
-@[simp] lemma mk_lt_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
-  (⟨n, hn⟩ : ℕ+) < ⟨k, hk⟩ ↔ n < k := iff.rfl
-
-@[simp, norm_cast] lemma coe_le_coe (n k : ℕ+) : (n : ℕ) ≤ k ↔ n ≤ k := iff.rfl
-
-@[simp, norm_cast] lemma coe_lt_coe (n k : ℕ+) : (n : ℕ) < k ↔ n < k := iff.rfl
-
-@[simp] theorem pos (n : ℕ+) : 0 < (n : ℕ) := n.2
-
-theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n := subtype.eq
-
 @[simp, norm_cast] lemma coe_inj {m n : ℕ+} : (m : ℕ) = n ↔ m = n := set_coe.ext_iff
 
-lemma coe_injective : function.injective (coe : ℕ+ → ℕ) := subtype.coe_injective
-
-@[simp] theorem mk_coe (n h) : ((⟨n, h⟩ : ℕ+) : ℕ) = n := rfl
-
 @[simp, norm_cast] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl
 
 /-- `pnat.coe` promoted to an `add_hom`, that is, a morphism which preserves addition. -/
@@ -149,34 +98,19 @@ instance : contravariant_class ℕ+ ℕ+ (+) (<) := positive.contravariant_class
 @[simp] lemma _root_.order_iso.pnat_iso_nat_symm_apply :
   ⇑order_iso.pnat_iso_nat.symm = nat.succ_pnat := rfl
 
-@[simp] theorem ne_zero (n : ℕ+) : (n : ℕ) ≠ 0 := n.2.ne'
-
-instance _root_.ne_zero.pnat {a : ℕ+} : _root_.ne_zero (a : ℕ) := ⟨a.ne_zero⟩
-
-theorem to_pnat'_coe {n : ℕ} : 0 < n → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos
-
-@[simp] theorem coe_to_pnat' (n : ℕ+) : (n : ℕ).to_pnat' = n := eq (to_pnat'_coe n.pos)
-
 theorem lt_add_one_iff : ∀ {a b : ℕ+}, a < b + 1 ↔ a ≤ b :=
 λ a b, nat.lt_add_one_iff
 
 theorem add_one_le_iff : ∀ {a b : ℕ+}, a + 1 ≤ b ↔ a < b :=
 λ a b, nat.add_one_le_iff
 
-@[simp] lemma one_le (n : ℕ+) : (1 : ℕ+) ≤ n := n.2
-
-@[simp] lemma not_lt_one (n : ℕ+) : ¬ n < 1 := not_lt_of_le n.one_le
-
 instance : order_bot ℕ+ :=
 { bot := 1,
   bot_le := λ a, a.property }
 
 @[simp] lemma bot_eq_one : (⊥ : ℕ+) = 1 := rfl
 
-instance : inhabited ℕ+ := ⟨1⟩
-
 -- Some lemmas that rewrite `pnat.mk n h`, for `n` an explicit numeral, into explicit numerals.
-@[simp] lemma mk_one {h} : (⟨1, h⟩ : ℕ+) = (1 : ℕ+) := rfl
 @[simp] lemma mk_bit0 (n) {h} : (⟨bit0 n, h⟩ : ℕ+) = (bit0 ⟨n, pos_of_bit0_pos h⟩ : ℕ+) := rfl
 @[simp] lemma mk_bit1 (n) {h} {k} : (⟨bit1 n, h⟩ : ℕ+) = (bit1 ⟨n, k⟩ : ℕ+) := rfl
 
@@ -196,7 +130,6 @@ iff.rfl
 @[simp] lemma bit1_le_bit1 (n m : ℕ+) : (bit1 n) ≤ (bit1 m) ↔ (bit1 (n : ℕ)) ≤ (bit1 (m : ℕ)) :=
 iff.rfl
 
-@[simp, norm_cast] theorem one_coe : ((1 : ℕ+) : ℕ) = 1 := rfl
 @[simp, norm_cast] theorem mul_coe (m n : ℕ+) : ((m * n : ℕ+) : ℕ) = m * n := rfl
 
 /-- `pnat.coe` promoted to a `monoid_hom`. -/
@@ -207,9 +140,6 @@ def coe_monoid_hom : ℕ+ →* ℕ :=
 
 @[simp] lemma coe_coe_monoid_hom : (coe_monoid_hom : ℕ+ → ℕ) = coe := rfl
 
-@[simp, norm_cast] lemma coe_eq_one_iff {m : ℕ+} : (m : ℕ) = 1 ↔ m = 1 :=
-subtype.coe_injective.eq_iff' one_coe
-
 @[simp] lemma le_one_iff {n : ℕ+} : n ≤ 1 ↔ n = 1 := le_bot_iff
 
 lemma lt_add_left (n m : ℕ+) : n < m + n := lt_add_of_pos_left _ m.2
@@ -239,13 +169,6 @@ theorem add_sub_of_lt {a b : ℕ+} : a < b → a + (b - a) = b :=
  λ h, eq $ by { rw [add_coe, sub_coe, if_pos h],
                 exact add_tsub_cancel_of_le h.le }
 
-instance : has_well_founded ℕ+ := ⟨(<), measure_wf coe⟩
-
-/-- Strong induction on `ℕ+`. -/
-def strong_induction_on {p : ℕ+ → Sort*} : ∀ (n : ℕ+) (h : ∀ k, (∀ m, m < k → p m) → p k), p n
-| n := λ IH, IH _ (λ a h, strong_induction_on a IH)
-using_well_founded { dec_tac := `[assumption] }
-
 /-- If `n : ℕ+` is different from `1`, then it is the successor of some `k : ℕ+`. -/
 lemma exists_eq_succ_of_ne_one : ∀ {n : ℕ+} (h1 : n ≠ 1), ∃ (k : ℕ+), n = k + 1
 | ⟨1, _⟩ h1 := false.elim $ h1 rfl
@@ -283,17 +206,6 @@ end
   @pnat.rec_on (n + 1) p p1 hp = hp n (@pnat.rec_on n p p1 hp) :=
 by { cases n with n h, cases n; [exact absurd h dec_trivial, refl] }
 
-/-- We define `m % k` and `m / k` in the same way as for `ℕ`
-  except that when `m = n * k` we take `m % k = k` and
-  `m / k = n - 1`.  This ensures that `m % k` is always positive
-  and `m = (m % k) + k * (m / k)` in all cases.  Later we
-  define a function `div_exact` which gives the usual `m / k`
-  in the case where `k` divides `m`.
--/
-def mod_div_aux : ℕ+ → ℕ → ℕ → ℕ+ × ℕ
-| k 0 q := ⟨k, q.pred⟩
-| k (r + 1) q := ⟨⟨r + 1, nat.succ_pos r⟩, q⟩
-
 lemma mod_div_aux_spec : ∀ (k : ℕ+) (r q : ℕ) (h : ¬ (r = 0 ∧ q = 0)),
  (((mod_div_aux k r q).1 : ℕ) + k * (mod_div_aux k r q).2 = (r + k * q))
 | k 0 0 h := (h ⟨rfl, rfl⟩).elim
@@ -302,27 +214,6 @@ lemma mod_div_aux_spec : ∀ (k : ℕ+) (r q : ℕ) (h : ¬ (r = 0 ∧ q = 0)),
   rw [nat.pred_succ, nat.mul_succ, zero_add, add_comm]}
 | k (r + 1) q h := rfl
 
-/-- `mod_div m k = (m % k, m / k)`.
-  We define `m % k` and `m / k` in the same way as for `ℕ`
-  except that when `m = n * k` we take `m % k = k` and
-  `m / k = n - 1`.  This ensures that `m % k` is always positive
-  and `m = (m % k) + k * (m / k)` in all cases.  Later we
-  define a function `div_exact` which gives the usual `m / k`
-  in the case where `k` divides `m`.
--/
-def mod_div (m k : ℕ+) : ℕ+ × ℕ := mod_div_aux k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ))
-
-/-- We define `m % k` in the same way as for `ℕ`
-  except that when `m = n * k` we take `m % k = k` This ensures that `m % k` is always positive.
--/
-def mod (m k : ℕ+) : ℕ+ := (mod_div m k).1
-
-/-- We define `m / k` in the same way as for `ℕ` except that when `m = n * k` we take
-  `m / k = n - 1`. This ensures that `m = (m % k) + k * (m / k)` in all cases. Later we
-  define a function `div_exact` which gives the usual `m / k` in the case where `k` divides `m`.
--/
-def div (m k : ℕ+) : ℕ  := (mod_div m k).2
-
 theorem mod_add_div (m k : ℕ+) : ((mod m k) + k * (div m k) : ℕ) = m :=
 begin
   let h₀ := nat.mod_add_div (m : ℕ) (k : ℕ),
@@ -342,24 +233,6 @@ by { rw mul_comm, exact mod_add_div _ _ }
 lemma div_add_mod' (m k : ℕ+) : ((div m k) * k + mod m k : ℕ) = m :=
 by { rw mul_comm, exact div_add_mod _ _ }
 
-theorem mod_coe (m k : ℕ+) :
- ((mod m k) : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) (k : ℕ) ((m : ℕ) % (k : ℕ)) :=
-begin
-  dsimp [mod, mod_div],
-  cases (m : ℕ) % (k : ℕ),
-  { rw [if_pos rfl], refl },
-  { rw [if_neg n.succ_ne_zero], refl }
-end
-
-theorem div_coe (m k : ℕ+) :
- ((div m k) : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) ((m : ℕ) / (k : ℕ)).pred ((m : ℕ) / (k : ℕ)) :=
-begin
-  dsimp [div, mod_div],
-  cases (m : ℕ) % (k : ℕ),
-  { rw [if_pos rfl], refl },
-  { rw [if_neg n.succ_ne_zero], refl }
-end
-
 theorem mod_le (m k : ℕ+) : mod m k ≤ m ∧ mod m k ≤ k :=
 begin
   change ((mod m k) : ℕ) ≤ (m : ℕ) ∧ ((mod m k) : ℕ) ≤ (k : ℕ),
@@ -396,10 +269,6 @@ end
 lemma le_of_dvd {m n : ℕ+} : m ∣ n → m ≤ n :=
 by { rw dvd_iff', intro h, rw ← h, apply (mod_le n m).left }
 
-/-- If `h : k | m`, then `k * (div_exact m k) = m`. Note that this is not equal to `m / k`. -/
-def div_exact (m k : ℕ+) : ℕ+ :=
- ⟨(div m k).succ, nat.succ_pos _⟩
-
 theorem mul_div_exact {m k : ℕ+} (h : k ∣ m) : k * (div_exact m k) = m :=
 begin
  apply eq, rw [mul_coe],
@@ -422,15 +291,3 @@ begin
 end
 
 end pnat
-
-section can_lift
-
-instance nat.can_lift_pnat : can_lift ℕ ℕ+ coe ((<) 0) :=
-⟨λ n hn, ⟨nat.to_pnat' n, pnat.to_pnat'_coe hn⟩⟩
-
-instance int.can_lift_pnat : can_lift ℤ ℕ+ coe ((<) 0) :=
-⟨λ n hn, ⟨nat.to_pnat' (int.nat_abs n),
-  by rw [coe_coe, nat.to_pnat'_coe, if_pos (int.nat_abs_pos_of_ne_zero hn.ne'),
-    int.nat_abs_of_nonneg hn.le]⟩⟩
-
-end can_lift
diff --git a/src/data/pnat/defs.lean b/src/data/pnat/defs.lean
new file mode 100644
index 0000000000000..9675b338eed1a
--- /dev/null
+++ b/src/data/pnat/defs.lean
@@ -0,0 +1,187 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Neil Strickland
+-/
+import order.basic
+import algebra.ne_zero
+
+/-!
+# The positive natural numbers
+
+This file contains the definitions, and basic results.
+Most algebraic facts are deferred to `data.pnat.basic`, as they need more imports.
+-/
+
+/-- `ℕ+` is the type of positive natural numbers. It is defined as a subtype,
+  and the VM representation of `ℕ+` is the same as `ℕ` because the proof
+  is not stored. -/
+@[derive [decidable_eq, linear_order]]
+def pnat := {n : ℕ // 0 < n}
+notation `ℕ+` := pnat
+
+instance : has_one ℕ+ := ⟨⟨1, nat.zero_lt_one⟩⟩
+
+instance coe_pnat_nat : has_coe ℕ+ ℕ := ⟨subtype.val⟩
+instance : has_repr ℕ+ := ⟨λ n, repr n.1⟩
+
+namespace pnat
+
+@[simp] theorem mk_coe (n h) : ((⟨n, h⟩ : ℕ+) : ℕ) = n := rfl
+
+/-- Predecessor of a `ℕ+`, as a `ℕ`. -/
+def nat_pred (i : ℕ+) : ℕ := i - 1
+
+@[simp] lemma nat_pred_eq_pred {n : ℕ} (h : 0 < n) : nat_pred (⟨n, h⟩ : ℕ+) = n.pred := rfl
+
+end pnat
+
+namespace nat
+
+/-- Convert a natural number to a positive natural number. The
+  positivity assumption is inferred by `dec_trivial`. -/
+def to_pnat (n : ℕ) (h : 0 < n . tactic.exact_dec_trivial) : ℕ+ := ⟨n, h⟩
+
+/-- Write a successor as an element of `ℕ+`. -/
+def succ_pnat (n : ℕ) : ℕ+ := ⟨succ n, succ_pos n⟩
+
+@[simp] theorem succ_pnat_coe (n : ℕ) : (succ_pnat n : ℕ) = succ n := rfl
+
+@[simp] theorem nat_pred_succ_pnat (n : ℕ) : n.succ_pnat.nat_pred = n := rfl
+
+@[simp] theorem _root_.pnat.succ_pnat_nat_pred (n : ℕ+) : n.nat_pred.succ_pnat = n :=
+subtype.eq $ succ_pred_eq_of_pos n.2
+
+/-- Convert a natural number to a pnat. `n+1` is mapped to itself,
+  and `0` becomes `1`. -/
+def to_pnat' (n : ℕ) : ℕ+ := succ_pnat (pred n)
+
+@[simp] theorem to_pnat'_coe : ∀ (n : ℕ),
+ ((to_pnat' n) : ℕ) = ite (0 < n) n 1
+| 0 := rfl
+| (m + 1) := by {rw [if_pos (succ_pos m)], refl}
+
+end nat
+
+namespace pnat
+
+open nat
+
+/-- We now define a long list of structures on ℕ+ induced by
+ similar structures on ℕ. Most of these behave in a completely
+ obvious way, but there are a few things to be said about
+ subtraction, division and powers.
+-/
+
+@[simp] lemma mk_le_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
+  (⟨n, hn⟩ : ℕ+) ≤ ⟨k, hk⟩ ↔ n ≤ k := iff.rfl
+
+@[simp] lemma mk_lt_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
+  (⟨n, hn⟩ : ℕ+) < ⟨k, hk⟩ ↔ n < k := iff.rfl
+
+@[simp, norm_cast] lemma coe_le_coe (n k : ℕ+) : (n : ℕ) ≤ k ↔ n ≤ k := iff.rfl
+
+@[simp, norm_cast] lemma coe_lt_coe (n k : ℕ+) : (n : ℕ) < k ↔ n < k := iff.rfl
+
+@[simp] theorem pos (n : ℕ+) : 0 < (n : ℕ) := n.2
+
+theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n := subtype.eq
+
+lemma coe_injective : function.injective (coe : ℕ+ → ℕ) := subtype.coe_injective
+
+@[simp] theorem ne_zero (n : ℕ+) : (n : ℕ) ≠ 0 := n.2.ne'
+
+instance _root_.ne_zero.pnat {a : ℕ+} : _root_.ne_zero (a : ℕ) := ⟨a.ne_zero⟩
+
+theorem to_pnat'_coe {n : ℕ} : 0 < n → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos
+
+@[simp] theorem coe_to_pnat' (n : ℕ+) : (n : ℕ).to_pnat' = n := eq (to_pnat'_coe n.pos)
+
+@[simp] lemma one_le (n : ℕ+) : (1 : ℕ+) ≤ n := n.2
+
+@[simp] lemma not_lt_one (n : ℕ+) : ¬ n < 1 := not_lt_of_le n.one_le
+
+instance : inhabited ℕ+ := ⟨1⟩
+
+-- Some lemmas that rewrite `pnat.mk n h`, for `n` an explicit numeral, into explicit numerals.
+@[simp] lemma mk_one {h} : (⟨1, h⟩ : ℕ+) = (1 : ℕ+) := rfl
+
+@[norm_cast] theorem one_coe : ((1 : ℕ+) : ℕ) = 1 := rfl
+
+@[simp, norm_cast] lemma coe_eq_one_iff {m : ℕ+} : (m : ℕ) = 1 ↔ m = 1 :=
+subtype.coe_injective.eq_iff' one_coe
+
+instance : has_well_founded ℕ+ := ⟨(<), measure_wf coe⟩
+
+/-- Strong induction on `ℕ+`. -/
+def strong_induction_on {p : ℕ+ → Sort*} : ∀ (n : ℕ+) (h : ∀ k, (∀ m, m < k → p m) → p k), p n
+| n := λ IH, IH _ (λ a h, strong_induction_on a IH)
+using_well_founded { dec_tac := `[assumption] }
+
+/-- We define `m % k` and `m / k` in the same way as for `ℕ`
+  except that when `m = n * k` we take `m % k = k` and
+  `m / k = n - 1`.  This ensures that `m % k` is always positive
+  and `m = (m % k) + k * (m / k)` in all cases.  Later we
+  define a function `div_exact` which gives the usual `m / k`
+  in the case where `k` divides `m`.
+-/
+def mod_div_aux : ℕ+ → ℕ → ℕ → ℕ+ × ℕ
+| k 0 q := ⟨k, q.pred⟩
+| k (r + 1) q := ⟨⟨r + 1, nat.succ_pos r⟩, q⟩
+
+/-- `mod_div m k = (m % k, m / k)`.
+  We define `m % k` and `m / k` in the same way as for `ℕ`
+  except that when `m = n * k` we take `m % k = k` and
+  `m / k = n - 1`.  This ensures that `m % k` is always positive
+  and `m = (m % k) + k * (m / k)` in all cases.  Later we
+  define a function `div_exact` which gives the usual `m / k`
+  in the case where `k` divides `m`.
+-/
+def mod_div (m k : ℕ+) : ℕ+ × ℕ := mod_div_aux k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ))
+
+/-- We define `m % k` in the same way as for `ℕ`
+  except that when `m = n * k` we take `m % k = k` This ensures that `m % k` is always positive.
+-/
+def mod (m k : ℕ+) : ℕ+ := (mod_div m k).1
+
+/-- We define `m / k` in the same way as for `ℕ` except that when `m = n * k` we take
+  `m / k = n - 1`. This ensures that `m = (m % k) + k * (m / k)` in all cases. Later we
+  define a function `div_exact` which gives the usual `m / k` in the case where `k` divides `m`.
+-/
+def div (m k : ℕ+) : ℕ  := (mod_div m k).2
+
+theorem mod_coe (m k : ℕ+) :
+ ((mod m k) : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) (k : ℕ) ((m : ℕ) % (k : ℕ)) :=
+begin
+  dsimp [mod, mod_div],
+  cases (m : ℕ) % (k : ℕ),
+  { rw [if_pos rfl], refl },
+  { rw [if_neg n.succ_ne_zero], refl }
+end
+
+theorem div_coe (m k : ℕ+) :
+ ((div m k) : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) ((m : ℕ) / (k : ℕ)).pred ((m : ℕ) / (k : ℕ)) :=
+begin
+  dsimp [div, mod_div],
+  cases (m : ℕ) % (k : ℕ),
+  { rw [if_pos rfl], refl },
+  { rw [if_neg n.succ_ne_zero], refl }
+end
+
+/-- If `h : k | m`, then `k * (div_exact m k) = m`. Note that this is not equal to `m / k`. -/
+def div_exact (m k : ℕ+) : ℕ+ :=
+ ⟨(div m k).succ, nat.succ_pos _⟩
+
+end pnat
+
+section can_lift
+
+instance nat.can_lift_pnat : can_lift ℕ ℕ+ coe ((<) 0) :=
+⟨λ n hn, ⟨nat.to_pnat' n, pnat.to_pnat'_coe hn⟩⟩
+
+instance int.can_lift_pnat : can_lift ℤ ℕ+ coe ((<) 0) :=
+⟨λ n hn, ⟨nat.to_pnat' (int.nat_abs n),
+  by rw [coe_coe, nat.to_pnat'_coe, if_pos (int.nat_abs_pos_of_ne_zero hn.ne'),
+    int.nat_abs_of_nonneg hn.le]⟩⟩
+
+end can_lift
diff --git a/src/data/pnat/interval.lean b/src/data/pnat/interval.lean
index 937de50f0455c..fa6731fc6f2a6 100644
--- a/src/data/pnat/interval.lean
+++ b/src/data/pnat/interval.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import data.nat.interval
-import data.pnat.basic
+import data.pnat.defs
 
 /-!
 # Finite intervals of positive naturals
diff --git a/src/data/rat/defs.lean b/src/data/rat/defs.lean
index 1afd1df41adc8..df6c791acf2c8 100644
--- a/src/data/rat/defs.lean
+++ b/src/data/rat/defs.lean
@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import data.int.cast
 import data.int.div
 import data.nat.gcd.basic
-import data.pnat.basic
+import data.pnat.defs
 import tactic.nth_rewrite
 
 /-!
diff --git a/src/data/rat/order.lean b/src/data/rat/order.lean
index 506112491ee7f..8b0350a793762 100644
--- a/src/data/rat/order.lean
+++ b/src/data/rat/order.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
-import algebra.order.field.basic
+import algebra.order.field.defs
 import data.rat.basic
 
 /-!
diff --git a/src/data/real/cardinality.lean b/src/data/real/cardinality.lean
index bc8e478aee486..58db59e8ab65a 100644
--- a/src/data/real/cardinality.lean
+++ b/src/data/real/cardinality.lean
@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import analysis.specific_limits.basic
 import data.rat.denumerable
-import data.set.intervals.image_preimage
+import data.set.pointwise.interval
 import set_theory.cardinal.continuum
 
 /-!
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index f6c8be026ef35..4f4a9ec77872f 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -2104,6 +2104,9 @@ by rw ← image_univ; exact image_subset _ (subset_univ _)
 theorem mem_range_of_mem_image (f : α → β) (s) {x : β} (h : x ∈ f '' s) : x ∈ range f :=
 image_subset_range f s h
 
+lemma nat.mem_range_succ (i : ℕ) : i ∈ range nat.succ ↔ 0 < i :=
+⟨by { rintros ⟨n, rfl⟩, exact nat.succ_pos n, }, λ h, ⟨_, nat.succ_pred_eq_of_pos h⟩⟩
+
 lemma nonempty.preimage' {s : set β} (hs : s.nonempty) {f : α → β} (hf : s ⊆ set.range f) :
   (f ⁻¹' s).nonempty :=
 let ⟨y, hy⟩ := hs, ⟨x, hx⟩ := hf hy in ⟨x, set.mem_preimage.2 $ hx.symm ▸ hy⟩
diff --git a/src/data/set/intervals/basic.lean b/src/data/set/intervals/basic.lean
index d0af8c043e6c5..6214d1a123697 100644
--- a/src/data/set/intervals/basic.lean
+++ b/src/data/set/intervals/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy Degenne
 -/
-import algebra.order.group.basic
+import order.min_max
 import order.rel_iso
 
 /-!
@@ -1309,162 +1309,8 @@ by simp
 
 end prod
 
-/-! ### Lemmas about membership of arithmetic operations -/
-
-section ordered_comm_group
-
-variables [ordered_comm_group α] {a b c d : α}
-
-/-! `inv_mem_Ixx_iff`, `sub_mem_Ixx_iff` -/
-@[to_additive] lemma inv_mem_Icc_iff : a⁻¹ ∈ set.Icc c d ↔ a ∈ set.Icc (d⁻¹) (c⁻¹) :=
-(and_comm _ _).trans $ and_congr inv_le' le_inv'
-@[to_additive] lemma inv_mem_Ico_iff : a⁻¹ ∈ set.Ico c d ↔ a ∈ set.Ioc (d⁻¹) (c⁻¹) :=
-(and_comm _ _).trans $ and_congr inv_lt' le_inv'
-@[to_additive] lemma inv_mem_Ioc_iff : a⁻¹ ∈ set.Ioc c d ↔ a ∈ set.Ico (d⁻¹) (c⁻¹) :=
-(and_comm _ _).trans $ and_congr inv_le' lt_inv'
-@[to_additive] lemma inv_mem_Ioo_iff : a⁻¹ ∈ set.Ioo c d ↔ a ∈ set.Ioo (d⁻¹) (c⁻¹) :=
-(and_comm _ _).trans $ and_congr inv_lt' lt_inv'
-
-end ordered_comm_group
-
-section ordered_add_comm_group
-
-variables [ordered_add_comm_group α] {a b c d : α}
-
-/-! `add_mem_Ixx_iff_left` -/
-lemma add_mem_Icc_iff_left : a + b ∈ set.Icc c d ↔ a ∈ set.Icc (c - b) (d - b) :=
-(and_congr sub_le_iff_le_add le_sub_iff_add_le).symm
-lemma add_mem_Ico_iff_left : a + b ∈ set.Ico c d ↔ a ∈ set.Ico (c - b) (d - b) :=
-(and_congr sub_le_iff_le_add lt_sub_iff_add_lt).symm
-lemma add_mem_Ioc_iff_left : a + b ∈ set.Ioc c d ↔ a ∈ set.Ioc (c - b) (d - b) :=
-(and_congr sub_lt_iff_lt_add le_sub_iff_add_le).symm
-lemma add_mem_Ioo_iff_left : a + b ∈ set.Ioo c d ↔ a ∈ set.Ioo (c - b) (d - b) :=
-(and_congr sub_lt_iff_lt_add lt_sub_iff_add_lt).symm
-
-/-! `add_mem_Ixx_iff_right` -/
-lemma add_mem_Icc_iff_right : a + b ∈ set.Icc c d ↔ b ∈ set.Icc (c - a) (d - a) :=
-(and_congr sub_le_iff_le_add' le_sub_iff_add_le').symm
-lemma add_mem_Ico_iff_right : a + b ∈ set.Ico c d ↔ b ∈ set.Ico (c - a) (d - a) :=
-(and_congr sub_le_iff_le_add' lt_sub_iff_add_lt').symm
-lemma add_mem_Ioc_iff_right : a + b ∈ set.Ioc c d ↔ b ∈ set.Ioc (c - a) (d - a) :=
-(and_congr sub_lt_iff_lt_add' le_sub_iff_add_le').symm
-lemma add_mem_Ioo_iff_right : a + b ∈ set.Ioo c d ↔ b ∈ set.Ioo (c - a) (d - a) :=
-(and_congr sub_lt_iff_lt_add' lt_sub_iff_add_lt').symm
-
-/-! `sub_mem_Ixx_iff_left` -/
-lemma sub_mem_Icc_iff_left : a - b ∈ set.Icc c d ↔ a ∈ set.Icc (c + b) (d + b) :=
-and_congr le_sub_iff_add_le sub_le_iff_le_add
-lemma sub_mem_Ico_iff_left : a - b ∈ set.Ico c d ↔ a ∈ set.Ico (c + b) (d + b) :=
-and_congr le_sub_iff_add_le sub_lt_iff_lt_add
-lemma sub_mem_Ioc_iff_left : a - b ∈ set.Ioc c d ↔ a ∈ set.Ioc (c + b) (d + b) :=
-and_congr lt_sub_iff_add_lt sub_le_iff_le_add
-lemma sub_mem_Ioo_iff_left : a - b ∈ set.Ioo c d ↔ a ∈ set.Ioo (c + b) (d + b) :=
-and_congr lt_sub_iff_add_lt sub_lt_iff_lt_add
-
-/-! `sub_mem_Ixx_iff_right` -/
-lemma sub_mem_Icc_iff_right : a - b ∈ set.Icc c d ↔ b ∈ set.Icc (a - d) (a - c) :=
-(and_comm _ _).trans $ and_congr sub_le_comm le_sub_comm
-lemma sub_mem_Ico_iff_right : a - b ∈ set.Ico c d ↔ b ∈ set.Ioc (a - d) (a - c) :=
-(and_comm _ _).trans $ and_congr sub_lt_comm le_sub_comm
-lemma sub_mem_Ioc_iff_right : a - b ∈ set.Ioc c d ↔ b ∈ set.Ico (a - d) (a - c) :=
-(and_comm _ _).trans $ and_congr sub_le_comm lt_sub_comm
-lemma sub_mem_Ioo_iff_right : a - b ∈ set.Ioo c d ↔ b ∈ set.Ioo (a - d) (a - c) :=
-(and_comm _ _).trans $ and_congr sub_lt_comm lt_sub_comm
-
--- I think that symmetric intervals deserve attention and API: they arise all the time,
--- for instance when considering metric balls in `ℝ`.
-lemma mem_Icc_iff_abs_le {R : Type*} [linear_ordered_add_comm_group R] {x y z : R} :
-  |x - y| ≤ z ↔ y ∈ Icc (x - z) (x + z) :=
-abs_le.trans $ (and_comm _ _).trans $ and_congr sub_le_comm neg_le_sub_iff_le_add
-
-end ordered_add_comm_group
-
-section linear_ordered_add_comm_group
-
-variables [linear_ordered_add_comm_group α]
-
-/-- If we remove a smaller interval from a larger, the result is nonempty -/
-lemma nonempty_Ico_sdiff {x dx y dy : α} (h : dy < dx) (hx : 0 < dx) :
-  nonempty ↥(Ico x (x + dx) \ Ico y (y + dy)) :=
-begin
-  cases lt_or_le x y with h' h',
-  { use x, simp [*, not_le.2 h'] },
-  { use max x (x + dy), simp [*, le_refl] }
-end
-
-end linear_ordered_add_comm_group
-
 end set
 
-open set
-
-namespace order_iso
-
-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]
-
-@[simp] lemma image_Iic (e : α ≃o β) (a : α) : e '' (Iic a) = Iic (e a) :=
-by rw [e.image_eq_preimage, e.symm.preimage_Iic, e.symm_symm]
-
-@[simp] lemma image_Ici (e : α ≃o β) (a : α) : e '' (Ici a) = Ici (e a) :=
-e.dual.image_Iic a
-
-@[simp] lemma image_Iio (e : α ≃o β) (a : α) : e '' (Iio a) = Iio (e a) :=
-by rw [e.image_eq_preimage, e.symm.preimage_Iio, e.symm_symm]
-
-@[simp] lemma image_Ioi (e : α ≃o β) (a : α) : e '' (Ioi a) = Ioi (e a) :=
-e.dual.image_Iio a
-
-@[simp] lemma image_Ioo (e : α ≃o β) (a b : α) : e '' (Ioo a b) = Ioo (e a) (e b) :=
-by rw [e.image_eq_preimage, e.symm.preimage_Ioo, e.symm_symm]
-
-@[simp] lemma image_Ioc (e : α ≃o β) (a b : α) : e '' (Ioc a b) = Ioc (e a) (e b) :=
-by rw [e.image_eq_preimage, e.symm.preimage_Ioc, e.symm_symm]
-
-@[simp] lemma image_Ico (e : α ≃o β) (a b : α) : e '' (Ico a b) = Ico (e a) (e b) :=
-by rw [e.image_eq_preimage, e.symm.preimage_Ico, e.symm_symm]
-
-@[simp] lemma image_Icc (e : α ≃o β) (a b : α) : e '' (Icc a b) = Icc (e a) (e b) :=
-by rw [e.image_eq_preimage, e.symm.preimage_Icc, e.symm_symm]
-
-end preorder
-
-/-- Order isomorphism between `Iic (⊤ : α)` and `α` when `α` has a top element -/
-def Iic_top [preorder α] [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 [preorder α] [order_bot α] : set.Ici (⊥ : α) ≃o α :=
-{ map_rel_iff' := λ x y, by refl,
-  .. (@equiv.subtype_univ_equiv α (set.Ici (⊥ : α)) (λ x, bot_le)) }
-
-end order_iso
-
 /-! ### Lemmas about intervals in dense orders -/
 
 section dense
diff --git a/src/data/set/intervals/group.lean b/src/data/set/intervals/group.lean
new file mode 100644
index 0000000000000..eb430b8c338aa
--- /dev/null
+++ b/src/data/set/intervals/group.lean
@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy Degenne
+-/
+import data.set.intervals.basic
+import algebra.order.group.abs
+
+/-! ### Lemmas about arithmetic operations and intervals. -/
+
+variables {α : Type*}
+
+namespace set
+
+section ordered_comm_group
+
+variables [ordered_comm_group α] {a b c d : α}
+
+/-! `inv_mem_Ixx_iff`, `sub_mem_Ixx_iff` -/
+@[to_additive] lemma inv_mem_Icc_iff : a⁻¹ ∈ set.Icc c d ↔ a ∈ set.Icc (d⁻¹) (c⁻¹) :=
+(and_comm _ _).trans $ and_congr inv_le' le_inv'
+@[to_additive] lemma inv_mem_Ico_iff : a⁻¹ ∈ set.Ico c d ↔ a ∈ set.Ioc (d⁻¹) (c⁻¹) :=
+(and_comm _ _).trans $ and_congr inv_lt' le_inv'
+@[to_additive] lemma inv_mem_Ioc_iff : a⁻¹ ∈ set.Ioc c d ↔ a ∈ set.Ico (d⁻¹) (c⁻¹) :=
+(and_comm _ _).trans $ and_congr inv_le' lt_inv'
+@[to_additive] lemma inv_mem_Ioo_iff : a⁻¹ ∈ set.Ioo c d ↔ a ∈ set.Ioo (d⁻¹) (c⁻¹) :=
+(and_comm _ _).trans $ and_congr inv_lt' lt_inv'
+
+end ordered_comm_group
+
+section ordered_add_comm_group
+
+variables [ordered_add_comm_group α] {a b c d : α}
+
+/-! `add_mem_Ixx_iff_left` -/
+lemma add_mem_Icc_iff_left : a + b ∈ set.Icc c d ↔ a ∈ set.Icc (c - b) (d - b) :=
+(and_congr sub_le_iff_le_add le_sub_iff_add_le).symm
+lemma add_mem_Ico_iff_left : a + b ∈ set.Ico c d ↔ a ∈ set.Ico (c - b) (d - b) :=
+(and_congr sub_le_iff_le_add lt_sub_iff_add_lt).symm
+lemma add_mem_Ioc_iff_left : a + b ∈ set.Ioc c d ↔ a ∈ set.Ioc (c - b) (d - b) :=
+(and_congr sub_lt_iff_lt_add le_sub_iff_add_le).symm
+lemma add_mem_Ioo_iff_left : a + b ∈ set.Ioo c d ↔ a ∈ set.Ioo (c - b) (d - b) :=
+(and_congr sub_lt_iff_lt_add lt_sub_iff_add_lt).symm
+
+/-! `add_mem_Ixx_iff_right` -/
+lemma add_mem_Icc_iff_right : a + b ∈ set.Icc c d ↔ b ∈ set.Icc (c - a) (d - a) :=
+(and_congr sub_le_iff_le_add' le_sub_iff_add_le').symm
+lemma add_mem_Ico_iff_right : a + b ∈ set.Ico c d ↔ b ∈ set.Ico (c - a) (d - a) :=
+(and_congr sub_le_iff_le_add' lt_sub_iff_add_lt').symm
+lemma add_mem_Ioc_iff_right : a + b ∈ set.Ioc c d ↔ b ∈ set.Ioc (c - a) (d - a) :=
+(and_congr sub_lt_iff_lt_add' le_sub_iff_add_le').symm
+lemma add_mem_Ioo_iff_right : a + b ∈ set.Ioo c d ↔ b ∈ set.Ioo (c - a) (d - a) :=
+(and_congr sub_lt_iff_lt_add' lt_sub_iff_add_lt').symm
+
+/-! `sub_mem_Ixx_iff_left` -/
+lemma sub_mem_Icc_iff_left : a - b ∈ set.Icc c d ↔ a ∈ set.Icc (c + b) (d + b) :=
+and_congr le_sub_iff_add_le sub_le_iff_le_add
+lemma sub_mem_Ico_iff_left : a - b ∈ set.Ico c d ↔ a ∈ set.Ico (c + b) (d + b) :=
+and_congr le_sub_iff_add_le sub_lt_iff_lt_add
+lemma sub_mem_Ioc_iff_left : a - b ∈ set.Ioc c d ↔ a ∈ set.Ioc (c + b) (d + b) :=
+and_congr lt_sub_iff_add_lt sub_le_iff_le_add
+lemma sub_mem_Ioo_iff_left : a - b ∈ set.Ioo c d ↔ a ∈ set.Ioo (c + b) (d + b) :=
+and_congr lt_sub_iff_add_lt sub_lt_iff_lt_add
+
+/-! `sub_mem_Ixx_iff_right` -/
+lemma sub_mem_Icc_iff_right : a - b ∈ set.Icc c d ↔ b ∈ set.Icc (a - d) (a - c) :=
+(and_comm _ _).trans $ and_congr sub_le_comm le_sub_comm
+lemma sub_mem_Ico_iff_right : a - b ∈ set.Ico c d ↔ b ∈ set.Ioc (a - d) (a - c) :=
+(and_comm _ _).trans $ and_congr sub_lt_comm le_sub_comm
+lemma sub_mem_Ioc_iff_right : a - b ∈ set.Ioc c d ↔ b ∈ set.Ico (a - d) (a - c) :=
+(and_comm _ _).trans $ and_congr sub_le_comm lt_sub_comm
+lemma sub_mem_Ioo_iff_right : a - b ∈ set.Ioo c d ↔ b ∈ set.Ioo (a - d) (a - c) :=
+(and_comm _ _).trans $ and_congr sub_lt_comm lt_sub_comm
+
+-- I think that symmetric intervals deserve attention and API: they arise all the time,
+-- for instance when considering metric balls in `ℝ`.
+lemma mem_Icc_iff_abs_le {R : Type*} [linear_ordered_add_comm_group R] {x y z : R} :
+  |x - y| ≤ z ↔ y ∈ Icc (x - z) (x + z) :=
+abs_le.trans $ (and_comm _ _).trans $ and_congr sub_le_comm neg_le_sub_iff_le_add
+
+end ordered_add_comm_group
+
+section linear_ordered_add_comm_group
+
+variables [linear_ordered_add_comm_group α]
+
+/-- If we remove a smaller interval from a larger, the result is nonempty -/
+lemma nonempty_Ico_sdiff {x dx y dy : α} (h : dy < dx) (hx : 0 < dx) :
+  nonempty ↥(Ico x (x + dx) \ Ico y (y + dy)) :=
+begin
+  cases lt_or_le x y with h' h',
+  { use x, simp [*, not_le.2 h'] },
+  { use max x (x + dy), simp [*, le_refl] }
+end
+
+end linear_ordered_add_comm_group
+
+end set
diff --git a/src/data/set/intervals/ord_connected_component.lean b/src/data/set/intervals/ord_connected_component.lean
index 7d2fa5011140d..53a1fe08d00ba 100644
--- a/src/data/set/intervals/ord_connected_component.lean
+++ b/src/data/set/intervals/ord_connected_component.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import data.set.intervals.ord_connected
+import tactic.wlog
 
 /-!
 # Order connected components of a set
diff --git a/src/data/set/intervals/order_iso.lean b/src/data/set/intervals/order_iso.lean
new file mode 100644
index 0000000000000..394a923b131d8
--- /dev/null
+++ b/src/data/set/intervals/order_iso.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy Degenne
+-/
+import data.set.intervals.basic
+import order.hom.basic
+
+/-!
+# Lemmas about images of intervals under order isomorphisms.
+-/
+
+variables {α β : Type*}
+open set
+
+namespace order_iso
+
+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]
+
+@[simp] lemma image_Iic (e : α ≃o β) (a : α) : e '' (Iic a) = Iic (e a) :=
+by rw [e.image_eq_preimage, e.symm.preimage_Iic, e.symm_symm]
+
+@[simp] lemma image_Ici (e : α ≃o β) (a : α) : e '' (Ici a) = Ici (e a) :=
+e.dual.image_Iic a
+
+@[simp] lemma image_Iio (e : α ≃o β) (a : α) : e '' (Iio a) = Iio (e a) :=
+by rw [e.image_eq_preimage, e.symm.preimage_Iio, e.symm_symm]
+
+@[simp] lemma image_Ioi (e : α ≃o β) (a : α) : e '' (Ioi a) = Ioi (e a) :=
+e.dual.image_Iio a
+
+@[simp] lemma image_Ioo (e : α ≃o β) (a b : α) : e '' (Ioo a b) = Ioo (e a) (e b) :=
+by rw [e.image_eq_preimage, e.symm.preimage_Ioo, e.symm_symm]
+
+@[simp] lemma image_Ioc (e : α ≃o β) (a b : α) : e '' (Ioc a b) = Ioc (e a) (e b) :=
+by rw [e.image_eq_preimage, e.symm.preimage_Ioc, e.symm_symm]
+
+@[simp] lemma image_Ico (e : α ≃o β) (a b : α) : e '' (Ico a b) = Ico (e a) (e b) :=
+by rw [e.image_eq_preimage, e.symm.preimage_Ico, e.symm_symm]
+
+@[simp] lemma image_Icc (e : α ≃o β) (a b : α) : e '' (Icc a b) = Icc (e a) (e b) :=
+by rw [e.image_eq_preimage, e.symm.preimage_Icc, e.symm_symm]
+
+end preorder
+
+/-- Order isomorphism between `Iic (⊤ : α)` and `α` when `α` has a top element -/
+def Iic_top [preorder α] [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 [preorder α] [order_bot α] : set.Ici (⊥ : α) ≃o α :=
+{ map_rel_iff' := λ x y, by refl,
+  .. (@equiv.subtype_univ_equiv α (set.Ici (⊥ : α)) (λ x, bot_le)) }
+
+end order_iso
diff --git a/src/data/set/intervals/unordered_interval.lean b/src/data/set/intervals/unordered_interval.lean
index e9e5239712fcb..0c8ac7d108ce0 100644
--- a/src/data/set/intervals/unordered_interval.lean
+++ b/src/data/set/intervals/unordered_interval.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Zhouhang Zhou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou
 -/
-import order.bounds
-import data.set.intervals.image_preimage
+import order.bounds.basic
+import data.set.intervals.basic
 
 /-!
 # Intervals without endpoints ordering
@@ -27,9 +27,7 @@ make the notation available.
 
 universe u
 
-open function
-open_locale pointwise
-open order_dual (to_dual of_dual)
+open function order_dual (to_dual of_dual)
 
 namespace set
 
@@ -214,97 +212,4 @@ lemma interval_oc_injective_left (a : α) : injective (Ι a) :=
 by simpa only [interval_oc_swap] using interval_oc_injective_right a
 
 end linear_order
-
-open_locale interval
-
-section ordered_add_comm_group
-
-variables {α : Type u} [linear_ordered_add_comm_group α] (a b c x y : α)
-
-@[simp] lemma preimage_const_add_interval : (λ x, a + x) ⁻¹' [b, c] = [b - a, c - a] :=
-by simp only [interval, preimage_const_add_Icc, min_sub_sub_right, max_sub_sub_right]
-
-@[simp] lemma preimage_add_const_interval : (λ x, x + a) ⁻¹' [b, c] = [b - a, c - a] :=
-by simpa only [add_comm] using preimage_const_add_interval a b c
-
-@[simp] lemma preimage_neg_interval : - [a, b] = [-a, -b] :=
-by simp only [interval, preimage_neg_Icc, min_neg_neg, max_neg_neg]
-
-@[simp] lemma preimage_sub_const_interval : (λ x, x - a) ⁻¹' [b, c] = [b + a, c + a] :=
-by simp [sub_eq_add_neg]
-
-@[simp] lemma preimage_const_sub_interval : (λ x, a - x) ⁻¹' [b, c] = [a - b, a - c] :=
-by { rw [interval, interval, preimage_const_sub_Icc],
-  simp only [sub_eq_add_neg, min_add_add_left, max_add_add_left, min_neg_neg, max_neg_neg], }
-
-@[simp] lemma image_const_add_interval : (λ x, a + x) '' [b, c] = [a + b, a + c] :=
-by simp [add_comm]
-
-@[simp] lemma image_add_const_interval : (λ x, x + a) '' [b, c] = [b + a, c + a] :=
-by simp
-
-@[simp] lemma image_const_sub_interval : (λ x, a - x) '' [b, c] = [a - b, a - c] :=
-by simp [sub_eq_add_neg, image_comp (λ x, a + x) (λ x, -x)]
-
-@[simp] lemma image_sub_const_interval : (λ x, x - a) '' [b, c] = [b - a, c - a] :=
-by simp [sub_eq_add_neg, add_comm]
-
-lemma image_neg_interval : has_neg.neg '' [a, b] = [-a, -b] := by simp
-
-variables {a b c x y}
-
-/-- If `[x, y]` is a subinterval of `[a, b]`, then the distance between `x` and `y`
-is less than or equal to that of `a` and `b` -/
-lemma abs_sub_le_of_subinterval (h : [x, y] ⊆ [a, b]) : |y - x| ≤ |b - a| :=
-begin
-  rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs],
-  rw [interval_subset_interval_iff_le] at h,
-  exact sub_le_sub h.2 h.1,
-end
-
-/-- If `x ∈ [a, b]`, then the distance between `a` and `x` is less than or equal to
-that of `a` and `b`  -/
-lemma abs_sub_left_of_mem_interval (h : x ∈ [a, b]) : |x - a| ≤ |b - a| :=
-abs_sub_le_of_subinterval (interval_subset_interval_left h)
-
-/-- If `x ∈ [a, b]`, then the distance between `x` and `b` is less than or equal to
-that of `a` and `b`  -/
-lemma abs_sub_right_of_mem_interval (h : x ∈ [a, b]) : |b - x| ≤ |b - a| :=
-abs_sub_le_of_subinterval (interval_subset_interval_right h)
-
-end ordered_add_comm_group
-
-section linear_ordered_field
-
-variables {k : Type u} [linear_ordered_field k] {a : k}
-
-@[simp] lemma preimage_mul_const_interval (ha : a ≠ 0) (b c : k) :
-  (λ x, x * a) ⁻¹' [b, c] = [b / a, c / a] :=
-(lt_or_gt_of_ne ha).elim
-  (λ ha, by simp [interval, ha, ha.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos])
-  (λ (ha : 0 < a), by simp [interval, ha, ha.le, min_div_div_right, max_div_div_right])
-
-@[simp] lemma preimage_const_mul_interval (ha : a ≠ 0) (b c : k) :
-  (λ x, a * x) ⁻¹' [b, c] = [b / a, c / a] :=
-by simp only [← preimage_mul_const_interval ha, mul_comm]
-
-@[simp] lemma preimage_div_const_interval (ha : a ≠ 0) (b c : k) :
-  (λ x, x / a) ⁻¹' [b, c] = [b * a, c * a] :=
-by simp only [div_eq_mul_inv, preimage_mul_const_interval (inv_ne_zero ha), inv_inv]
-
-@[simp] lemma image_mul_const_interval (a b c : k) : (λ x, x * a) '' [b, c] = [b * a, c * a] :=
-if ha : a = 0 then by simp [ha] else
-calc (λ x, x * a) '' [b, c] = (λ x, x * a⁻¹) ⁻¹' [b, c] :
-  (units.mk0 a ha).mul_right.image_eq_preimage _
-... = (λ x, x / a) ⁻¹' [b, c] : by simp only [div_eq_mul_inv]
-... = [b * a, c * a] : preimage_div_const_interval ha _ _
-
-@[simp] lemma image_const_mul_interval (a b c : k) : (λ x, a * x) '' [b, c] = [a * b, a * c] :=
-by simpa only [mul_comm] using image_mul_const_interval a b c
-
-@[simp] lemma image_div_const_interval (a b c : k) : (λ x, x / a) '' [b, c] = [b / a, c / a] :=
-by simp only [div_eq_mul_inv, image_mul_const_interval]
-
-end linear_ordered_field
-
 end set
diff --git a/src/data/set/pairwise.lean b/src/data/set/pairwise.lean
index 005e3961858a9..e9c4e27aa5b9f 100644
--- a/src/data/set/pairwise.lean
+++ b/src/data/set/pairwise.lean
@@ -3,18 +3,21 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import data.set.lattice
 import logic.relation
+import logic.pairwise
+import data.set.lattice
 
 /-!
 # Relations holding pairwise
 
-This file defines pairwise relations and pairwise disjoint indexed sets.
+This file defines pairwise relations on sets and pairwise disjoint indexed sets.
+
+We also prove many basic facts about `pairwise`. It is possible that an intermediate file,
+with more imports than `logic.pairwise` but not importing `data.set.lattice` would be appropriate
+to hold many of these basic facts.
 
 ## Main declarations
 
-* `pairwise`: `pairwise r` states that `r i j` for all `i ≠ j`.
-* `set.pairwise`: `s.pairwise r` states that `r i j` for all `i ≠ j` with `i, j ∈ s`.
 * `set.pairwise_disjoint`: `s.pairwise_disjoint f` states that images under `f` of distinct elements
   of `s` are either equal or `disjoint`.
 
@@ -31,14 +34,6 @@ variables {α β γ ι ι' : Type*} {r p q : α → α → Prop}
 section pairwise
 variables {f g : ι → α} {s t u : set α} {a b : α}
 
-/-- A relation `r` holds pairwise if `r i j` for all `i ≠ j`. -/
-def pairwise (r : α → α → Prop) := ∀ ⦃i j⦄, i ≠ j → r i j
-
-lemma pairwise.mono (hr : pairwise r) (h : ∀ ⦃i j⦄, r i j → p i j) : pairwise p :=
-λ i j hij, h $ hr hij
-
-protected lemma pairwise.eq (h : pairwise r) : ¬ r a b → a = b := not_imp_comm.1 $ @h _ _
-
 lemma pairwise_on_bool (hr : symmetric r) {a b : α} : pairwise (r on (λ c, cond c a b)) ↔ r a b :=
 by simpa [pairwise, function.on_fun] using @hr a b
 
@@ -58,34 +53,15 @@ lemma pairwise_disjoint.mono [semilattice_inf α] [order_bot α]
   (hs : pairwise (disjoint on f)) (h : g ≤ f) : pairwise (disjoint on g) :=
 hs.mono (λ i j hij, disjoint.mono (h i) (h j) hij)
 
-lemma function.injective_iff_pairwise_ne : injective f ↔ pairwise ((≠) on f) :=
-forall₂_congr $ λ i j, not_imp_not.symm
-
 alias function.injective_iff_pairwise_ne ↔ function.injective.pairwise_ne _
 
 namespace set
 
-/-- The relation `r` holds pairwise on the set `s` if `r x y` for all *distinct* `x y ∈ s`. -/
-protected def pairwise (s : set α) (r : α → α → Prop) := ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → r x y
-
-lemma pairwise_of_forall (s : set α) (r : α → α → Prop) (h : ∀ a b, r a b) : s.pairwise r :=
-λ a _ b _ _, h a b
-
-lemma pairwise.imp_on (h : s.pairwise r) (hrp : s.pairwise (λ ⦃a b : α⦄, r a b → p a b)) :
-  s.pairwise p :=
-λ a ha b hb hab, hrp ha hb hab $ h ha hb hab
-
-lemma pairwise.imp (h : s.pairwise r) (hpq : ∀ ⦃a b : α⦄, r a b → p a b) : s.pairwise p :=
-h.imp_on $ pairwise_of_forall s _ hpq
-
 lemma pairwise.mono (h : t ⊆ s) (hs : s.pairwise r) : t.pairwise r :=
 λ x xt y yt, hs (h xt) (h yt)
 
 lemma pairwise.mono' (H : r ≤ p) (hr : s.pairwise r) : s.pairwise p := hr.imp H
 
-protected lemma pairwise.eq (hs : s.pairwise r) (ha : a ∈ s) (hb : b ∈ s) (h : ¬ r a b) : a = b :=
-of_not_not $ λ hab, h $ hs ha hb hab
-
 lemma pairwise_top (s : set α) : s.pairwise ⊤ := pairwise_of_forall s _ (λ a b, trivial)
 
 protected lemma subsingleton.pairwise (h : s.subsingleton) (r : α → α → Prop) :
@@ -103,10 +79,6 @@ forall₄_congr $ λ a _ b _, or_iff_not_imp_left.symm.trans $ or_iff_right_of_i
 
 alias pairwise_iff_of_refl ↔ pairwise.of_refl _
 
-lemma _root_.reflexive.set_pairwise_iff (hr : reflexive r) :
-  s.pairwise r ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b :=
-forall₄_congr $ λ a _ b _, or_iff_not_imp_left.symm.trans $ or_iff_right_of_imp $ eq.rec $ hr a
-
 lemma nonempty.pairwise_iff_exists_forall [is_equiv α r] {s : set ι} (hs : s.nonempty) :
   (s.pairwise (r on f)) ↔ ∃ z, ∀ x ∈ s, r (f x) z :=
 begin
@@ -191,11 +163,6 @@ by simp only [set.pairwise, pairwise, mem_univ, forall_const]
 
 alias pairwise_bot_iff ↔ pairwise.subsingleton _
 
-lemma pairwise.on_injective (hs : s.pairwise r) (hf : function.injective f)
-  (hfs : ∀ x, f x ∈ s) :
-  pairwise (r on f) :=
-λ i j hij, hs (hfs i) (hfs j) (hf.ne hij)
-
 lemma inj_on.pairwise_image {s : set ι} (h : s.inj_on f) :
   (f '' s).pairwise r ↔ s.pairwise (r on f) :=
 by simp [h.eq_iff, set.pairwise] {contextual := tt}
@@ -219,8 +186,6 @@ by { rw [sUnion_eq_Union, pairwise_Union (h.directed_coe), set_coe.forall], refl
 
 end set
 
-lemma pairwise.set_pairwise (h : pairwise r) (s : set α) : s.pairwise r := λ x hx y hy hxy, h hxy
-
 end pairwise
 
 lemma pairwise_subtype_iff_pairwise_set (s : set α) (r : α → α → Prop) :
diff --git a/src/data/set/intervals/image_preimage.lean b/src/data/set/pointwise/interval.lean
similarity index 72%
rename from src/data/set/intervals/image_preimage.lean
rename to src/data/set/pointwise/interval.lean
index 12de3d9947f87..c7c59fdb570fb 100644
--- a/src/data/set/intervals/image_preimage.lean
+++ b/src/data/set/pointwise/interval.lean
@@ -3,6 +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, Patrick Massot
 -/
+import data.set.intervals.unordered_interval
 import data.set.pointwise.basic
 import algebra.order.field.basic
 
@@ -15,8 +16,9 @@ lemmas about preimages and images of all intervals. We also prove a few lemmas a
 `x ↦ a * x`, `x ↦ x * a` and `x ↦ x⁻¹`.
 -/
 
-universe u
-open_locale pointwise
+open_locale interval pointwise
+
+variables {α : Type*}
 
 namespace set
 
@@ -30,7 +32,7 @@ The lemmas in this section state that addition maps intervals bijectively. The t
 TODO : move as much as possible in this file to the setting of this weaker typeclass.
 -/
 
-variables {α : Type u} [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] (a b d : α)
+variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] (a b d : α)
 
 lemma Icc_add_bij : bij_on (+d) (Icc a b) (Icc (a + d) (b + d)) :=
 begin
@@ -91,8 +93,7 @@ end
 end has_exists_add_of_le
 
 section ordered_add_comm_group
-
-variables {G : Type u} [ordered_add_comm_group G] (a b c : G)
+variables [ordered_add_comm_group α] (a b c : α)
 
 /-!
 ### Preimages under `x ↦ a + x`
@@ -356,147 +357,229 @@ end
 
 end ordered_add_comm_group
 
+section linear_ordered_add_comm_group
+variables [linear_ordered_add_comm_group α] (a b c d : α)
+
+@[simp] lemma preimage_const_add_interval : (λ x, a + x) ⁻¹' [b, c] = [b - a, c - a] :=
+by simp only [interval, preimage_const_add_Icc, min_sub_sub_right, max_sub_sub_right]
+
+@[simp] lemma preimage_add_const_interval : (λ x, x + a) ⁻¹' [b, c] = [b - a, c - a] :=
+by simpa only [add_comm] using preimage_const_add_interval a b c
+
+@[simp] lemma preimage_neg_interval : - [a, b] = [-a, -b] :=
+by simp only [interval, preimage_neg_Icc, min_neg_neg, max_neg_neg]
+
+@[simp] lemma preimage_sub_const_interval : (λ x, x - a) ⁻¹' [b, c] = [b + a, c + a] :=
+by simp [sub_eq_add_neg]
+
+@[simp] lemma preimage_const_sub_interval : (λ x, a - x) ⁻¹' [b, c] = [a - b, a - c] :=
+by { rw [interval, interval, preimage_const_sub_Icc],
+  simp only [sub_eq_add_neg, min_add_add_left, max_add_add_left, min_neg_neg, max_neg_neg], }
+
+@[simp] lemma image_const_add_interval : (λ x, a + x) '' [b, c] = [a + b, a + c] :=
+by simp [add_comm]
+
+@[simp] lemma image_add_const_interval : (λ x, x + a) '' [b, c] = [b + a, c + a] :=
+by simp
+
+@[simp] lemma image_const_sub_interval : (λ x, a - x) '' [b, c] = [a - b, a - c] :=
+by simp [sub_eq_add_neg, image_comp (λ x, a + x) (λ x, -x)]
+
+@[simp] lemma image_sub_const_interval : (λ x, x - a) '' [b, c] = [b - a, c - a] :=
+by simp [sub_eq_add_neg, add_comm]
+
+lemma image_neg_interval : has_neg.neg '' [a, b] = [-a, -b] := by simp
+
+variables {a b c d}
+
+/-- If `[c, d]` is a subinterval of `[a, b]`, then the distance between `c` and `d` is less than or
+equal to that of `a` and `b` -/
+lemma abs_sub_le_of_subinterval (h : [c, d] ⊆ [a, b]) : |d - c| ≤ |b - a| :=
+begin
+  rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs],
+  rw [interval_subset_interval_iff_le] at h,
+  exact sub_le_sub h.2 h.1,
+end
+
+/-- If `c ∈ [a, b]`, then the distance between `a` and `c` is less than or equal to
+that of `a` and `b`  -/
+lemma abs_sub_left_of_mem_interval (h : c ∈ [a, b]) : |c - a| ≤ |b - a| :=
+abs_sub_le_of_subinterval (interval_subset_interval_left h)
+
+/-- If `x ∈ [a, b]`, then the distance between `c` and `b` is less than or equal to
+that of `a` and `b`  -/
+lemma abs_sub_right_of_mem_interval (h : c ∈ [a, b]) : |b - c| ≤ |b - a| :=
+abs_sub_le_of_subinterval (interval_subset_interval_right h)
+
+end linear_ordered_add_comm_group
+
 /-!
 ### Multiplication and inverse in a field
 -/
 
 section linear_ordered_field
+variables [linear_ordered_field α] {a : α}
 
-variables {k : Type u} [linear_ordered_field k]
-
-@[simp] lemma preimage_mul_const_Iio (a : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_mul_const_Iio (a : α) {c : α} (h : 0 < c) :
   (λ x, x * c) ⁻¹' (Iio a) = Iio (a / c) :=
 ext $ λ x, (lt_div_iff h).symm
 
-@[simp] lemma preimage_mul_const_Ioi (a : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_mul_const_Ioi (a : α) {c : α} (h : 0 < c) :
   (λ x, x * c) ⁻¹' (Ioi a) = Ioi (a / c) :=
 ext $ λ x, (div_lt_iff h).symm
 
-@[simp] lemma preimage_mul_const_Iic (a : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_mul_const_Iic (a : α) {c : α} (h : 0 < c) :
   (λ x, x * c) ⁻¹' (Iic a) = Iic (a / c) :=
 ext $ λ x, (le_div_iff h).symm
 
-@[simp] lemma preimage_mul_const_Ici (a : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_mul_const_Ici (a : α) {c : α} (h : 0 < c) :
   (λ x, x * c) ⁻¹' (Ici a) = Ici (a / c) :=
 ext $ λ x, (div_le_iff h).symm
 
-@[simp] lemma preimage_mul_const_Ioo (a b : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_mul_const_Ioo (a b : α) {c : α} (h : 0 < c) :
   (λ x, x * c) ⁻¹' (Ioo a b) = Ioo (a / c) (b / c) :=
 by simp [← Ioi_inter_Iio, h]
 
-@[simp] lemma preimage_mul_const_Ioc (a b : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_mul_const_Ioc (a b : α) {c : α} (h : 0 < c) :
   (λ x, x * c) ⁻¹' (Ioc a b) = Ioc (a / c) (b / c) :=
 by simp [← Ioi_inter_Iic, h]
 
-@[simp] lemma preimage_mul_const_Ico (a b : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_mul_const_Ico (a b : α) {c : α} (h : 0 < c) :
   (λ x, x * c) ⁻¹' (Ico a b) = Ico (a / c) (b / c) :=
 by simp [← Ici_inter_Iio, h]
 
-@[simp] lemma preimage_mul_const_Icc (a b : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_mul_const_Icc (a b : α) {c : α} (h : 0 < c) :
   (λ x, x * c) ⁻¹' (Icc a b) = Icc (a / c) (b / c) :=
 by simp [← Ici_inter_Iic, h]
 
-@[simp] lemma preimage_mul_const_Iio_of_neg (a : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_mul_const_Iio_of_neg (a : α) {c : α} (h : c < 0) :
   (λ x, x * c) ⁻¹' (Iio a) = Ioi (a / c) :=
 ext $ λ x, (div_lt_iff_of_neg h).symm
 
-@[simp] lemma preimage_mul_const_Ioi_of_neg (a : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_mul_const_Ioi_of_neg (a : α) {c : α} (h : c < 0) :
   (λ x, x * c) ⁻¹' (Ioi a) = Iio (a / c) :=
 ext $ λ x, (lt_div_iff_of_neg h).symm
 
-@[simp] lemma preimage_mul_const_Iic_of_neg (a : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_mul_const_Iic_of_neg (a : α) {c : α} (h : c < 0) :
   (λ x, x * c) ⁻¹' (Iic a) = Ici (a / c) :=
 ext $ λ x, (div_le_iff_of_neg h).symm
 
-@[simp] lemma preimage_mul_const_Ici_of_neg (a : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_mul_const_Ici_of_neg (a : α) {c : α} (h : c < 0) :
   (λ x, x * c) ⁻¹' (Ici a) = Iic (a / c) :=
 ext $ λ x, (le_div_iff_of_neg h).symm
 
-@[simp] lemma preimage_mul_const_Ioo_of_neg (a b : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_mul_const_Ioo_of_neg (a b : α) {c : α} (h : c < 0) :
   (λ x, x * c) ⁻¹' (Ioo a b) = Ioo (b / c) (a / c) :=
 by simp [← Ioi_inter_Iio, h, inter_comm]
 
-@[simp] lemma preimage_mul_const_Ioc_of_neg (a b : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_mul_const_Ioc_of_neg (a b : α) {c : α} (h : c < 0) :
   (λ x, x * c) ⁻¹' (Ioc a b) = Ico (b / c) (a / c) :=
 by simp [← Ioi_inter_Iic, ← Ici_inter_Iio, h, inter_comm]
 
-@[simp] lemma preimage_mul_const_Ico_of_neg (a b : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_mul_const_Ico_of_neg (a b : α) {c : α} (h : c < 0) :
   (λ x, x * c) ⁻¹' (Ico a b) = Ioc (b / c) (a / c) :=
 by simp [← Ici_inter_Iio, ← Ioi_inter_Iic, h, inter_comm]
 
-@[simp] lemma preimage_mul_const_Icc_of_neg (a b : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_mul_const_Icc_of_neg (a b : α) {c : α} (h : c < 0) :
   (λ x, x * c) ⁻¹' (Icc a b) = Icc (b / c) (a / c) :=
 by simp [← Ici_inter_Iic, h, inter_comm]
 
-@[simp] lemma preimage_const_mul_Iio (a : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_const_mul_Iio (a : α) {c : α} (h : 0 < c) :
   ((*) c) ⁻¹' (Iio a) = Iio (a / c) :=
 ext $ λ x, (lt_div_iff' h).symm
 
-@[simp] lemma preimage_const_mul_Ioi (a : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_const_mul_Ioi (a : α) {c : α} (h : 0 < c) :
   ((*) c) ⁻¹' (Ioi a) = Ioi (a / c) :=
 ext $ λ x, (div_lt_iff' h).symm
 
-@[simp] lemma preimage_const_mul_Iic (a : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_const_mul_Iic (a : α) {c : α} (h : 0 < c) :
   ((*) c) ⁻¹' (Iic a) = Iic (a / c) :=
 ext $ λ x, (le_div_iff' h).symm
 
-@[simp] lemma preimage_const_mul_Ici (a : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_const_mul_Ici (a : α) {c : α} (h : 0 < c) :
   ((*) c) ⁻¹' (Ici a) = Ici (a / c) :=
 ext $ λ x, (div_le_iff' h).symm
 
-@[simp] lemma preimage_const_mul_Ioo (a b : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_const_mul_Ioo (a b : α) {c : α} (h : 0 < c) :
   ((*) c) ⁻¹' (Ioo a b) = Ioo (a / c) (b / c) :=
 by simp [← Ioi_inter_Iio, h]
 
-@[simp] lemma preimage_const_mul_Ioc (a b : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_const_mul_Ioc (a b : α) {c : α} (h : 0 < c) :
   ((*) c) ⁻¹' (Ioc a b) = Ioc (a / c) (b / c) :=
 by simp [← Ioi_inter_Iic, h]
 
-@[simp] lemma preimage_const_mul_Ico (a b : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_const_mul_Ico (a b : α) {c : α} (h : 0 < c) :
   ((*) c) ⁻¹' (Ico a b) = Ico (a / c) (b / c) :=
 by simp [← Ici_inter_Iio, h]
 
-@[simp] lemma preimage_const_mul_Icc (a b : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_const_mul_Icc (a b : α) {c : α} (h : 0 < c) :
   ((*) c) ⁻¹' (Icc a b) = Icc (a / c) (b / c) :=
 by simp [← Ici_inter_Iic, h]
 
-@[simp] lemma preimage_const_mul_Iio_of_neg (a : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_const_mul_Iio_of_neg (a : α) {c : α} (h : c < 0) :
   ((*) c) ⁻¹' (Iio a) = Ioi (a / c) :=
 by simpa only [mul_comm] using preimage_mul_const_Iio_of_neg a h
 
-@[simp] lemma preimage_const_mul_Ioi_of_neg (a : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_const_mul_Ioi_of_neg (a : α) {c : α} (h : c < 0) :
   ((*) c) ⁻¹' (Ioi a) = Iio (a / c) :=
 by simpa only [mul_comm] using preimage_mul_const_Ioi_of_neg a h
 
-@[simp] lemma preimage_const_mul_Iic_of_neg (a : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_const_mul_Iic_of_neg (a : α) {c : α} (h : c < 0) :
   ((*) c) ⁻¹' (Iic a) = Ici (a / c) :=
 by simpa only [mul_comm] using preimage_mul_const_Iic_of_neg a h
 
-@[simp] lemma preimage_const_mul_Ici_of_neg (a : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_const_mul_Ici_of_neg (a : α) {c : α} (h : c < 0) :
   ((*) c) ⁻¹' (Ici a) = Iic (a / c) :=
 by simpa only [mul_comm] using preimage_mul_const_Ici_of_neg a h
 
-@[simp] lemma preimage_const_mul_Ioo_of_neg (a b : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_const_mul_Ioo_of_neg (a b : α) {c : α} (h : c < 0) :
   ((*) c) ⁻¹' (Ioo a b) = Ioo (b / c) (a / c) :=
 by simpa only [mul_comm] using preimage_mul_const_Ioo_of_neg a b h
 
-@[simp] lemma preimage_const_mul_Ioc_of_neg (a b : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_const_mul_Ioc_of_neg (a b : α) {c : α} (h : c < 0) :
   ((*) c) ⁻¹' (Ioc a b) = Ico (b / c) (a / c) :=
 by simpa only [mul_comm] using preimage_mul_const_Ioc_of_neg a b h
 
-@[simp] lemma preimage_const_mul_Ico_of_neg (a b : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_const_mul_Ico_of_neg (a b : α) {c : α} (h : c < 0) :
   ((*) c) ⁻¹' (Ico a b) = Ioc (b / c) (a / c) :=
 by simpa only [mul_comm] using preimage_mul_const_Ico_of_neg a b h
 
-@[simp] lemma preimage_const_mul_Icc_of_neg (a b : k) {c : k} (h : c < 0) :
+@[simp] lemma preimage_const_mul_Icc_of_neg (a b : α) {c : α} (h : c < 0) :
   ((*) c) ⁻¹' (Icc a b) = Icc (b / c) (a / c) :=
 by simpa only [mul_comm] using preimage_mul_const_Icc_of_neg a b h
 
-lemma image_mul_right_Icc' (a b : k) {c : k} (h : 0 < c) :
+@[simp] lemma preimage_mul_const_interval (ha : a ≠ 0) (b c : α) :
+  (λ x, x * a) ⁻¹' [b, c] = [b / a, c / a] :=
+(lt_or_gt_of_ne ha).elim
+  (λ ha, by simp [interval, ha, ha.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos])
+  (λ (ha : 0 < a), by simp [interval, ha, ha.le, min_div_div_right, max_div_div_right])
+
+@[simp] lemma preimage_const_mul_interval (ha : a ≠ 0) (b c : α) :
+  (λ x, a * x) ⁻¹' [b, c] = [b / a, c / a] :=
+by simp only [← preimage_mul_const_interval ha, mul_comm]
+
+@[simp] lemma preimage_div_const_interval (ha : a ≠ 0) (b c : α) :
+  (λ x, x / a) ⁻¹' [b, c] = [b * a, c * a] :=
+by simp only [div_eq_mul_inv, preimage_mul_const_interval (inv_ne_zero ha), inv_inv]
+
+@[simp] lemma image_mul_const_interval (a b c : α) : (λ x, x * a) '' [b, c] = [b * a, c * a] :=
+if ha : a = 0 then by simp [ha] else
+calc (λ x, x * a) '' [b, c] = (λ x, x * a⁻¹) ⁻¹' [b, c] :
+  (units.mk0 a ha).mul_right.image_eq_preimage _
+... = (λ x, x / a) ⁻¹' [b, c] : by simp only [div_eq_mul_inv]
+... = [b * a, c * a] : preimage_div_const_interval ha _ _
+
+@[simp] lemma image_const_mul_interval (a b c : α) : (λ x, a * x) '' [b, c] = [a * b, a * c] :=
+by simpa only [mul_comm] using image_mul_const_interval a b c
+
+@[simp] lemma image_div_const_interval (a b c : α) : (λ x, x / a) '' [b, c] = [b / a, c / a] :=
+by simp only [div_eq_mul_inv, image_mul_const_interval]
+
+lemma image_mul_right_Icc' (a b : α) {c : α} (h : 0 < c) :
   (λ x, x * c) '' Icc a b = Icc (a * c) (b * c) :=
 ((units.mk0 c h.ne').mul_right.image_eq_preimage _).trans (by simp [h, division_def])
 
-lemma image_mul_right_Icc {a b c : k} (hab : a ≤ b) (hc : 0 ≤ c) :
+lemma image_mul_right_Icc {a b c : α} (hab : a ≤ b) (hc : 0 ≤ c) :
   (λ x, x * c) '' Icc a b = Icc (a * c) (b * c) :=
 begin
   cases eq_or_lt_of_le hc,
@@ -505,31 +588,31 @@ begin
   exact image_mul_right_Icc' a b ‹0 < c›
 end
 
-lemma image_mul_left_Icc' {a : k} (h : 0 < a) (b c : k) :
+lemma image_mul_left_Icc' {a : α} (h : 0 < a) (b c : α) :
   ((*) a) '' Icc b c = Icc (a * b) (a * c) :=
 by { convert image_mul_right_Icc' b c h using 1; simp only [mul_comm _ a] }
 
-lemma image_mul_left_Icc {a b c : k} (ha : 0 ≤ a) (hbc : b ≤ c) :
+lemma image_mul_left_Icc {a b c : α} (ha : 0 ≤ a) (hbc : b ≤ c) :
   ((*) a) '' Icc b c = Icc (a * b) (a * c) :=
 by { convert image_mul_right_Icc hbc ha using 1; simp only [mul_comm _ a] }
 
-lemma image_mul_right_Ioo (a b : k) {c : k} (h : 0 < c) :
+lemma image_mul_right_Ioo (a b : α) {c : α} (h : 0 < c) :
   (λ x, x * c) '' Ioo a b = Ioo (a * c) (b * c) :=
 ((units.mk0 c h.ne').mul_right.image_eq_preimage _).trans (by simp [h, division_def])
 
-lemma image_mul_left_Ioo {a : k} (h : 0 < a) (b c : k) :
+lemma image_mul_left_Ioo {a : α} (h : 0 < a) (b c : α) :
   ((*) a) '' Ioo b c = Ioo (a * b) (a * c) :=
 by { convert image_mul_right_Ioo b c h using 1; simp only [mul_comm _ a] }
 
 /-- The (pre)image under `inv` of `Ioo 0 a` is `Ioi a⁻¹`. -/
-lemma inv_Ioo_0_left {a : k} (ha : 0 < a) : (Ioo 0 a)⁻¹ = Ioi a⁻¹ :=
+lemma inv_Ioo_0_left {a : α} (ha : 0 < a) : (Ioo 0 a)⁻¹ = Ioi a⁻¹ :=
 begin
   ext x,
   exact ⟨λ h, inv_inv x ▸ (inv_lt_inv ha h.1).2 h.2, λ h, ⟨inv_pos.2 $ (inv_pos.2 ha).trans h,
     inv_inv a ▸ (inv_lt_inv ((inv_pos.2 ha).trans h) (inv_pos.2 ha)).2 h⟩⟩,
 end
 
-lemma inv_Ioi {a : k} (ha : 0 < a) : (Ioi a)⁻¹ = Ioo 0 a⁻¹ :=
+lemma inv_Ioi {a : α} (ha : 0 < a) : (Ioi a)⁻¹ = Ioo 0 a⁻¹ :=
 by rw [inv_eq_iff_inv_eq, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]
 
 lemma image_const_mul_Ioi_zero {k : Type*} [linear_ordered_field k]
@@ -542,7 +625,7 @@ by erw [(units.mk0 x hx.ne').mul_left.image_eq_preimage, preimage_const_mul_Ioi
 ### Images under `x ↦ a * x + b`
 -/
 
-@[simp] lemma image_affine_Icc' {a : k} (h : 0 < a) (b c d : k) :
+@[simp] lemma image_affine_Icc' {a : α} (h : 0 < a) (b c d : α) :
   (λ x, a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b) :=
 begin
   suffices : (λ x, x + b) '' ((λ x, a * x) '' Icc c d) = Icc (a * c + b) (a * d + b),
diff --git a/src/dynamics/periodic_pts.lean b/src/dynamics/periodic_pts.lean
index 9861814a1e6bb..706e8668d8ed9 100644
--- a/src/dynamics/periodic_pts.lean
+++ b/src/dynamics/periodic_pts.lean
@@ -6,6 +6,7 @@ Authors: Yury G. Kudryashov
 
 import algebra.hom.iterate
 import data.list.cycle
+import data.pnat.basic
 import data.nat.prime
 import data.set.pointwise.basic
 import dynamics.fixed_points.basic
diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean
index 9646c9c246b50..401f552008396 100644
--- a/src/group_theory/submonoid/operations.lean
+++ b/src/group_theory/submonoid/operations.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
 Amelia Livingston, Yury Kudryashov
 -/
+import algebra.order.group.basic
 import group_theory.group_action.defs
 import group_theory.submonoid.basic
 import group_theory.subsemigroup.operations
diff --git a/src/group_theory/subsemigroup/operations.lean b/src/group_theory/subsemigroup/operations.lean
index db85872d922ed..26abc32512503 100644
--- a/src/group_theory/subsemigroup/operations.lean
+++ b/src/group_theory/subsemigroup/operations.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzza
 Amelia Livingston, Yury Kudryashov, Yakov Pechersky, Jireh Loreaux
 -/
 import group_theory.subsemigroup.basic
+import algebra.group.prod
 
 /-!
 # Operations on `subsemigroup`s
diff --git a/src/linear_algebra/affine_space/affine_map.lean b/src/linear_algebra/affine_space/affine_map.lean
index 878eb6c3a187e..2afe884989e5f 100644
--- a/src/linear_algebra/affine_space/affine_map.lean
+++ b/src/linear_algebra/affine_space/affine_map.lean
@@ -3,13 +3,11 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
-import algebra.add_torsor
-import data.set.intervals.unordered_interval
+import data.set.pointwise.interval
 import linear_algebra.affine_space.basic
 import linear_algebra.bilinear_map
 import linear_algebra.pi
 import linear_algebra.prod
-import tactic.abel
 
 /-!
 # Affine maps
diff --git a/src/linear_algebra/free_module/basic.lean b/src/linear_algebra/free_module/basic.lean
index 15a86b4839cb2..25c1a2c1321fe 100644
--- a/src/linear_algebra/free_module/basic.lean
+++ b/src/linear_algebra/free_module/basic.lean
@@ -5,7 +5,7 @@ Authors: Riccardo Brasca
 -/
 
 import linear_algebra.direct_sum.finsupp
-import logic.small
+import logic.small.basic
 import linear_algebra.std_basis
 import linear_algebra.finsupp_vector_space
 
diff --git a/src/logic/encodable/basic.lean b/src/logic/encodable/basic.lean
index 6b5e4ce62d351..d0c537f6f5426 100644
--- a/src/logic/encodable/basic.lean
+++ b/src/logic/encodable/basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 import logic.equiv.nat
+import data.pnat.basic
 import order.directed
 import data.countable.defs
 import order.rel_iso
diff --git a/src/logic/equiv/nat.lean b/src/logic/equiv/nat.lean
index 78ad9cb376042..b86c0bb7680fb 100644
--- a/src/logic/equiv/nat.lean
+++ b/src/logic/equiv/nat.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.nat.pairing
-import data.pnat.basic
+import data.pnat.defs
 
 /-!
 # Equivalences involving `ℕ`
diff --git a/src/logic/pairwise.lean b/src/logic/pairwise.lean
new file mode 100644
index 0000000000000..0f4677e2afc9e
--- /dev/null
+++ b/src/logic/pairwise.lean
@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+-/
+import logic.relation
+
+/-!
+# Relations holding pairwise
+
+This file defines pairwise relations.
+
+## Main declarations
+
+* `pairwise`: `pairwise r` states that `r i j` for all `i ≠ j`.
+* `set.pairwise`: `s.pairwise r` states that `r i j` for all `i ≠ j` with `i, j ∈ s`.
+-/
+
+open set function
+
+variables {α β γ ι ι' : Type*} {r p q : α → α → Prop}
+
+section pairwise
+variables {f g : ι → α} {s t u : set α} {a b : α}
+
+/-- A relation `r` holds pairwise if `r i j` for all `i ≠ j`. -/
+def pairwise (r : α → α → Prop) := ∀ ⦃i j⦄, i ≠ j → r i j
+
+lemma pairwise.mono (hr : pairwise r) (h : ∀ ⦃i j⦄, r i j → p i j) : pairwise p :=
+λ i j hij, h $ hr hij
+
+protected lemma pairwise.eq (h : pairwise r) : ¬ r a b → a = b := not_imp_comm.1 $ @h _ _
+
+lemma function.injective_iff_pairwise_ne : injective f ↔ pairwise ((≠) on f) :=
+forall₂_congr $ λ i j, not_imp_not.symm
+
+alias function.injective_iff_pairwise_ne ↔ function.injective.pairwise_ne _
+
+namespace set
+
+/-- The relation `r` holds pairwise on the set `s` if `r x y` for all *distinct* `x y ∈ s`. -/
+protected def pairwise (s : set α) (r : α → α → Prop) := ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → r x y
+
+lemma pairwise_of_forall (s : set α) (r : α → α → Prop) (h : ∀ a b, r a b) : s.pairwise r :=
+λ a _ b _ _, h a b
+
+lemma pairwise.imp_on (h : s.pairwise r) (hrp : s.pairwise (λ ⦃a b : α⦄, r a b → p a b)) :
+  s.pairwise p :=
+λ a ha b hb hab, hrp ha hb hab $ h ha hb hab
+
+lemma pairwise.imp (h : s.pairwise r) (hpq : ∀ ⦃a b : α⦄, r a b → p a b) : s.pairwise p :=
+h.imp_on $ pairwise_of_forall s _ hpq
+
+protected lemma pairwise.eq (hs : s.pairwise r) (ha : a ∈ s) (hb : b ∈ s) (h : ¬ r a b) : a = b :=
+of_not_not $ λ hab, h $ hs ha hb hab
+
+lemma _root_.reflexive.set_pairwise_iff (hr : reflexive r) :
+  s.pairwise r ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b :=
+forall₄_congr $ λ a _ b _, or_iff_not_imp_left.symm.trans $ or_iff_right_of_imp $ eq.rec $ hr a
+
+lemma pairwise.on_injective (hs : s.pairwise r) (hf : function.injective f)
+  (hfs : ∀ x, f x ∈ s) :
+  pairwise (r on f) :=
+λ i j hij, hs (hfs i) (hfs j) (hf.ne hij)
+
+end set
+
+lemma pairwise.set_pairwise (h : pairwise r) (s : set α) : s.pairwise r := λ x hx y hy w, h w
+
+end pairwise
diff --git a/src/logic/small.lean b/src/logic/small/basic.lean
similarity index 92%
rename from src/logic/small.lean
rename to src/logic/small/basic.lean
index ae110d8e29457..5fde86ccdf39f 100644
--- a/src/logic/small.lean
+++ b/src/logic/small/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import data.vector.basic
+import logic.equiv.set
 
 /-!
 # Small types
@@ -132,15 +132,5 @@ theorem not_small_type : ¬ small.{u} (Type (max u v))
   (λ a, ⟨_, cast (e.3 _).symm a⟩)
   (λ a b e, (cast_inj _).1 $ eq_of_heq (sigma.mk.inj e).2)
 
-instance small_vector {α : Type v} {n : ℕ} [small.{u} α] :
-  small.{u} (vector α n) :=
-small_of_injective (equiv.vector_equiv_fin α n).injective
-
-instance small_list {α : Type v} [small.{u} α] :
-  small.{u} (list α) :=
-begin
-  let e : (Σ n, vector α n) ≃ list α := equiv.sigma_fiber_equiv list.length,
-  exact small_of_surjective e.surjective,
-end
 
 end
diff --git a/src/logic/small/list.lean b/src/logic/small/list.lean
new file mode 100644
index 0000000000000..eb668f3dcb118
--- /dev/null
+++ b/src/logic/small/list.lean
@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import logic.small.basic
+import data.vector.basic
+
+/-!
+# Instances for `small (list α)` and `small (vector α)`.
+
+These must not be in `logic.small.basic` as this is very low in the import hierarchy,
+and is used by category theory files which do not need everything imported by `data.vector.basic`.
+-/
+
+universes u v
+
+instance small_vector {α : Type v} {n : ℕ} [small.{u} α] :
+  small.{u} (vector α n) :=
+small_of_injective (equiv.vector_equiv_fin α n).injective
+
+instance small_list {α : Type v} [small.{u} α] :
+  small.{u} (list α) :=
+begin
+  let e : (Σ n, vector α n) ≃ list α := equiv.sigma_fiber_equiv list.length,
+  exact small_of_surjective e.surjective,
+end
diff --git a/src/model_theory/basic.lean b/src/model_theory/basic.lean
index 8cfc16ffd5ae2..179c579c5b429 100644
--- a/src/model_theory/basic.lean
+++ b/src/model_theory/basic.lean
@@ -7,7 +7,7 @@ import category_theory.concrete_category.bundled
 import data.fin.tuple.basic
 import data.fin.vec_notation
 import logic.encodable.basic
-import logic.small
+import logic.small.list
 import set_theory.cardinal.basic
 
 
diff --git a/src/number_theory/ADE_inequality.lean b/src/number_theory/ADE_inequality.lean
index a0e005f382dc4..67760b10cddb9 100644
--- a/src/number_theory/ADE_inequality.lean
+++ b/src/number_theory/ADE_inequality.lean
@@ -7,7 +7,7 @@ Authors: Johan Commelin
 import data.multiset.sort
 import data.pnat.interval
 import data.rat.order
-
+import data.pnat.basic
 import tactic.norm_num
 import tactic.field_simp
 import tactic.interval_cases
diff --git a/src/number_theory/lucas_lehmer.lean b/src/number_theory/lucas_lehmer.lean
index 788f96290d363..e386565478866 100644
--- a/src/number_theory/lucas_lehmer.lean
+++ b/src/number_theory/lucas_lehmer.lean
@@ -313,7 +313,7 @@ Here and below, we introduce `p' = p - 2`, in order to avoid using subtraction i
 lemma two_lt_q (p' : ℕ) : 2 < q (p'+2) := begin
   by_contradiction H,
   simp at H,
-  interval_cases q (p'+2); clear H,
+  interval_cases q (p'+2), clear H,
   { -- If q = 1, we get a contradiction from 2^p = 2
     dsimp [q] at h, injection h with h', clear h,
     simp [mersenne] at h',
diff --git a/src/order/atoms.lean b/src/order/atoms.lean
index 76cd3550aa72d..47c58ab24b0bf 100644
--- a/src/order/atoms.lean
+++ b/src/order/atoms.lean
@@ -3,11 +3,8 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-
-import order.complete_boolean_algebra
-import order.cover
+import data.set.finite
 import order.modular_lattice
-import data.fintype.basic
 
 /-!
 # Atoms, Coatoms, and Simple Lattices
diff --git a/src/order/basic.lean b/src/order/basic.lean
index 86701491f0c81..dcd08337c5d9b 100644
--- a/src/order/basic.lean
+++ b/src/order/basic.lean
@@ -731,7 +731,7 @@ end prod
 
 /-! ### Additional order classes -/
 
-/-- An order is dense if there is an element between any pair of distinct elements. -/
+/-- An order is dense if there is an element between any pair of distinct comparable elements. -/
 class densely_ordered (α : Type u) [has_lt α] : Prop :=
 (dense : ∀ a₁ a₂ : α, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂)
 
diff --git a/src/order/bounds.lean b/src/order/bounds/basic.lean
similarity index 95%
rename from src/order/bounds.lean
rename to src/order/bounds/basic.lean
index b1a2e3681b28f..2a2cadf45ab66 100644
--- a/src/order/bounds.lean
+++ b/src/order/bounds/basic.lean
@@ -804,30 +804,7 @@ in ⟨c, hcs, hac.lt_of_ne $ λ hac, h' $ hac.symm ▸ hcs, hcb⟩
 
 end linear_order
 
-/-!
-### Least upper bound and the greatest lower bound in linear ordered additive commutative groups
--/
-
-section linear_ordered_add_comm_group
-
-variables [linear_ordered_add_comm_group α] {s : set α} {a ε : α}
-
-lemma is_glb.exists_between_self_add (h : is_glb s a) (hε : 0 < ε) :
-  ∃ b ∈ s, a ≤ b ∧ b < a + ε :=
-h.exists_between $ lt_add_of_pos_right _ hε
-
-lemma is_glb.exists_between_self_add' (h : is_glb s a) (h₂ : a ∉ s) (hε : 0 < ε) :
-  ∃ b ∈ s, a < b ∧ b < a + ε :=
-h.exists_between' h₂ $ lt_add_of_pos_right _ hε
 
-lemma is_lub.exists_between_sub_self  (h : is_lub s a) (hε : 0 < ε) : ∃ b ∈ s, a - ε < b ∧ b ≤ a :=
-h.exists_between $ sub_lt_self _ hε
-
-lemma is_lub.exists_between_sub_self' (h : is_lub s a) (h₂ : a ∉ s) (hε : 0 < ε) :
-  ∃ b ∈ s, a - ε < b ∧ b < a :=
-h.exists_between' h₂ $ sub_lt_self _ hε
-
-end linear_ordered_add_comm_group
 
 /-!
 ### Images of upper/lower bounds under monotone functions
@@ -1209,51 +1186,3 @@ end
 lemma is_glb_prod [preorder α] [preorder β] {s : set (α × β)} (p : α × β) :
   is_glb s p ↔ is_glb (prod.fst '' s) p.1 ∧ is_glb (prod.snd '' s) p.2 :=
 @is_lub_prod αᵒᵈ βᵒᵈ _ _ _ _
-
-namespace order_iso
-
-variables [preorder α] [preorder β] (f : α ≃o β)
-
-lemma upper_bounds_image {s : set α} :
-  upper_bounds (f '' s) = f '' upper_bounds s :=
-subset.antisymm
-  (λ x hx, ⟨f.symm x, λ y hy, f.le_symm_apply.2 (hx $ mem_image_of_mem _ hy), f.apply_symm_apply x⟩)
-  f.monotone.image_upper_bounds_subset_upper_bounds_image
-
-lemma lower_bounds_image {s : set α} : lower_bounds (f '' s) = f '' lower_bounds s :=
-@upper_bounds_image αᵒᵈ βᵒᵈ _ _ f.dual _
-
-@[simp] lemma is_lub_image {s : set α} {x : β} :
-  is_lub (f '' s) x ↔ is_lub s (f.symm x) :=
-⟨λ h, is_lub.of_image (λ _ _, f.le_iff_le) ((f.apply_symm_apply x).symm ▸ h),
-  λ h, is_lub.of_image (λ _ _, f.symm.le_iff_le) $ (f.symm_image_image s).symm ▸ h⟩
-
-lemma is_lub_image' {s : set α} {x : α} :
-  is_lub (f '' s) (f x) ↔ is_lub s x :=
-by rw [is_lub_image, f.symm_apply_apply]
-
-@[simp] lemma is_glb_image {s : set α} {x : β} :
-  is_glb (f '' s) x ↔ is_glb s (f.symm x) :=
-f.dual.is_lub_image
-
-lemma is_glb_image' {s : set α} {x : α} :
-  is_glb (f '' s) (f x) ↔ is_glb s x :=
-f.dual.is_lub_image'
-
-@[simp] lemma is_lub_preimage {s : set β} {x : α} :
-  is_lub (f ⁻¹' s) x ↔ is_lub s (f x) :=
-by rw [← f.symm_symm, ← image_eq_preimage, is_lub_image]
-
-lemma is_lub_preimage' {s : set β} {x : β} :
-  is_lub (f ⁻¹' s) (f.symm x) ↔ is_lub s x :=
-by rw [is_lub_preimage, f.apply_symm_apply]
-
-@[simp] lemma is_glb_preimage {s : set β} {x : α} :
-  is_glb (f ⁻¹' s) x ↔ is_glb s (f x) :=
-f.dual.is_lub_preimage
-
-lemma is_glb_preimage' {s : set β} {x : β} :
-  is_glb (f ⁻¹' s) (f.symm x) ↔ is_glb s x :=
-f.dual.is_lub_preimage'
-
-end order_iso
diff --git a/src/order/bounds/order_iso.lean b/src/order/bounds/order_iso.lean
new file mode 100644
index 0000000000000..85357d9106e25
--- /dev/null
+++ b/src/order/bounds/order_iso.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Yury Kudryashov
+-/
+import order.bounds.basic
+import order.hom.basic
+
+/-!
+# Order isomorhpisms and bounds.
+-/
+
+variables {α β : Type*}
+open set
+
+namespace order_iso
+
+variables [preorder α] [preorder β] (f : α ≃o β)
+
+lemma upper_bounds_image {s : set α} :
+  upper_bounds (f '' s) = f '' upper_bounds s :=
+subset.antisymm
+  (λ x hx, ⟨f.symm x, λ y hy, f.le_symm_apply.2 (hx $ mem_image_of_mem _ hy), f.apply_symm_apply x⟩)
+  f.monotone.image_upper_bounds_subset_upper_bounds_image
+
+lemma lower_bounds_image {s : set α} : lower_bounds (f '' s) = f '' lower_bounds s :=
+@upper_bounds_image αᵒᵈ βᵒᵈ _ _ f.dual _
+
+@[simp] lemma is_lub_image {s : set α} {x : β} :
+  is_lub (f '' s) x ↔ is_lub s (f.symm x) :=
+⟨λ h, is_lub.of_image (λ _ _, f.le_iff_le) ((f.apply_symm_apply x).symm ▸ h),
+  λ h, is_lub.of_image (λ _ _, f.symm.le_iff_le) $ (f.symm_image_image s).symm ▸ h⟩
+
+lemma is_lub_image' {s : set α} {x : α} :
+  is_lub (f '' s) (f x) ↔ is_lub s x :=
+by rw [is_lub_image, f.symm_apply_apply]
+
+@[simp] lemma is_glb_image {s : set α} {x : β} :
+  is_glb (f '' s) x ↔ is_glb s (f.symm x) :=
+f.dual.is_lub_image
+
+lemma is_glb_image' {s : set α} {x : α} :
+  is_glb (f '' s) (f x) ↔ is_glb s x :=
+f.dual.is_lub_image'
+
+@[simp] lemma is_lub_preimage {s : set β} {x : α} :
+  is_lub (f ⁻¹' s) x ↔ is_lub s (f x) :=
+by rw [← f.symm_symm, ← image_eq_preimage, is_lub_image]
+
+lemma is_lub_preimage' {s : set β} {x : β} :
+  is_lub (f ⁻¹' s) (f.symm x) ↔ is_lub s x :=
+by rw [is_lub_preimage, f.apply_symm_apply]
+
+@[simp] lemma is_glb_preimage {s : set β} {x : α} :
+  is_glb (f ⁻¹' s) x ↔ is_glb s (f x) :=
+f.dual.is_lub_preimage
+
+lemma is_glb_preimage' {s : set β} {x : β} :
+  is_glb (f ⁻¹' s) (f.symm x) ↔ is_glb s x :=
+f.dual.is_lub_preimage'
+
+end order_iso
diff --git a/src/order/compactly_generated.lean b/src/order/compactly_generated.lean
index 47a3120645fbd..6de1bfbc724d3 100644
--- a/src/order/compactly_generated.lean
+++ b/src/order/compactly_generated.lean
@@ -10,6 +10,7 @@ import order.sup_indep
 import order.zorn
 import data.finset.order
 import data.finite.default
+import data.set.intervals.order_iso
 
 /-!
 # Compactness properties for complete lattices
diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean
index 83817a54446ad..16b65fee1bb3d 100644
--- a/src/order/complete_lattice.lean
+++ b/src/order/complete_lattice.lean
@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import data.bool.set
-import data.ulift
 import data.nat.set
-import order.bounds
+import data.ulift
+import order.bounds.basic
+import order.hom.basic
 
 /-!
 # Theory of complete lattices
diff --git a/src/order/conditionally_complete_lattice.lean b/src/order/conditionally_complete_lattice.lean
index 53908b91df6c0..51265fad68977 100644
--- a/src/order/conditionally_complete_lattice.lean
+++ b/src/order/conditionally_complete_lattice.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import order.bounds
+import order.bounds.basic
 import data.set.intervals.basic
 import data.set.finite
 import data.set.lattice
diff --git a/src/order/filter/at_top_bot.lean b/src/order/filter/at_top_bot.lean
index 729fe4138614d..7eb8d3a73b9a6 100644
--- a/src/order/filter/at_top_bot.lean
+++ b/src/order/filter/at_top_bot.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov, Patrick Massot
 import algebra.order.field.basic
 import data.finset.preimage
 import data.set.intervals.disjoint
+import data.set.intervals.order_iso
 import order.filter.bases
 
 /-!
diff --git a/src/order/lattice_intervals.lean b/src/order/lattice_intervals.lean
index 48e4b07455219..e26b862a81131 100644
--- a/src/order/lattice_intervals.lean
+++ b/src/order/lattice_intervals.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 
-import order.bounds
+import order.bounds.basic
 
 /-!
 # Intervals in Lattices
diff --git a/src/order/semiconj_Sup.lean b/src/order/semiconj_Sup.lean
index 12f70d69ab22b..7d3148c8c3842 100644
--- a/src/order/semiconj_Sup.lean
+++ b/src/order/semiconj_Sup.lean
@@ -5,6 +5,7 @@ Authors: Yury G. Kudryashov
 -/
 import algebra.hom.equiv
 import logic.function.conjugate
+import order.bounds.order_iso
 import order.conditionally_complete_lattice
 import order.ord_continuous
 
diff --git a/src/order/succ_pred/interval_succ.lean b/src/order/succ_pred/interval_succ.lean
index 82d875a0264c8..b3c9786f5f910 100644
--- a/src/order/succ_pred/interval_succ.lean
+++ b/src/order/succ_pred/interval_succ.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import data.set.pairwise
 import order.succ_pred.basic
-import data.set.lattice
 
 /-!
 # Intervals `Ixx (f x) (f (order.succ x))`
diff --git a/src/order/upper_lower.lean b/src/order/upper_lower.lean
index f8128d480dcfe..74881aa190911 100644
--- a/src/order/upper_lower.lean
+++ b/src/order/upper_lower.lean
@@ -5,6 +5,7 @@ Authors: Yaël Dillies, Sara Rousta
 -/
 import data.set_like.basic
 import data.set.intervals.ord_connected
+import data.set.intervals.order_iso
 import order.hom.complete_lattice
 
 /-!
diff --git a/src/ring_theory/hahn_series.lean b/src/ring_theory/hahn_series.lean
index 48c1531c5bc67..d4465f9599bb7 100644
--- a/src/ring_theory/hahn_series.lean
+++ b/src/ring_theory/hahn_series.lean
@@ -10,6 +10,7 @@ import algebra.module.pi
 import ring_theory.power_series.basic
 import data.finsupp.pwo
 import data.finset.mul_antidiagonal
+import algebra.order.group.with_top
 
 /-!
 # Hahn Series
diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean
index c7c9bc542e541..d5c3798e5c1ff 100644
--- a/src/set_theory/cardinal/basic.lean
+++ b/src/set_theory/cardinal/basic.lean
@@ -7,7 +7,7 @@ import data.fintype.card
 import data.finsupp.defs
 import data.nat.part_enat
 import data.set.countable
-import logic.small
+import logic.small.basic
 import order.conditionally_complete_lattice
 import order.succ_pred.basic
 import set_theory.cardinal.schroeder_bernstein
diff --git a/src/set_theory/zfc/basic.lean b/src/set_theory/zfc/basic.lean
index 00a3d2406577e..2c38bbbcc4d59 100644
--- a/src/set_theory/zfc/basic.lean
+++ b/src/set_theory/zfc/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.set.lattice
-import logic.small
+import logic.small.basic
 import order.well_founded
 
 /-!
diff --git a/src/tactic/interval_cases.lean b/src/tactic/interval_cases.lean
index d923e76a6d4bc..9cffa15e8d41a 100644
--- a/src/tactic/interval_cases.lean
+++ b/src/tactic/interval_cases.lean
@@ -7,6 +7,7 @@ import tactic.fin_cases
 import data.fin.interval -- These imports aren't required to compile this file,
 import data.int.interval -- but they are needed at the use site for the tactic to work
 import data.pnat.interval -- (on values of type fin/int/pnat)
+import data.pnat.basic
 
 /-!
 # Case bash on variables in finite intervals
diff --git a/src/tactic/linarith/lemmas.lean b/src/tactic/linarith/lemmas.lean
index 83d7faf69ead9..391600f131e19 100644
--- a/src/tactic/linarith/lemmas.lean
+++ b/src/tactic/linarith/lemmas.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
 
-import algebra.order.ring
+import algebra.order.ring.basic
 
 /-!
 # Lemmas for `linarith`
diff --git a/src/tactic/monotonicity/lemmas.lean b/src/tactic/monotonicity/lemmas.lean
index 9f7be88c70997..470c17e7070dc 100644
--- a/src/tactic/monotonicity/lemmas.lean
+++ b/src/tactic/monotonicity/lemmas.lean
@@ -3,7 +3,9 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import algebra.order.ring
+import algebra.order.group.abs
+import algebra.order.ring.basic
+import algebra.order.sub.canonical
 import data.set.lattice
 import tactic.monotonicity.basic
 
diff --git a/src/testing/slim_check/sampleable.lean b/src/testing/slim_check/sampleable.lean
index 7db0718f158fd..347238d9241d3 100644
--- a/src/testing/slim_check/sampleable.lean
+++ b/src/testing/slim_check/sampleable.lean
@@ -5,6 +5,7 @@ Authors: Simon Hudon
 -/
 import data.lazy_list.basic
 import data.tree
+import data.pnat.basic
 import control.bifunctor
 import control.ulift
 import tactic.linarith
diff --git a/src/topology/algebra/order/basic.lean b/src/topology/algebra/order/basic.lean
index 9c9c30bb83588..2d3bae6a98bbe 100644
--- a/src/topology/algebra/order/basic.lean
+++ b/src/topology/algebra/order/basic.lean
@@ -3,14 +3,11 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 -/
-import algebra.group_with_zero.power
 import data.set.intervals.pi
+import data.set.pointwise.interval
 import order.filter.interval
 import topology.algebra.field
 import topology.algebra.order.left_right
-import tactic.linarith
-import tactic.tfae
-import tactic.positivity
 
 /-!
 # Theory of topology on ordered spaces
diff --git a/src/topology/instances/real.lean b/src/topology/instances/real.lean
index 74e29016255ff..e1d207f7f8e27 100644
--- a/src/topology/instances/real.lean
+++ b/src/topology/instances/real.lean
@@ -10,6 +10,7 @@ import topology.algebra.ring
 import topology.algebra.star
 import ring_theory.subring.basic
 import group_theory.archimedean
+import algebra.order.group.bounds
 import algebra.periodic
 import order.filter.archimedean
 import topology.instances.int
diff --git a/test/finish4.lean b/test/finish4.lean
index 3bc84021728a6..ed900d192fae7 100644
--- a/test/finish4.lean
+++ b/test/finish4.lean
@@ -7,7 +7,7 @@ Tests for `finish using [...]`
 -/
 
 import tactic.finish
-import algebra.order.ring
+import algebra.order.ring.basic
 
 section list_rev
 open list
diff --git a/test/library_search/ordered_ring.lean b/test/library_search/ordered_ring.lean
index f3df249637e19..fb33b229dabd6 100644
--- a/test/library_search/ordered_ring.lean
+++ b/test/library_search/ordered_ring.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import tactic.basic
 import data.nat.order
-import algebra.order.ring
+import algebra.order.ring.basic
 
 /- Turn off trace messages so they don't pollute the test build: -/
 set_option trace.silence_library_search true
diff --git a/test/monotonicity.lean b/test/monotonicity.lean
index d2bb7cd321199..1fc83c445a805 100644
--- a/test/monotonicity.lean
+++ b/test/monotonicity.lean
@@ -5,7 +5,7 @@ Authors: Simon Hudon
 -/
 import tactic.monotonicity
 import tactic.norm_num
-import algebra.order.ring
+import algebra.order.ring.basic
 import measure_theory.measure.lebesgue
 import measure_theory.function.locally_integrable
 import data.list.defs
diff --git a/test/nontriviality.lean b/test/nontriviality.lean
index 56a4d23f76ff6..7174ec3059737 100644
--- a/test/nontriviality.lean
+++ b/test/nontriviality.lean
@@ -1,5 +1,5 @@
 import logic.nontrivial
-import algebra.order.ring
+import algebra.order.ring.basic
 import data.nat.basic
 
 /-! ### Test `nontriviality` with inequality hypotheses -/
diff --git a/test/squeeze.lean b/test/squeeze.lean
index a6ce4fb352976..f2b9d01add632 100644
--- a/test/squeeze.lean
+++ b/test/squeeze.lean
@@ -1,5 +1,5 @@
 import data.nat.basic
-import data.pnat.basic
+import data.pnat.defs
 import tactic.squeeze
 
 namespace tactic