Update LocallyCompactRegular.lean

Author: CoolRmal

Mathlib/Topology/Baire/LocallyCompactRegular.lean

@@ -17,11 +17,10 @@ In this file we prove that a locally compact regular topological space has Baire
 
 open TopologicalSpace Set
 
-variable {X : Type*} [TopologicalSpace X] {s : Set X}
+variable {X : Type*} [TopologicalSpace X] {s : Set X} [R1Space X] [LocallyCompactSpace X]
 
 /-- **Second Baire theorem**: locally compact R₁ spaces are Baire. -/
-instance (priority := 100) BaireSpace.of_t2Space_locallyCompactSpace
-    [R1Space X] [LocallyCompactSpace X] : BaireSpace X := by
+instance (priority := 100) BaireSpace.of_t2Space_locallyCompactSpace : BaireSpace X := by
   constructor
   intro f ho hd
   /- To prove that an intersection of open dense subsets is dense, prove that its intersection
@@ -60,7 +59,7 @@ instance (priority := 100) BaireSpace.of_t2Space_locallyCompactSpace
   exact hK_nonempty.mono hK_subset
 
 /-- A Gδ subset of a locally compact R₁ space is Baire. -/
-theorem IsGδ.of_t2Space_locallyCompactSpace (hG : IsGδ s) [R1Space X] [LocallyCompactSpace X] :
+theorem IsGδ.of_t2Space_locallyCompactSpace (hG : IsGδ s) :
     BaireSpace s := by
   have : BaireSpace (closure s) := by
     convert BaireSpace.of_t2Space_locallyCompactSpace using 1