feat(Topology/UniformSpace): add isRefl_of_mem_uniformity (leanprover-community#32850)

This PR adds a lemma to directly obtain `U.IsRefl` for an entourage `U` of a uniform space.

Author: gasparattila

Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean

@@ -333,7 +333,7 @@ theorem coverEntropyInf_eq_iSup_netEntropyInfEntourage :
     coverEntropyInf T F = ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U := by
   apply le_antisymm <;> refine iSup₂_le fun U U_uni ↦ ?_
   · obtain ⟨V, V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni
-    have := SetRel.id_subset_iff.1 <| refl_le_uniformity V_uni
+    have := isRefl_of_mem_uniformity V_uni
     apply (coverEntropyInfEntourage_antitone T F V_U).trans (le_iSup₂_of_le V V_uni _)
     exact coverEntropyInfEntourage_le_netEntropyInfEntourage T F
   · apply (netEntropyInfEntourage_antitone T F SetRel.symmetrize_subset_self).trans
@@ -349,7 +349,7 @@ theorem coverEntropy_eq_iSup_netEntropyEntourage :
   apply le_antisymm <;> refine iSup₂_le fun U U_uni ↦ ?_
   · obtain ⟨V, V_uni, V_symm, V_comp_U⟩ := comp_symm_mem_uniformity_sets U_uni
     apply (coverEntropyEntourage_antitone T F V_comp_U).trans (le_iSup₂_of_le V V_uni _)
-    have := SetRel.id_subset_iff.1 <| refl_le_uniformity V_uni
+    have := isRefl_of_mem_uniformity V_uni
     exact coverEntropyEntourage_le_netEntropyEntourage T F
   · apply (netEntropyEntourage_antitone T F SetRel.symmetrize_subset_self).trans
     apply (le_iSup₂ (SetRel.symmetrize U) (symmetrize_mem_uniformity U_uni)).trans'

Mathlib/Topology/UniformSpace/Basic.lean

@@ -85,7 +85,7 @@ theorem eventually_uniformity_iterate_comp_subset {s : SetRel α α} (hs : s ∈
     rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
     refine (ihn htU).mono fun U hU => ?_
     rw [Function.iterate_succ_apply']
-    have : SetRel.IsRefl t := SetRel.id_subset_iff.1 <| refl_le_uniformity htU
+    have := isRefl_of_mem_uniformity htU
     exact ⟨hU.1.trans <| SetRel.left_subset_comp.trans hts,
      (SetRel.comp_subset_comp hU.1 hU.2).trans hts⟩
 

Mathlib/Topology/UniformSpace/Closeds.lean

@@ -102,7 +102,7 @@ protected abbrev UniformSpace.hausdorff : UniformSpace (Set α) := .ofCore
     refl := by
       simp_rw [Filter.principal_le_lift', SetRel.id_subset_iff]
       intro (U : SetRel α α) hU
-      have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU⟩
+      have := isRefl_of_mem_uniformity hU
       exact isRefl_hausdorffEntourage U
     symm :=
       Filter.tendsto_lift'.mpr fun U hU => Filter.mem_of_superset

Mathlib/Topology/UniformSpace/Defs.lean

@@ -470,6 +470,9 @@ instance uniformity.neBot [Nonempty α] : NeBot (𝓤 α) :=
 theorem refl_mem_uniformity {x : α} {s : SetRel α α} (h : s ∈ 𝓤 α) : (x, x) ∈ s :=
   refl_le_uniformity h rfl
 
+theorem isRefl_of_mem_uniformity {s : SetRel α α} (h : s ∈ 𝓤 α) : s.IsRefl :=
+  ⟨fun _ => refl_mem_uniformity h⟩
+
 theorem mem_uniformity_of_eq {x y : α} {s : SetRel α α} (h : s ∈ 𝓤 α) (hx : x = y) : (x, y) ∈ s :=
   refl_le_uniformity h hx
 
@@ -480,8 +483,8 @@ theorem comp_le_uniformity : ((𝓤 α).lift' fun s : SetRel α α => s ○ s) 
   UniformSpace.comp
 
 theorem lift'_comp_uniformity : ((𝓤 α).lift' fun s : SetRel α α => s ○ s) = 𝓤 α :=
-  comp_le_uniformity.antisymm <| le_lift'.2 fun s hs ↦ mem_of_superset hs <|
-    have : SetRel.IsRefl s := ⟨fun _ ↦ refl_mem_uniformity hs⟩; SetRel.left_subset_comp
+  comp_le_uniformity.antisymm <| le_lift'.2 fun _s hs ↦ mem_of_superset hs <|
+    have := isRefl_of_mem_uniformity hs; SetRel.left_subset_comp
 
 theorem tendsto_swap_uniformity : Tendsto (@Prod.swap α α) (𝓤 α) (𝓤 α) :=
   symm_le_uniformity
@@ -561,7 +564,7 @@ theorem uniformity_lift_le_comp {f : SetRel α α → Filter β} (h : Monotone f
 theorem comp3_mem_uniformity {s : SetRel α α} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ (t ○ t) ⊆ s :=
   let ⟨_t', ht', ht's⟩ := comp_mem_uniformity_sets hs
   let ⟨t, ht, htt'⟩ := comp_mem_uniformity_sets ht'
-  have : SetRel.IsRefl t := SetRel.id_subset_iff.1 <| refl_le_uniformity ht
+  have := isRefl_of_mem_uniformity ht
   ⟨t, ht, (SetRel.comp_subset_comp (SetRel.left_subset_comp.trans htt') htt').trans ht's⟩
 
 /-- See also `comp3_mem_uniformity`. -/
@@ -580,7 +583,7 @@ theorem comp_symm_mem_uniformity_sets {s : SetRel α α} (hs : s ∈ 𝓤 α) :
     _ ⊆ s := w_sub
 
 theorem subset_comp_self_of_mem_uniformity {s : SetRel α α} (h : s ∈ 𝓤 α) : s ⊆ s ○ s :=
-  have : SetRel.IsRefl s := SetRel.id_subset_iff.1 <| refl_le_uniformity h; SetRel.left_subset_comp
+  have := isRefl_of_mem_uniformity h; SetRel.left_subset_comp
 
 theorem comp_comp_symm_mem_uniformity_sets {s : SetRel α α} (hs : s ∈ 𝓤 α) :
     ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s := by