chore(LocallyCompact): rename the "of basis" constructor (#9327)

Rename `locallyCompactSpace_of_hasBasis` to `LocallyCompactSpace.of_hasBasis`
to allow the new-style dot notation.

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -676,7 +676,7 @@ theorem ChartedSpace.locallyCompactSpace [LocallyCompactSpace H] : LocallyCompac
     rw [← (chartAt H x).symm_map_nhds_eq (mem_chart_source H x)]
     exact ((compact_basis_nhds (chartAt H x x)).hasBasis_self_subset
       (chart_target_mem_nhds H x)).map _
-  refine locallyCompactSpace_of_hasBasis this ?_
+  refine .of_hasBasis this ?_
   rintro x s ⟨_, h₂, h₃⟩
   exact h₂.image_of_continuousOn ((chartAt H x).continuousOn_symm.mono h₃)
 #align charted_space.locally_compact ChartedSpace.locallyCompactSpace

Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

@@ -357,7 +357,7 @@ protected theorem locallyCompactSpace [LocallyCompactSpace E] (I : ModelWithCorn
       fun s => I.symm '' (s ∩ range I) := fun x ↦ by
     rw [← I.symm_map_nhdsWithin_range]
     exact ((compact_basis_nhds (I x)).inf_principal _).map _
-  refine' locallyCompactSpace_of_hasBasis this _
+  refine' .of_hasBasis this _
   rintro x s ⟨-, hsc⟩
   exact (hsc.inter_right I.closed_range).image I.continuous_symm
 #align model_with_corners.locally_compact ModelWithCorners.locallyCompactSpace

Mathlib/Topology/Compactness/LocallyCompact.lean

@@ -86,19 +86,22 @@ theorem local_compact_nhds [LocallyCompactSpace X] {x : X} {n : Set X} (h : n 
   LocallyCompactSpace.local_compact_nhds _ _ h
 #align local_compact_nhds local_compact_nhds
 
-theorem locallyCompactSpace_of_hasBasis {ι : X → Type*} {p : ∀ x, ι x → Prop}
+theorem LocallyCompactSpace.of_hasBasis {ι : X → Type*} {p : ∀ x, ι x → Prop}
     {s : ∀ x, ι x → Set X} (h : ∀ x, (𝓝 x).HasBasis (p x) (s x))
     (hc : ∀ x i, p x i → IsCompact (s x i)) : LocallyCompactSpace X :=
   ⟨fun x _t ht =>
     let ⟨i, hp, ht⟩ := (h x).mem_iff.1 ht
     ⟨s x i, (h x).mem_of_mem hp, ht, hc x i hp⟩⟩
-#align locally_compact_space_of_has_basis locallyCompactSpace_of_hasBasis
+#align locally_compact_space_of_has_basis LocallyCompactSpace.of_hasBasis
+
+@[deprecated] -- since 29 Dec 2023
+alias locallyCompactSpace_of_hasBasis := LocallyCompactSpace.of_hasBasis
 
 instance Prod.locallyCompactSpace (X : Type*) (Y : Type*) [TopologicalSpace X]
     [TopologicalSpace Y] [LocallyCompactSpace X] [LocallyCompactSpace Y] :
     LocallyCompactSpace (X × Y) :=
   have := fun x : X × Y => (compact_basis_nhds x.1).prod_nhds' (compact_basis_nhds x.2)
-  locallyCompactSpace_of_hasBasis this fun _ _ ⟨⟨_, h₁⟩, _, h₂⟩ => h₁.prod h₂
+ .of_hasBasis this fun _ _ ⟨⟨_, h₁⟩, _, h₂⟩ => h₁.prod h₂
 #align prod.locally_compact_space Prod.locallyCompactSpace
 
 section Pi
@@ -214,11 +217,10 @@ theorem exists_compact_between [LocallyCompactSpace X] {K U : Set X} (hK : IsCom
 
 protected theorem ClosedEmbedding.locallyCompactSpace [LocallyCompactSpace Y] {f : X → Y}
     (hf : ClosedEmbedding f) : LocallyCompactSpace X :=
-  haveI : ∀ x : X, (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (f x) ∧ IsCompact s) fun s => f ⁻¹' s := by
-    intro x
+  haveI : ∀ x : X, (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (f x) ∧ IsCompact s) (f ⁻¹' ·) := fun x ↦ by
     rw [hf.toInducing.nhds_eq_comap]
     exact (compact_basis_nhds _).comap _
-  locallyCompactSpace_of_hasBasis this fun x s hs => hf.isCompact_preimage hs.2
+  .of_hasBasis this fun x s hs => hf.isCompact_preimage hs.2
 #align closed_embedding.locally_compact_space ClosedEmbedding.locallyCompactSpace
 
 protected theorem IsClosed.locallyCompactSpace [LocallyCompactSpace X] {s : Set X}
@@ -228,13 +230,12 @@ protected theorem IsClosed.locallyCompactSpace [LocallyCompactSpace X] {s : Set
 
 protected theorem OpenEmbedding.locallyCompactSpace [LocallyCompactSpace Y] {f : X → Y}
     (hf : OpenEmbedding f) : LocallyCompactSpace X := by
-  have : ∀ x : X, (𝓝 x).HasBasis
-      (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s := by
-    intro x
-    rw [hf.toInducing.nhds_eq_comap]
-    exact
-      ((compact_basis_nhds _).restrict_subset <| hf.open_range.mem_nhds <| mem_range_self _).comap _
-  refine' locallyCompactSpace_of_hasBasis this fun x s hs => _
+  have : ∀ x : X,
+      (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) (f ⁻¹' ·) := fun x ↦ by
+    rw [hf.nhds_eq_comap]
+    exact ((compact_basis_nhds _).restrict_subset <| hf.open_range.mem_nhds <|
+      mem_range_self _).comap _
+  refine .of_hasBasis this fun x s hs => ?_
   rw [hf.toInducing.isCompact_iff, image_preimage_eq_of_subset hs.2]
   exact hs.1.2
 #align open_embedding.locally_compact_space OpenEmbedding.locallyCompactSpace

Mathlib/Topology/MetricSpace/PseudoMetric.lean

@@ -2109,7 +2109,7 @@ instance (priority := 100) proper_of_compact [CompactSpace α] : ProperSpace α
 -- see Note [lower instance priority]
 /-- A proper space is locally compact -/
 instance (priority := 100) locally_compact_of_proper [ProperSpace α] : LocallyCompactSpace α :=
-  locallyCompactSpace_of_hasBasis (fun _ => nhds_basis_closedBall) fun _ _ _ =>
+  .of_hasBasis (fun _ => nhds_basis_closedBall) fun _ _ _ =>
     isCompact_closedBall _ _
 #align locally_compact_of_proper locally_compact_of_proper