[Merged by Bors] - chore: splitting up metric spaces files

[kim-em]

No description provided.

[github-actions]

PR summary 2ec5e228ee

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Instances.Discrete	881	726	-155 (-17.59%)
Mathlib.Topology.MetricSpace.MetricSeparated	862	827	-35 (-4.06%)
Mathlib.Topology.MetricSpace.Pseudo.Defs	862	828	-34 (-3.94%)
Mathlib.Topology.MetricSpace.Pseudo.Lemmas	875	867	-8 (-0.91%)
Mathlib.Topology.MetricSpace.Pseudo.Constructions	864	858	-6 (-0.69%)
Mathlib.Topology.MetricSpace.Equicontinuity	881	875	-6 (-0.68%)
Mathlib.Analysis.Convex.Extrema	1058	1056	-2 (-0.19%)
Mathlib.Topology.MetricSpace.Cauchy	876	875	-1 (-0.11%)
Mathlib.Topology.Instances.Int	895	894	-1 (-0.11%)

Import changes for all files

Files	Import difference
There are 1048 files with changed transitive imports: this is too many to display!

---

Declarations diff

+ dist_le_of_mem_Icc
+ dist_le_of_mem_Icc_01
+ dist_le_of_mem_uIcc
+ dist_left_le_of_mem_uIcc
+ dist_right_le_of_mem_uIcc
+ instance (priority := 100) DiscreteTopology.metrizableSpace
+ instance [MetricSpace X] : MetricSpace (Additive X) := ‹MetricSpace X›
+ instance [MetricSpace X] : MetricSpace (Multiplicative X) := ‹MetricSpace X›
+ instance [MetricSpace X] : MetricSpace Xᵒᵈ := ‹MetricSpace X›
- Real.dist_le_of_mem_Icc
- Real.dist_le_of_mem_Icc_01
- Real.dist_le_of_mem_uIcc
- Real.dist_left_le_of_mem_uIcc
- Real.dist_right_le_of_mem_uIcc
- instance (priority := 100) DiscreteTopology.metrizableSpace [DiscreteTopology α] :
- instance : PseudoMetricSpace (Additive X) := ‹PseudoMetricSpace X›
- instance : PseudoMetricSpace (Multiplicative X) := ‹PseudoMetricSpace X›

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.

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[urkud]

Thanks! 🎉
bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style