chore: split Data.Real.Basic (#8356)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Archive/Imo/Imo2005Q3.lean

@@ -5,6 +5,8 @@ Authors: Manuel Candales
 -/
 import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
 
 #align_import imo.imo2005_q3 from "leanprover-community/mathlib"@"308826471968962c6b59c7ff82a22757386603e3"
 

Archive/Imo/Imo2008Q2.lean

@@ -5,6 +5,9 @@ Authors: Manuel Candales
 -/
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Set.Finite
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Abel
+import Mathlib.Tactic.Linarith
 
 #align_import imo.imo2008_q2 from "leanprover-community/mathlib"@"5f25c089cb34db4db112556f23c50d12da81b297"
 

Archive/Imo/Imo2011Q3.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Renshaw
 -/
 import Mathlib.Data.Real.Basic
+import Mathlib.Tactic.Linarith
 
 #align_import imo.imo2011_q3 from "leanprover-community/mathlib"@"5f25c089cb34db4db112556f23c50d12da81b297"
 
@@ -57,4 +58,3 @@ theorem imo2011_q3 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) ≤ y * f x + f (f
     rw [hno] at hp
     linarith
 #align imo2011_q3 imo2011_q3
-

Archive/Imo/Imo2013Q5.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Renshaw
 -/
 import Mathlib.Algebra.GeomSum
-import Mathlib.Data.Rat.Defs
-import Mathlib.Data.Real.Basic
+import Mathlib.Data.Real.Archimedean
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.LinearCombination
 

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -6,6 +6,7 @@ Authors: Floris van Doorn
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Set.Finite
 import Mathlib.Data.Set.Intervals.Disjoint
+import Mathlib.Data.Set.Intervals.Group
 
 #align_import wiedijk_100_theorems.cubing_a_cube from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"
 

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -5,6 +5,7 @@ Authors: Jalex Stark, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Data.Real.Basic
+import Mathlib.Tactic.FieldSimp
 
 #align_import wiedijk_100_theorems.inverse_triangle_sum from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"
 

Mathlib.lean

@@ -1834,6 +1834,7 @@ import Mathlib.Data.Rbtree.Init
 import Mathlib.Data.Rbtree.Insert
 import Mathlib.Data.Rbtree.Main
 import Mathlib.Data.Rbtree.MinMax
+import Mathlib.Data.Real.Archimedean
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.Cardinality
 import Mathlib.Data.Real.CauSeq

Mathlib/Analysis/Convex/Cone/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Frédéric Dupuis
 -/
 import Mathlib.Analysis.Convex.Hull
-import Mathlib.Data.Real.Basic
+import Mathlib.Data.Real.Archimedean
 import Mathlib.LinearAlgebra.LinearPMap
 
 #align_import analysis.convex.cone.basic from "leanprover-community/mathlib"@"915591b2bb3ea303648db07284a161a7f2a9e3d4"