Update Mathlib/Topology/Baire/LocallyCompactRegular.lean

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

Author: CoolRmal

Mathlib/Topology/Baire/LocallyCompactRegular.lean

@@ -64,8 +64,8 @@ theorem IsGδ.of_t2Space_locallyCompactSpace (hG : IsGδ s) : BaireSpace s := by
     convert BaireSpace.of_t2Space_locallyCompactSpace using 1
     · infer_instance
     · exact isClosed_closure.locallyCompactSpace
-  have : BaireSpace ((↑) ⁻¹' s : Set (closure s)) := IsGδ.baireSpace_of_dense
-    (isGδ_induced continuous_subtype_val hG)
+  have : BaireSpace ((↑) ⁻¹' s : Set (closure s)) :=
+    (isGδ_induced continuous_subtype_val hG).baireSpace_of_dense
     (by simp [Subtype.dense_iff, inter_eq_right.mpr subset_closure])
   have h_homeo : Homeomorph ((↑) ⁻¹' s : Set (closure s)) s := ⟨⟨fun x => ⟨x, x.2⟩,
     fun x => ⟨⟨x, subset_closure x.2⟩, x.2⟩, by grind, by grind⟩, by fun_prop, by fun_prop⟩