diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean
index 0559d62d..13589172 100644
--- a/SphereEversion/Loops/Surrounding.lean
+++ b/SphereEversion/Loops/Surrounding.lean
@@ -998,7 +998,7 @@ theorem exists_surrounding_loops (hK : IsClosed K) (hΩ_op : IsOpen Ω) (hg : 
         (surroundingFamilyIn_iff_germ.mpr ⟨hγ₂, h'γ₂⟩) with
       ⟨U, U_in, γ, H, H''⟩
     cases' surroundingFamilyIn_iff_germ.mp H with H H'
-    refine' ⟨γ, H, mem_of_superset U_in H', Eventually.union_nhdsSet.mpr H''⟩
+    exact ⟨γ, H, mem_of_superset U_in H', Eventually.union_nhdsSet.mpr H''⟩
 
 -- #lint
 -- #print axioms satisfied_or_refund