fix(Geometry/Manifold): restore the Hausdorff hypothesis in NonemptyDiffeomorphSphere

[Deicyde]

ContinuousMap.HomotopyEquiv.NonemptyDiffeomorphSphere M n (the smooth Poincaré conjecture for M in dimension n) has no Hausdorff hypothesis. As stated it is false in every positive dimension. One can construct a non-Hausdorff counter-example by taking 𝕊ⁿ as the one-point compactification of ℝⁿ and glue a second copy of the open half-space B = {x₀ < 1} onto 𝕊ⁿ along the smaller open half-space A = {x₀ < 0}.

A Lean proof of ¬ NonemptyDiffeomorphSphere M (n + 1) for this M compiles against Mathlib.

The variable-inclusion backport #15607 removed [T2Space M] from the variable line and added it to each proof_wanted in the file, but not to this def, which silently lost it.

---

comparator

[github-actions]

PR summary 915b9d6803

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

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

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 915b9d6).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 915b9d6803
Reference commit f6734f8e47

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.py 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).

[grunweg]

Nice catch, thanks! (And using comparator is great :-)) You need to fix a linter failure, otherwise this looks good to me!
bors d+

[mathlib-bors]

✌️ Deicyde can now approve this pull request until 2026-09-23 10:22 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, Wanted/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean, Wanted.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

[grunweg]

Aside, looking at the formalisation:

• mathlib already has pullbackChartedSpace -- is there missing API that it should gain? (I'd happily review such a PR.)
• similarly, further mathlib lemmas about e.g. one-point compatification are also welcome.

[SnirBroshi]

Doesn't it make more sense to require T2Space M instead of defining the proposition with it?
Currently every non-Hausdorff space satisfies this vacuously, which seems strange (although I don't know the maths here, so maybe it makes sense).

[grunweg]

Also, every topological space which is not a manifold satisfies this vacuously... so I'm not convinced yet that Hausdorff-ness is very particular in this regard.

[Deicyde]

I wrote it this way in order to fix a linter warning. The other option is to add @[nolint unusedArguments]. Do you prefer it like this?

[SnirBroshi]

Yeah that is what I meant, but I'm not an expert, so it's best to ask @grunweg.

btw what's the point of this def? I would have expected something more like the proof_wanteds in Geometry/Manifold/PoincareConjecture. If this def accurately describes the smooth Poincaré conjecture as its docstring claims, shouldn't there be a proof_wanted for it?