feat: generalize urysohns lemma (#32337)

Generalize some of the theorems in the Urysohn's lemma file.

Author: plp127

Mathlib/Topology/UrysohnsLemma.lean

@@ -478,10 +478,10 @@ theorem exists_continuous_one_zero_of_isCompact_of_isGδ [RegularSpace X] [Local
   · apply le_trans _ hu.le
     exact (S x).tsum_le_tsum (fun n ↦ I n x) u_sum
 
-/-- A variation of Urysohn's lemma. In a `T2Space X`, for a closed set `t` and a relatively
+/-- A variation of Urysohn's lemma. In a `R1Space X`, for a closed set `t` and a relatively
 compact open set `s` such that `t ⊆ s`, there is a continuous function `f` supported in `s`,
 `f x = 1` on `t` and `0 ≤ f x ≤ 1`. -/
-lemma exists_tsupport_one_of_isOpen_isClosed [T2Space X] {s t : Set X}
+lemma exists_tsupport_one_of_isOpen_isClosed [R1Space X] {s t : Set X}
     (hs : IsOpen s) (hscp : IsCompact (closure s)) (ht : IsClosed t) (hst : t ⊆ s) :
     ∃ f : C(X, ℝ), tsupport f ⊆ s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
 -- separate `sᶜ` and `t` by `u` and `v`.
@@ -529,14 +529,16 @@ lemma exists_tsupport_one_of_isOpen_isClosed [T2Space X] {s t : Set X}
 /-- A variation of **Urysohn's lemma**. In a Hausdorff locally compact space, for a compact set `K`
 contained in an open set `V`, there exists a compactly supported continuous function `f` such that
 `0 ≤ f ≤ 1`, `f = 1` on K and the support of `f` is contained in `V`. -/
-lemma exists_continuousMap_one_of_isCompact_subset_isOpen [T2Space X] [LocallyCompactSpace X]
+lemma exists_continuousMap_one_of_isCompact_subset_isOpen [R1Space X] [LocallyCompactSpace X]
     {K V : Set X} (hK : IsCompact K) (hV : IsOpen V) (hKV : K ⊆ V) :
     ∃ f : C(X, ℝ), Set.EqOn f 1 K ∧ IsCompact (tsupport f) ∧
       tsupport f ⊆ V ∧ ∀ x, f x ∈ Set.Icc 0 1 := by
   obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_open_between_and_isCompact_closure hK hV hKV
-  obtain ⟨f, hf1, hf2, hf3⟩ := exists_tsupport_one_of_isOpen_isClosed hU1 hU4 hK.isClosed hU2
-  have : tsupport f ⊆ closure U := hf1.trans subset_closure
-  exact ⟨f, hf2, hU4.of_isClosed_subset isClosed_closure this, this.trans hU3, hf3⟩
+  obtain ⟨f, hf1, hf2, hf3⟩ := exists_tsupport_one_of_isOpen_isClosed hU1 hU4
+    isClosed_closure (hK.closure_subset_of_isOpen hU1 hU2)
+  have hfU : tsupport f ⊆ closure U := hf1.trans subset_closure
+  exact ⟨f, hf2.mono subset_closure,
+    .of_isClosed_subset hU4 isClosed_closure hfU, hfU.trans hU3, hf3⟩
 
 theorem exists_continuous_nonneg_pos [RegularSpace X] [LocallyCompactSpace X] (x : X) :
     ∃ f : C(X, ℝ), HasCompactSupport f ∧ 0 ≤ (f : X → ℝ) ∧ f x ≠ 0 := by