Update Mathlib/Analysis/LocallyConvex/Separation.lean

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Author: CoolRmal

Mathlib/Analysis/LocallyConvex/Separation.lean

@@ -396,8 +396,7 @@ theorem iInter_nat_halfSpaces_eq_of_prod {F : Type*} {s : Set (E × F)}
     simp [← map_add]
   · intro hs₃ hsne i
     obtain ⟨z, hz⟩ := eq2 hs₃ hsne i
-    use z.1, z.2
-    simpa [← map_add] using hz
+    exact ⟨z.1, z.2, by simpa [← map_add] using hz⟩
 
 end Countable