From 32965b55ceace6c3f6a9e0dfb549dd1cf6fec74c Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 6 Feb 2023 01:55:09 +0000
Subject: [PATCH] feat: port Topology.Algebra.Order.Archimedean (#2083)

---
 Mathlib.lean                                  |  1 +
 .../Topology/Algebra/Order/Archimedean.lean   | 29 +++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 Mathlib/Topology/Algebra/Order/Archimedean.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 01de326a35665..68ae97b2cc344 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -974,6 +974,7 @@ import Mathlib.Testing.SlimCheck.Sampleable
 import Mathlib.Testing.SlimCheck.Testable
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions
+import Mathlib.Topology.Algebra.Order.Archimedean
 import Mathlib.Topology.Algebra.Order.LeftRight
 import Mathlib.Topology.Bases
 import Mathlib.Topology.Basic
diff --git a/Mathlib/Topology/Algebra/Order/Archimedean.lean b/Mathlib/Topology/Algebra/Order/Archimedean.lean
new file mode 100644
index 0000000000000..1f128c2dbb2e4
--- /dev/null
+++ b/Mathlib/Topology/Algebra/Order/Archimedean.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2022 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury G. Kudryashov
+
+! This file was ported from Lean 3 source module topology.algebra.order.archimedean
+! leanprover-community/mathlib commit 4c19a16e4b705bf135cf9a80ac18fcc99c438514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Order.Basic
+import Mathlib.Algebra.Order.Archimedean
+
+/-!
+# Rational numbers are dense in a linear ordered archimedean field
+
+In this file we prove that coercion from `ℚ` to a linear ordered archimedean field has dense range.
+This lemma is in a separate file because `Mathlib.Topology.Order.Basic` does not import
+`Mathlib.Algebra.Order.Archimedean`.
+-/
+
+
+variable {𝕜 : Type _} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [Archimedean 𝕜]
+
+/-- Rational numbers are dense in a linear ordered archimedean field. -/
+theorem Rat.denseRange_cast : DenseRange ((↑) : ℚ → 𝕜) :=
+  dense_of_exists_between fun _ _ h => Set.exists_range_iff.2 <| exists_rat_btwn h
+#align rat.dense_range_cast Rat.denseRange_cast
+