Update Mathlib/Topology/Baire/LocallyCompactRegular.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

Author: CoolRmal

Mathlib/Topology/Baire/LocallyCompactRegular.lean

@@ -63,7 +63,7 @@ theorem IsGδ.of_t2Space_locallyCompactSpace (hG : IsGδ s) : BaireSpace s := by
   have : BaireSpace (closure s) := by
     convert BaireSpace.of_t2Space_locallyCompactSpace using 1
     · infer_instance
-    · exact IsClosed.locallyCompactSpace isClosed_closure
+    · exact isClosed_closure.locallyCompactSpace
   have : BaireSpace ((↑) ⁻¹' s : Set (closure s)) := IsGδ.baireSpace_of_dense
     (isGδ_induced continuous_subtype_val hG)
     (by simp [Subtype.dense_iff, inter_eq_right.mpr subset_closure])