fix: replace ? with ?_ in refine (anonymous goal syntax)

Author: thothrde

Mathlib/Condensed/Solid.lean

@@ -146,7 +146,7 @@ lemma isSolid_of_isLimit {J : Type*} [SmallCategory J]
     (c : Cone F) (hc : IsLimit c)
     (hj : ∀ j, (F.obj j).IsSolid) :
     c.pt.IsSolid := by
-  refine ⟨fun X => ?⟩
+  refine ⟨fun X => ?_⟩
   rw [isIso_iff_bijective]
   set sol := (profiniteSolidification R).app X
   have bijFun : ∀ j, Function.Bijective ((yoneda.obj (F.obj j)).map sol.op) := by
@@ -176,7 +176,7 @@ lemma isSolid_of_isLimit {J : Type*} [SmallCategory J]
                 naturality := fun j k φ => by
                   change 𝟙 _ ≫ g_j k = g_j j ≫ F.map φ
                   simp only [Category.id_comp]; exact (compat φ).symm } }
-    refine ⟨hc.lift g_cone, ?⟩
+    refine ⟨hc.lift g_cone, ?_⟩
     change sol ≫ hc.lift g_cone = h_map
     apply hc.hom_ext; intro j
     have hfac : hc.lift g_cone ≫ c.π.app j = g_j j := hc.fac g_cone j