feat: Urysohn lemma in regular locally compact spaces (#8124)

Also change a few theorems to instances, as instance loops are not a
problem any more.

---
<!-- The text above the `---` will become the commit message when your
PR is merged. Please leave a blank newline before the `---`, otherwise
GitHub will format the text above it as a title.

To indicate co-authors, include lines at the bottom of the commit
message
(that is, before the `---`) using the following format:

Co-authored-by: Author Name <author@email.com>

Any other comments you want to keep out of the PR commit should go
below the `---`, and placed outside this HTML comment, or else they
will be invisible to reviewers.

If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]
-->

[![Open in
Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Mathlib/Topology/EMetricSpace/Basic.lean

@@ -852,9 +852,9 @@ open TopologicalSpace
 
 variable (α)
 
-/-- A sigma compact pseudo emetric space has second countable topology. This is not an instance
-to avoid a loop with `sigmaCompactSpace_of_locally_compact_second_countable`.  -/
-theorem secondCountable_of_sigmaCompact [SigmaCompactSpace α] : SecondCountableTopology α := by
+/-- A sigma compact pseudo emetric space has second countable topology. -/
+instance (priority := 90) secondCountable_of_sigmaCompact [SigmaCompactSpace α] :
+    SecondCountableTopology α := by
   suffices SeparableSpace α by exact UniformSpace.secondCountable_of_separable α
   choose T _ hTc hsubT using fun n =>
     subset_countable_closure_of_compact (isCompact_compactCovering α n)

Mathlib/Topology/Metrizable/Urysohn.lean

@@ -109,7 +109,8 @@ theorem exists_inducing_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Inducing f := by
 /-- *Urysohn's metrization theorem* (Tychonoff's version):
 a regular topological space with second countable topology `X` is metrizable,
 i.e., there exists a pseudometric space structure that generates the same topology. -/
-lemma PseudoMetrizableSpace.of_regularSpace_secondCountableTopology : PseudoMetrizableSpace X :=
+instance (priority := 90) PseudoMetrizableSpace.of_regularSpace_secondCountableTopology :
+    PseudoMetrizableSpace X :=
   let ⟨_, hf⟩ := exists_inducing_l_infty X
   hf.pseudoMetrizableSpace
 
@@ -124,8 +125,7 @@ theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f :=
 /-- *Urysohn's metrization theorem* (Tychonoff's version): a T₃ topological space with second
 countable topology `X` is metrizable, i.e., there exists a metric space structure that generates the
 same topology. -/
-theorem metrizableSpace_of_t3_second_countable : MetrizableSpace X :=
+instance (priority := 90) metrizableSpace_of_t3_second_countable : MetrizableSpace X :=
   let ⟨_, hf⟩ := exists_embedding_l_infty X
   hf.metrizableSpace
 #align topological_space.metrizable_space_of_t3_second_countable TopologicalSpace.metrizableSpace_of_t3_second_countable
-

Mathlib/Topology/Separation.lean

@@ -1731,8 +1731,8 @@ section ClosableCompactSubsetOpenSpace
 
 /-- A class of topological spaces in which, given a compact set included inside an open set, then
 the closure of the compact set is also included in the open set.
-Satisfied notably for T2 spaces and regular spaces, and useful
-when discussing classes of regular measures. -/
+Satisfied notably for T2 spaces and regular spaces, and useful when discussing classes of
+regular measures. Equivalent to regularity among locally compact spaces. -/
 class ClosableCompactSubsetOpenSpace (X : Type*) [TopologicalSpace X] : Prop :=
   closure_subset_of_isOpen : ∀ (K U : Set X), IsCompact K → IsOpen U → K ⊆ U → closure K ⊆ U
 
@@ -1741,12 +1741,12 @@ theorem IsCompact.closure_subset_of_isOpen [ClosableCompactSubsetOpenSpace X]
     closure s ⊆ u :=
   ClosableCompactSubsetOpenSpace.closure_subset_of_isOpen s u hs hu h
 
-instance [T2Space X] : ClosableCompactSubsetOpenSpace X :=
+instance (priority := 150) [T2Space X] : ClosableCompactSubsetOpenSpace X :=
   ⟨fun K _U K_comp _U_open KU ↦ by rwa [K_comp.isClosed.closure_eq]⟩
 
 /-- In a (possibly non-Hausdorff) regular space, if a compact set `s` is contained in an
 open set `u`, then its closure is also contained in `u`. -/
-instance [RegularSpace X] : ClosableCompactSubsetOpenSpace X := by
+instance (priority := 150) [RegularSpace X] : ClosableCompactSubsetOpenSpace X := by
   refine ⟨fun s u hs hu h ↦ ?_⟩
   obtain ⟨F, sF, F_closed, Fu⟩ : ∃ F, s ⊆ F ∧ IsClosed F ∧ F ⊆ u := by
     apply hs.induction_on (p := fun t ↦ ∃ F, t ⊆ F ∧ IsClosed F ∧ F ⊆ u)
@@ -1779,6 +1779,16 @@ theorem exists_compact_closed_between [LocallyCompactSpace X] [ClosableCompactSu
   · apply M_comp.closure_subset_of_isOpen hU
     exact ML.trans (interior_subset.trans LU)
 
+/-- A locally compact space with the `ClosableCompactSubsetOpenSpace` is `Regular`. -/
+instance (priority := 80) [LocallyCompactSpace X] [ClosableCompactSubsetOpenSpace X] :
+    RegularSpace X := by
+  apply RegularSpace.ofExistsMemNhdsIsClosedSubset (fun x s hx ↦ ?_)
+  rcases _root_.mem_nhds_iff.1 hx with ⟨u, us, u_open, xu⟩
+  rcases exists_compact_closed_between (isCompact_singleton (a := x)) u_open (by simpa using xu)
+    with ⟨t, -, t_closed, xt, tu⟩
+  have : interior t ∈ 𝓝 x := isOpen_interior.mem_nhds (by simpa using xt)
+  exact ⟨t, interior_mem_nhds.mp this, t_closed, tu.trans us⟩
+
 protected theorem IsCompact.closure [WeaklyLocallyCompactSpace X] [ClosableCompactSubsetOpenSpace X]
     {K : Set X} (hK : IsCompact K) : IsCompact (closure K) := by
   rcases exists_compact_superset hK with ⟨L, L_comp, hL⟩