diff --git a/Mathlib/Geometry/Manifold/PoincareConjecture.lean b/Mathlib/Geometry/Manifold/PoincareConjecture.lean
index 35a71bbd1c70bb..2d3161b21fd34f 100644
--- a/Mathlib/Geometry/Manifold/PoincareConjecture.lean
+++ b/Mathlib/Geometry/Manifold/PoincareConjecture.lean
@@ -38,6 +38,7 @@ open ContinuousMap
 /-- The smooth Poincaré conjecture; true for n = 1, 2, 3, 5, 6, 12, 56, and 61,
 open for n = 4, and it is conjectured that there are no other n > 4 for which it is true
 (Conjecture 1.17, https://annals.math.princeton.edu/2017/186-2/p03). -/
-def ContinuousMap.HomotopyEquiv.NonemptyDiffeomorphSphere (n : ℕ) : Prop :=
+@[nolint unusedArguments]
+def ContinuousMap.HomotopyEquiv.NonemptyDiffeomorphSphere [T2Space M] (n : ℕ) : Prop :=
   ∀ (_ : ChartedSpace ℝⁿ M) (_ : IsManifold (𝓡 n) ∞ M),
     M ≃ₕ 𝕊ⁿ → Nonempty (M ≃ₘ⟮𝓡 n, 𝓡 n⟯ 𝕊ⁿ)