chore(Topology/Instances/Real): reduce imports

[YaelDillies]

---

[github-actions]

PR summary 93f3fefd61

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Instances.Real	1177	1173	-4 (-0.34%)

Import changes for all files

Files	Import difference
157 files Mathlib.Data.Real.Hyperreal Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.Probability.Kernel.Defs Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Topology.MetricSpace.Thickening Mathlib.Analysis.Subadditive Mathlib.Topology.Homotopy.Contractible Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.Data.Real.GoldenRatio Mathlib.MeasureTheory.Order.Lattice Mathlib.Analysis.Hofer Mathlib.Analysis.Convex.Topology Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.Topology.Instances.CantorSet Mathlib.Data.Real.Sqrt Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Group.Arithmetic Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Category.MeasCat Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.Dynamics.Ergodic.Conservative Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Topology.Order.Bounded Mathlib.Topology.Homotopy.Path Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.Data.Complex.Exponential Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.MeasureTheory.Measure.Content Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.Topology.Homotopy.Basic Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.MeasureTheory.Measure.Sub Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.Real Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.Kernel.Composition.Basic Mathlib.NumberTheory.Rayleigh Mathlib.AlgebraicTopology.SingularSet Mathlib.Probability.Kernel.Proper Mathlib.MeasureTheory.Measure.Trim Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.Analysis.SumOverResidueClass Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.Topology.MetricSpace.Polish Mathlib.Topology.Instances.Rat Mathlib.Probability.Kernel.Invariance Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Data.Real.CompleteField Mathlib.MeasureTheory.Group.Pointwise Mathlib.Data.Real.Irrational Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Algebra.Star.CHSH Mathlib.Probability.ConditionalProbability Mathlib.Order.Filter.ENNReal Mathlib.Data.Complex.FiniteDimensional Mathlib.Topology.UnitInterval Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Data.Real.StarOrdered Mathlib.MeasureTheory.Measure.Count Mathlib.Probability.Kernel.Basic Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Measure.Comap Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.Topology.MetricSpace.Contracting Mathlib.Data.Complex.Cardinality Mathlib.Topology.Baire.BaireMeasurable Mathlib.Analysis.Convex.Contractible Mathlib.MeasureTheory.Group.Convolution Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Topology.MetricSpace.Perfect Mathlib.Topology.Connected.PathConnected Mathlib.Dynamics.Ergodic.Ergodic Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Dirac Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.NumberTheory.Pell Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.Topology.MetricSpace.PiNat Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Topology.Instances.EReal Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Data.Complex.Order Mathlib.Probability.Independence.Basic Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Topology.MetricSpace.CantorScheme Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.Topology.Instances.Irrational Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Data.Real.Cardinality Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.Topology.Instances.RealVectorSpace Mathlib.MeasureTheory.Measure.Restrict Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.Probability.Independence.Kernel Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.MeasureTheory.Measure.Prod Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.Data.Complex.Abs Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.MeasureTheory.Constructions.Projective Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Instances.NNReal Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Integral.Indicator Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Topology.MetricSpace.Closeds Mathlib.Topology.Semicontinuous Mathlib.Analysis.SpecificLimits.Basic Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.MeasureTheory.Function.Floor Mathlib.Probability.UniformOn Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.Topology.Baire.CompleteMetrizable Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Group.Defs Mathlib.Topology.Instances.ENNReal Mathlib.Topology.Instances.RatLemmas Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.MeasureTheory.OuterMeasure.BorelCantelli	-4
40 files Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.AlgebraicGeometry.PrimeSpectrum.FreeLocus Mathlib.Topology.Instances.ZMultiples Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.RingTheory.Flat.Localization Mathlib.Topology.Instances.AddCircle Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.RingTheory.Etale.Field Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.AlgebraicGeometry.RationalMap Mathlib.FieldTheory.LinearDisjoint Mathlib.LinearAlgebra.LinearDisjoint Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.Algebra.Module.CharacterModule Mathlib.Topology.EMetricSpace.BoundedVariation Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Analysis.Convex.TotallyBounded Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Flat.Equalizer Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.RingTheory.Flat.Stability Mathlib.Algebra.Category.Grp.Injective Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.RingTheory.Unramified.Finite	-3
Mathlib.Topology.UniformSpace.CompareReals	-1

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

I'm not really convinced by this; it's only four files, and proving mul lemmas using smul is a standard and useful trick.

Maybe @urkud disagrees.