chore: move Data.Rat.NatSqrt.Real to Analysis (leanprover-community#39976)

It's about the real square root; that's firmly within analysis.

Removing all transitive `Data` imports from `Analysis` will require moving certain basic files (such as `Data.String.Defs` to a new `Basic` directory).

Author: grunweg

Mathlib.lean

@@ -2284,6 +2284,7 @@ public import Mathlib.Analysis.RCLike.Inner
 public import Mathlib.Analysis.RCLike.Lemmas
 public import Mathlib.Analysis.RCLike.Sqrt
 public import Mathlib.Analysis.RCLike.TangentCone
+public import Mathlib.Analysis.Rat.NatSqrt.Real
 public import Mathlib.Analysis.Real.Cardinality
 public import Mathlib.Analysis.Real.Hyperreal
 public import Mathlib.Analysis.Real.OfDigits
@@ -4277,7 +4278,6 @@ public import Mathlib.Data.Rat.Floor
 public import Mathlib.Data.Rat.Init
 public import Mathlib.Data.Rat.Lemmas
 public import Mathlib.Data.Rat.NatSqrt.Defs
-public import Mathlib.Data.Rat.NatSqrt.Real
 public import Mathlib.Data.Rat.Sqrt
 public import Mathlib.Data.Rat.Star
 public import Mathlib.Data.Real.Basic

Mathlib/Data/Rat/NatSqrt/Real.lean Mathlib/Analysis/Rat/NatSqrt/Real.leanMathlib/Data/Rat/NatSqrt/Real.lean renamed to Mathlib/Analysis/Rat/NatSqrt/Real.lean

@@ -11,7 +11,7 @@ public import Mathlib.Algebra.Order.Field.Basic
 /-!
 Rational approximation of the square root of a natural number.
 
-See also `Mathlib.Data.Rat.NatSqrt.Real` for comparisons with the real square root.
+See also `Mathlib.Analysis.Rat.NatSqrt.Real` for comparisons with the real square root.
 -/
 
 @[expose] public section

Mathlib/Data/Rat/NatSqrt/Defs.lean

@@ -618,9 +618,6 @@ def overrideAllowedImportDirs : NamePrefixRel := .ofArray #[
   (`Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion, `Mathlib.AlgebraicTopology),
   (`Mathlib.Probability.Kernel.Category, `Mathlib.CategoryTheory), -- For the category of s-finite/Markov kernels
   (`Mathlib.RepresentationTheory.Continuous, `Mathlib.Topology), -- For continuous representations
-
-  -- TODO: reduce these with further moving files out of `Data`
-  (`Mathlib.Data.Rat.NatSqrt.Real, `Mathlib.Analysis),
   -- TODO: think about the role of Analysis and Algebra, and perhaps further separation
   (`Mathlib.Algebra.Order.Archimedean.Real, `Mathlib.Analysis),
   (`Mathlib.Algebra.Star.CHSH, `Mathlib.Analysis),

Mathlib/Tactic/Linter/DirectoryDependency.lean

@@ -1,6 +1,6 @@
 import Mathlib.Tactic.Eval
 import Mathlib.Tactic.NormNum.NatSqrt
-import Mathlib.Data.Rat.NatSqrt.Real
+import Mathlib.Analysis.Rat.NatSqrt.Real
 
 open Nat