Changed space to be over type alpha

anishrajeev · anishrajeev · commit 10167220c8eb · 2025-12-16T19:27:07.000-05:00
diff --git a/Mathlib/ModelTheory/Topology/Types.lean b/Mathlib/ModelTheory/Topology/Types.lean
@@ -66,7 +66,7 @@ instance : TotallySeparatedSpace (CompleteType T α) := by
         by change ¬∼φ∈q; rwa [not_mem_iff,←hφ, not_not, ←not_mem_iff]
       ⟩)
 
-instance {n : ℕ} : CompactSpace (T.CompleteType (Fin n)) := by
+instance : CompactSpace (T.CompleteType α) := by
   constructor
   rw[isCompact_iff_ultrafilter_le_nhds]
   intros F _
