From e11285628f402b32a4675d1af116961c69238510 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 1 Nov 2022 13:13:52 +0000
Subject: [PATCH] feat(algebra/order/field): Uniform bound in pi types (#16971)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

If `x` is less than `y` in all dimensions, we can find `ε > 0` such that `∀ i, x i + ε < y i`.
---
 src/algebra/order/field.lean            | 16 ++++++++++-
 src/algebra/order/monoid/canonical.lean |  9 +++++++
 src/algebra/order/monoid/lemmas.lean    | 36 +++++++++++++++++++++++++
 3 files changed, 60 insertions(+), 1 deletion(-)

diff --git a/src/algebra/order/field.lean b/src/algebra/order/field.lean
index 84b6bc911076e..85b3a72e45127 100644
--- a/src/algebra/order/field.lean
+++ b/src/algebra/order/field.lean
@@ -5,6 +5,7 @@ Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
 import algebra.order.field_defs
 import algebra.order.with_zero
+import data.fintype.basic
 
 /-!
 # Linear ordered (semi)fields
@@ -24,7 +25,7 @@ set_option old_structure_cmd true
 
 open function order_dual
 
-variables {α β : Type*}
+variables {ι α β : Type*}
 
 namespace function
 
@@ -634,6 +635,19 @@ lemma is_glb.mul_right {s : set α} (ha : 0 ≤ a) (hs : is_glb s b) :
   is_glb ((λ b, b * a) '' s) (b * a) :=
 by simpa [mul_comm] using hs.mul_left ha
 
+lemma pi.exists_forall_pos_add_lt [has_exists_add_of_le α] [finite ι] {x y : ι → α}
+  (h : ∀ i, x i < y i) : ∃ ε, 0 < ε ∧ ∀ i, x i + ε < y i :=
+begin
+  casesI nonempty_fintype ι,
+  casesI is_empty_or_nonempty ι,
+  { exact ⟨1, zero_lt_one, is_empty_elim⟩ },
+  choose ε hε hxε using λ i, exists_pos_add_of_lt' (h i),
+  obtain rfl : x + ε = y := funext hxε,
+  have hε : 0 < finset.univ.inf' finset.univ_nonempty ε := (finset.lt_inf'_iff _).2 (λ i _, hε _),
+  exact ⟨_, half_pos hε, λ i, add_lt_add_left ((half_lt_self hε).trans_le $ finset.inf'_le _ $
+    finset.mem_univ _) _⟩,
+end
+
 end linear_ordered_semifield
 
 section
diff --git a/src/algebra/order/monoid/canonical.lean b/src/algebra/order/monoid/canonical.lean
index 9931cafb67783..f1c5e929055fa 100644
--- a/src/algebra/order/monoid/canonical.lean
+++ b/src/algebra/order/monoid/canonical.lean
@@ -33,6 +33,15 @@ export has_exists_mul_of_le (exists_mul_of_le)
 
 export has_exists_add_of_le (exists_add_of_le)
 
+section mul_one_class
+variables [mul_one_class α] [preorder α] [contravariant_class α α (*) (<)] [has_exists_mul_of_le α]
+  {a b : α}
+
+@[to_additive] lemma exists_one_lt_mul_of_lt' (h : a < b) : ∃ c, 1 < c ∧ a * c = b :=
+by { obtain ⟨c, rfl⟩ := exists_mul_of_le h.le, exact ⟨c, one_lt_of_lt_mul_right h, rfl⟩ }
+
+end mul_one_class
+
 section has_exists_mul_of_le
 variables [linear_order α] [densely_ordered α] [monoid α] [has_exists_mul_of_le α]
   [covariant_class α α (*) (<)] [contravariant_class α α (*) (<)] {a b : α}
diff --git a/src/algebra/order/monoid/lemmas.lean b/src/algebra/order/monoid/lemmas.lean
index c89f86faf4a00..37beb06d52e1c 100644
--- a/src/algebra/order/monoid/lemmas.lean
+++ b/src/algebra/order/monoid/lemmas.lean
@@ -271,6 +271,24 @@ lemma mul_le_of_le_one_left' [covariant_class α α (swap (*)) (≤)]
 calc  b * a ≤ 1 * a : mul_le_mul_right' h a
         ... = a     : one_mul a
 
+@[to_additive]
+lemma one_le_of_le_mul_right [contravariant_class α α (*) (≤)] {a b : α} (h : a ≤ a * b) : 1 ≤ b :=
+le_of_mul_le_mul_left' $ by simpa only [mul_one]
+
+@[to_additive]
+lemma le_one_of_mul_le_right [contravariant_class α α (*) (≤)] {a b : α} (h : a * b ≤ a) : b ≤ 1 :=
+le_of_mul_le_mul_left' $ by simpa only [mul_one]
+
+@[to_additive]
+lemma one_le_of_le_mul_left [contravariant_class α α (swap (*)) (≤)] {a b : α} (h : b ≤ a * b) :
+  1 ≤ a :=
+le_of_mul_le_mul_right' $ by simpa only [one_mul]
+
+@[to_additive]
+lemma le_one_of_mul_le_left [contravariant_class α α (swap (*)) (≤)] {a b : α} (h : a * b ≤ b) :
+  a ≤ 1 :=
+le_of_mul_le_mul_right' $ by simpa only [one_mul]
+
 @[simp, to_additive le_add_iff_nonneg_right]
 lemma le_mul_iff_one_le_right'
   [covariant_class α α (*) (≤)] [contravariant_class α α (*) (≤)]
@@ -332,6 +350,24 @@ lemma mul_lt_of_lt_one_left' [covariant_class α α (swap (*)) (<)]
 calc  b * a < 1 * a : mul_lt_mul_right' h a
         ... = a     : one_mul a
 
+@[to_additive]
+lemma one_lt_of_lt_mul_right [contravariant_class α α (*) (<)] {a b : α} (h : a < a * b) : 1 < b :=
+lt_of_mul_lt_mul_left' $ by simpa only [mul_one]
+
+@[to_additive]
+lemma lt_one_of_mul_lt_right [contravariant_class α α (*) (<)] {a b : α} (h : a * b < a) : b < 1 :=
+lt_of_mul_lt_mul_left' $ by simpa only [mul_one]
+
+@[to_additive]
+lemma one_lt_of_lt_mul_left [contravariant_class α α (swap (*)) (<)] {a b : α} (h : b < a * b) :
+  1 < a :=
+lt_of_mul_lt_mul_right' $ by simpa only [one_mul]
+
+@[to_additive]
+lemma lt_one_of_mul_lt_left [contravariant_class α α (swap (*)) (<)] {a b : α} (h : a * b < b) :
+  a < 1 :=
+lt_of_mul_lt_mul_right' $ by simpa only [one_mul]
+
 @[simp, to_additive lt_add_iff_pos_right]
 lemma lt_mul_iff_one_lt_right'
   [covariant_class α α (*) (<)] [contravariant_class α α (*) (<)]