feat(algebra/order/field): Uniform bound in pi types (#16971)

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

@@ -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

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 : α}

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 α α (*) (<)]