chore: fix universe issue in FinitaryExtensive Stonean (#8131)

Now `Stonean.{u}` is finitary extensive for any universe `u`.

Mathlib/Topology/Category/Stonean/Limits.lean

@@ -323,15 +323,19 @@ instance : HasPullbacksOfInclusions Stonean where
     apply Stonean.Sigma.openEmbedding_ι
 
 noncomputable
-instance : PreservesPullbacksOfInclusions Stonean.toCompHaus where
+instance : PreservesPullbacksOfInclusions Stonean.toCompHaus.{u} where
   preservesPullbackInl := by
     intros X Y Z f
     apply (config := { allowSynthFailures := true }) preservesPullbackSymmetry
     have : OpenEmbedding (coprod.inl : X ⟶ X ⨿ Y) := Stonean.Sigma.openEmbedding_ι _ _
     have := Stonean.createsPullbacksOfOpenEmbedding f this
-    apply preservesLimitOfReflectsOfPreserves Stonean.toCompHaus compHausToTop
+    refine @preservesLimitOfReflectsOfPreserves _ _ _ _ _ _ _ _ _ Stonean.toCompHaus
+      compHausToTop inferInstance ?_
+    apply (config := { allowSynthFailures := true }) ReflectsLimitsOfShape.reflectsLimit
+    apply (config := { allowSynthFailures := true }) ReflectsLimitsOfSize.reflectsLimitsOfShape
+    exact reflectsLimitsOfSizeShrink _
 
-instance : FinitaryExtensive Stonean :=
+instance : FinitaryExtensive Stonean.{u} :=
   have := fullyFaithfulReflectsLimits Stonean.toCompHaus
   have := fullyFaithfulReflectsColimits Stonean.toCompHaus
   finitaryExtensive_of_preserves_and_reflects Stonean.toCompHaus