[Merged by Bors] - fix(Topology/Metrizable/CompletelyMetrizable): make instances anonymous to avoid name collisions

[justin-palumbo]

Drop instance names TopologicalSpace.IsCompletelyPseudoMetrizableSpace.{Pseudo,}MetrizableSpace. The current names violate naming convention, and can cause confusing errors (as this shadows the e.g. MetrizableSpace class).

---

Why? As named, each instance shadows the class it produces --- any declaration in IsCompletelyMetrizableSpace resolves MetrizableSpace to the instance rather than the type, when the type is going to always be what is intended.

I discovered this while trying to add a proof that all CompletelyMetrizable subspaces of a Metrizable space are G\delta - the signature

theorem TopologicalSpace.IsCompletelyMetrizableSpace.isGδ
{X : Type*} [TopologicalSpace X] [MetrizableSpace X] {s : Set X}
(hs : IsCompletelyMetrizableSpace s) : IsGδ s

caused an error, because MetrizableSpace was interpreted as the instance (which takes no parameters) rather than the type MetrizableSpace.

The updated naming matches convention already used for other such instances as in Mathlib/Topology/Metrizable/Basic.lean

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 3be9846100

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ instance (priority := 90) [TopologicalSpace X]
+ instance (priority := 90) [TopologicalSpace X] [IsCompletelyMetrizableSpace X] :
- instance (priority := 90) MetrizableSpace [TopologicalSpace X] [IsCompletelyMetrizableSpace X] :
- instance (priority := 90) PseudoMetrizableSpace [TopologicalSpace X]

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 3be9846).

• +2 new declarations
• −2 removed declarations

-TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace
+TopologicalSpace.IsCompletelyMetrizableSpace.instMetrizableSpace
-TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace
+TopologicalSpace.IsCompletelyPseudoMetrizableSpace.instPseudoMetrizableSpace

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 3be9846100
Reference commit 618f225e1f

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[CoolRmal]

The name change does make sense to me, but for the theorem you want to prove you should instead write:

theorem TopologicalSpace.IsCompletelyMetrizableSpace.isGδ
    {X : Type*} [TopologicalSpace X] [IsCompletelyMetrizableSpace X] {s : Set X} : 
    IsGδ s := by 
  sorry

I am also not sure about deprecations. These two instances are rarely used so I guess it is fine to skip deprecations. I'll ask a maintainer to decide on it.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by CoolRmal.

[CoolRmal]

easy

[plp127]

The name change does make sense to me, but for the theorem you want to prove you should instead write:

theorem TopologicalSpace.IsCompletelyMetrizableSpace.isGδ
    {X : Type*} [TopologicalSpace X] [IsCompletelyMetrizableSpace X] {s : Set X} : 
    IsGδ s := by 
  sorry

But this theorem is false? Not every subset of a completely metrizable space is G-delta. For example, the rational numbers are not G-delta in the reals.

[CoolRmal]

Oh sorry I think I see what the original author mean. You are completely correct. In that case maybe we should refactor these files so that we can have both IsCompletelyMetrizable (as a function Set X → Prop) and CompletelyMetrizableSpace (similar to the APIs of IsCompact and CompactSpace).

[justin-palumbo]

Oh sorry I think I see what the original author mean.

Ah sorry, yes, reading again now I realize the initial description wasn't clear enough --- said more clearly, the theorem (often called Alexandrov's theorem in Descriptive Set Theory circles) is: given a metrizable space S, any completely metrizable subspace s is Gdelta as a subset of X. (Updated the description to make that clearer I hope)

FWIW that is up now as a PR #42912

[grunweg]

Renaming named instances doesn't need a deprecation warning (as mathlib's policy mentions: https://leanprover-community.github.io/contribute/style.html#deprecation) - that part is fine.

Thanks for the PR, this looks good. I'm not 100% sure if the correct name is of the form "instFoo" or "toFoo" here: let me defer to another maintainer. I do think the PR description is a bit verbose; I have edited it to be more concise. (Everything below the "----" line is not part of the eventual commit message.)
maintainer merge?

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[EtienneC30]

I thought we didn't want named instances, so these should not be named.

[sgouezel]

I agree that there is no reason to name these instances. Can you just remove the name?

[justin-palumbo]

Took the advice and dropped the instance names altogether -- updated title and description correspondingly

[sgouezel]

bors r+
Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Test and lint
• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job