feat(algebra/order/archimedean): Comparing with rationals determines …

…the order (#13602)

In a linear ordered field, if `q < x → q ≤ y` for all `q : ℚ`, then `x ≤ y`, and similar results.

src/algebra/order/archimedean.lean

@@ -284,7 +284,7 @@ archimedean_iff_rat_lt.trans
  λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
    lt_of_le_of_lt h (rat.cast_lt.2 (lt_add_one _))⟩⟩
 
-variable [archimedean α]
+variables [archimedean α] {x y : α}
 
 theorem exists_rat_lt (x : α) : ∃ q : ℚ, (q : α) < x :=
 let ⟨n, h⟩ := exists_int_lt x in ⟨n, by rwa rat.cast_coe_int⟩
@@ -308,6 +308,20 @@ begin
   { rw [rat.coe_nat_denom, nat.cast_one], exact one_ne_zero }
 end
 
+lemma le_of_forall_rat_lt_imp_le (h : ∀ q : ℚ, (q : α) < x → (q : α) ≤ y) : x ≤ y :=
+le_of_not_lt $ λ hyx, let ⟨q, hy, hx⟩ := exists_rat_btwn hyx in hy.not_le $ h _ hx
+
+lemma le_of_forall_lt_rat_imp_le (h : ∀ q : ℚ, y < q → x ≤ q) : x ≤ y :=
+le_of_not_lt $ λ hyx, let ⟨q, hy, hx⟩ := exists_rat_btwn hyx in hx.not_le $ h _ hy
+
+lemma eq_of_forall_rat_lt_iff_lt (h : ∀ q : ℚ, (q : α) < x ↔ (q : α) < y) : x = y :=
+(le_of_forall_rat_lt_imp_le $ λ q hq, ((h q).1 hq).le).antisymm $ le_of_forall_rat_lt_imp_le $
+  λ q hq, ((h q).2 hq).le
+
+lemma eq_of_forall_lt_rat_iff_lt (h : ∀ q : ℚ, x < q ↔ y < q) : x = y :=
+(le_of_forall_lt_rat_imp_le $ λ q hq, ((h q).2 hq).le).antisymm $ le_of_forall_lt_rat_imp_le $
+  λ q hq, ((h q).1 hq).le
+
 theorem exists_nat_one_div_lt {ε : α} (hε : 0 < ε) : ∃ n : ℕ, 1 / (n + 1: α) < ε :=
 begin
   cases exists_nat_gt (1/ε) with n hn,