feat: review and expand API on behavior of topological bases under so…

…me constructions (#10732)

The main addition is `IsTopologicalBasis.inf` (see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Inf.20of.20a.20pair.20of.20topologies/near/419989448), and I also reordered things to be in the more typical order (deducing the `Pi` version from the `iInf` version rather than the converse).

Also a few extra golfs and variations.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>

Mathlib/Data/Analysis/Topology.lean

@@ -160,7 +160,7 @@ protected theorem isOpen [TopologicalSpace α] (F : Realizer α) (s : F.σ) : Is
 
 theorem ext' [T : TopologicalSpace α] {σ : Type*} {F : Ctop α σ}
     (H : ∀ a s, s ∈ 𝓝 a ↔ ∃ b, a ∈ F b ∧ F b ⊆ s) : F.toTopsp = T := by
-  refine' eq_of_nhds_eq_nhds fun x ↦ _
+  refine TopologicalSpace.ext_nhds fun x ↦ ?_
   ext s
   rw [mem_nhds_toTopsp, H]
 #align ctop.realizer.ext' Ctop.Realizer.ext'

Mathlib/Order/Filter/Bases.lean

@@ -432,6 +432,13 @@ theorem HasBasis.comp_equiv (h : l.HasBasis p s) (e : ι' ≃ ι) : l.HasBasis (
   h.comp_surjective e.surjective
 #align filter.has_basis.comp_equiv Filter.HasBasis.comp_equiv
 
+theorem HasBasis.to_image_id' (h : l.HasBasis p s) : l.HasBasis (fun t ↦ ∃ i, p i ∧ s i = t) id :=
+  ⟨fun _ ↦ by simp [h.mem_iff]⟩
+
+theorem HasBasis.to_image_id {ι : Type*} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
+    l.HasBasis (· ∈ s '' {i | p i}) id :=
+  h.to_image_id'
+
 /-- If `{s i | p i}` is a basis of a filter `l` and each `s i` includes `s j` such that
 `p j ∧ q j`, then `{s j | p j ∧ q j}` is a basis of `l`. -/
 theorem HasBasis.restrict (h : l.HasBasis p s) {q : ι → Prop}

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -898,7 +898,7 @@ theorem continuous_of_continuousAt_one₂ {H M : Type*} [CommMonoid M] [Topologi
 theorem TopologicalGroup.ext {G : Type*} [Group G] {t t' : TopologicalSpace G}
     (tg : @TopologicalGroup G t _) (tg' : @TopologicalGroup G t' _)
     (h : @nhds G t 1 = @nhds G t' 1) : t = t' :=
-  eq_of_nhds_eq_nhds fun x => by
+  TopologicalSpace.ext_nhds fun x ↦ by
     rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]
 #align topological_group.ext TopologicalGroup.ext
 #align topological_add_group.ext TopologicalAddGroup.ext

Mathlib/Topology/Bases.lean

@@ -119,21 +119,23 @@ theorem isTopologicalBasis_of_subbasis {s : Set (Set α)} (hs : t = generateFrom
     exact ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩
 #align topological_space.is_topological_basis_of_subbasis TopologicalSpace.isTopologicalBasis_of_subbasis
 
+theorem IsTopologicalBasis.of_hasBasis_nhds {s : Set (Set α)}
+    (h_nhds : ∀ a, (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id) : IsTopologicalBasis s where
+  exists_subset_inter t₁ ht₁ t₂ ht₂ x hx := by
+    simpa only [and_assoc, (h_nhds x).mem_iff]
+      using (inter_mem ((h_nhds _).mem_of_mem ⟨ht₁, hx.1⟩) ((h_nhds _).mem_of_mem ⟨ht₂, hx.2⟩))
+  sUnion_eq := sUnion_eq_univ_iff.2 fun x ↦ (h_nhds x).ex_mem
+  eq_generateFrom := ext_nhds fun x ↦ by
+    simpa only [nhds_generateFrom, and_comm] using (h_nhds x).eq_biInf
+
 /-- If a family of open sets `s` is such that every open neighbourhood contains some
 member of `s`, then `s` is a topological basis. -/
 theorem isTopologicalBasis_of_isOpen_of_nhds {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u)
     (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) :
-    IsTopologicalBasis s := by
-  refine'
-    ⟨fun t₁ ht₁ t₂ ht₂ x hx => h_nhds _ _ hx (IsOpen.inter (h_open _ ht₁) (h_open _ ht₂)), _, _⟩
-  · refine' sUnion_eq_univ_iff.2 fun a => _
-    rcases h_nhds a univ trivial isOpen_univ with ⟨u, h₁, h₂, -⟩
-    exact ⟨u, h₁, h₂⟩
-  · refine' (le_generateFrom h_open).antisymm fun u hu => _
-    refine (@isOpen_iff_nhds α u (generateFrom s)).mpr fun a ha ↦ ?_
-    rcases h_nhds a u ha hu with ⟨v, hvs, hav, hvu⟩
-    rw [nhds_generateFrom]
-    exact iInf₂_le_of_le v ⟨hav, hvs⟩ (le_principal_iff.2 hvu)
+    IsTopologicalBasis s :=
+  .of_hasBasis_nhds <| fun a ↦
+    (nhds_basis_opens a).to_hasBasis' (by simpa [and_assoc] using h_nhds a)
+      fun t ⟨hts, hat⟩ ↦ (h_open _ hts).mem_nhds hat
 #align topological_space.is_topological_basis_of_open_of_nhds TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
 
 /-- A set `s` is in the neighbourhood of `a` iff there is some basis set `t`, which
@@ -245,32 +247,38 @@ theorem isTopologicalBasis_opens : IsTopologicalBasis { U : Set α | IsOpen U }
   isTopologicalBasis_of_isOpen_of_nhds (by tauto) (by tauto)
 #align topological_space.is_topological_basis_opens TopologicalSpace.isTopologicalBasis_opens
 
+protected theorem IsTopologicalBasis.inducing {β} [TopologicalSpace β] {f : α → β} {T : Set (Set β)}
+    (hf : Inducing f) (h : IsTopologicalBasis T) : IsTopologicalBasis ((preimage f) '' T) :=
+  .of_hasBasis_nhds fun a ↦ by
+    convert (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s
+    aesop
+#align topological_space.is_topological_basis.inducing TopologicalSpace.IsTopologicalBasis.inducing
+
+protected theorem IsTopologicalBasis.induced [s : TopologicalSpace β] (f : α → β)
+    {T : Set (Set β)} (h : IsTopologicalBasis T) :
+    IsTopologicalBasis (t := induced f s) ((preimage f) '' T) :=
+  h.inducing (t := induced f s) (inducing_induced f)
+
+protected theorem IsTopologicalBasis.inf {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)}
+    (h₁ : IsTopologicalBasis (t := t₁) B₁) (h₂ : IsTopologicalBasis (t := t₂) B₂) :
+    IsTopologicalBasis (t := t₁ ⊓ t₂) (image2 (· ∩ ·) B₁ B₂) := by
+  refine .of_hasBasis_nhds (t := ?_) fun a ↦ ?_
+  rw [nhds_inf (t₁ := t₁)]
+  convert ((h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))).to_image_id
+  aesop
+
+theorem IsTopologicalBasis.inf_induced {γ} [s : TopologicalSpace β] {B₁ : Set (Set α)}
+    {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) (f₁ : γ → α)
+    (f₂ : γ → β) :
+    IsTopologicalBasis (t := induced f₁ t ⊓ induced f₂ s) (image2 (f₁ ⁻¹' · ∩ f₂ ⁻¹' ·) B₁ B₂) := by
+  simpa only [image2_image_left, image2_image_right] using (h₁.induced f₁).inf (h₂.induced f₂)
+
 protected theorem IsTopologicalBasis.prod {β} [TopologicalSpace β] {B₁ : Set (Set α)}
     {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) :
-    IsTopologicalBasis (image2 (· ×ˢ ·) B₁ B₂) := by
-  refine' isTopologicalBasis_of_isOpen_of_nhds _ _
-  · rintro _ ⟨u₁, hu₁, u₂, hu₂, rfl⟩
-    exact (h₁.isOpen hu₁).prod (h₂.isOpen hu₂)
-  · rintro ⟨a, b⟩ u hu uo
-    rcases (h₁.nhds_hasBasis.prod_nhds h₂.nhds_hasBasis).mem_iff.1 (IsOpen.mem_nhds uo hu) with
-      ⟨⟨s, t⟩, ⟨⟨hs, ha⟩, ht, hb⟩, hu⟩
-    exact ⟨s ×ˢ t, mem_image2_of_mem hs ht, ⟨ha, hb⟩, hu⟩
+    IsTopologicalBasis (image2 (· ×ˢ ·) B₁ B₂) :=
+  h₁.inf_induced h₂ Prod.fst Prod.snd
 #align topological_space.is_topological_basis.prod TopologicalSpace.IsTopologicalBasis.prod
 
-protected theorem IsTopologicalBasis.inducing {β} [TopologicalSpace β] {f : α → β} {T : Set (Set β)}
-    (hf : Inducing f) (h : IsTopologicalBasis T) : IsTopologicalBasis ((preimage f) '' T) := by
-  refine' isTopologicalBasis_of_isOpen_of_nhds _ _
-  · rintro _ ⟨V, hV, rfl⟩
-    rw [hf.isOpen_iff]
-    exact ⟨V, h.isOpen hV, rfl⟩
-  · intro a U ha hU
-    rw [hf.isOpen_iff] at hU
-    obtain ⟨V, hV, rfl⟩ := hU
-    obtain ⟨S, hS, rfl⟩ := h.open_eq_sUnion hV
-    obtain ⟨W, hW, ha⟩ := ha
-    exact ⟨f ⁻¹' W, ⟨_, hS hW, rfl⟩, ha, Set.preimage_mono <| Set.subset_sUnion_of_mem hW⟩
-#align topological_space.is_topological_basis.inducing TopologicalSpace.IsTopologicalBasis.inducing
-
 theorem isTopologicalBasis_of_cover {ι} {U : ι → Set α} (Uo : ∀ i, IsOpen (U i))
     (Uc : ⋃ i, U i = univ) {b : ∀ i, Set (Set (U i))} (hb : ∀ i, IsTopologicalBasis (b i)) :
     IsTopologicalBasis (⋃ i : ι, image ((↑) : U i → α) '' b i) := by
@@ -561,45 +569,44 @@ end TopologicalSpace
 
 open TopologicalSpace
 
+protected theorem IsTopologicalBasis.iInf {β : Type*} {ι : Type*} {t : ι → TopologicalSpace β}
+    {T : ι → Set (Set β)} (h_basis : ∀ i, IsTopologicalBasis (t := t i) (T i)) :
+    IsTopologicalBasis (t := ⨅ i, t i)
+      { S | ∃ (U : ι → Set β) (F : Finset ι), (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ i ∈ F, U i } := by
+  let _ := ⨅ i, t i
+  refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
+  · rintro - ⟨U, F, hU, rfl⟩
+    refine isOpen_biInter_finset fun i hi ↦
+      (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)
+  · intro a u ha hu
+    rcases (nhds_iInf (t := t) (a := a)).symm ▸ hasBasis_iInf'
+      (fun i ↦ (h_basis i).nhds_hasBasis (t := t i)) |>.mem_iff.1 (hu.mem_nhds ha)
+      with ⟨⟨F, U⟩, ⟨hF, hU⟩, hUu⟩
+    refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩ <;> simp only [Finite.mem_toFinset, mem_iInter]
+    · exact fun i hi ↦ (hU i hi).1
+    · exact fun i hi ↦ (hU i hi).2
+    · exact hUu
+
+theorem IsTopologicalBasis.iInf_induced {β : Type*} {ι : Type*} {X : ι → Type*}
+    [t : Π i, TopologicalSpace (X i)] {T : Π i, Set (Set (X i))}
+    (cond : ∀ i, IsTopologicalBasis (T i)) (f : Π i, β → X i) :
+    IsTopologicalBasis (t := ⨅ i, induced (f i) (t i))
+      { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),
+        (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ (i) (_ : i ∈ F), f i ⁻¹' U i } := by
+  convert IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i)) with S
+  constructor <;> rintro ⟨U, F, hUT, hSU⟩
+  · exact ⟨fun i ↦ (f i) ⁻¹' (U i), F, fun i hi ↦ mem_image_of_mem _ (hUT i hi), hSU⟩
+  · choose! U' hU' hUU' using hUT
+    exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩
+#align is_topological_basis_infi IsTopologicalBasis.iInf_induced
+
 theorem isTopologicalBasis_pi {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
     {T : ∀ i, Set (Set (X i))} (cond : ∀ i, IsTopologicalBasis (T i)) :
     IsTopologicalBasis { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),
       (∀ i, i ∈ F → U i ∈ T i) ∧ S = (F : Set ι).pi U } := by
-  refine' isTopologicalBasis_of_isOpen_of_nhds _ _
-  · rintro _ ⟨U, F, h1, rfl⟩
-    apply isOpen_set_pi F.finite_toSet
-    intro i hi
-    exact (cond i).isOpen (h1 i hi)
-  · intro a U ha hU
-    obtain ⟨I, t, hta, htU⟩ : ∃ (I : Finset ι) (t : ∀ i : ι, Set (X i)),
-        (∀ i, t i ∈ 𝓝 (a i)) ∧ Set.pi (↑I) t ⊆ U := by
-      rw [← Filter.mem_pi', ← nhds_pi]
-      exact hU.mem_nhds ha
-    have : ∀ i, ∃ V ∈ T i, a i ∈ V ∧ V ⊆ t i := fun i => (cond i).mem_nhds_iff.1 (hta i)
-    choose V hVT haV hVt using this
-    exact ⟨_, ⟨V, I, fun i _ => hVT i, rfl⟩, fun i _ => haV i, (pi_mono fun i _ => hVt i).trans htU⟩
+  simpa only [Set.pi_def] using IsTopologicalBasis.iInf_induced cond eval
 #align is_topological_basis_pi isTopologicalBasis_pi
 
-theorem isTopologicalBasis_iInf {β : Type*} {ι : Type*} {X : ι → Type*}
-    [t : ∀ i, TopologicalSpace (X i)] {T : ∀ i, Set (Set (X i))}
-    (cond : ∀ i, IsTopologicalBasis (T i)) (f : ∀ i, β → X i) :
-    @IsTopologicalBasis β (⨅ i, induced (f i) (t i))
-      { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),
-        (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ (i) (_ : i ∈ F), f i ⁻¹' U i } := by
-  letI := ⨅ i, induced (f i) (t i)
-  convert (isTopologicalBasis_pi cond).inducing (inducing_iInf_to_pi f)
-  ext V
-  constructor
-  · rintro ⟨U, F, h1, rfl⟩
-    refine' ⟨(F : Set ι).pi U, ⟨U, F, h1, rfl⟩, _⟩
-    simp_rw [pi_def, Set.preimage_iInter]
-    rfl
-  · rintro ⟨U, ⟨U, F, h1, rfl⟩, rfl⟩
-    refine' ⟨U, F, h1, _⟩
-    simp_rw [pi_def, Set.preimage_iInter]
-    rfl
-#align is_topological_basis_infi isTopologicalBasis_iInf
-
 theorem isTopologicalBasis_singletons (α : Type*) [TopologicalSpace α] [DiscreteTopology α] :
     IsTopologicalBasis { s | ∃ x : α, (s : Set α) = {x} } :=
   isTopologicalBasis_of_isOpen_of_nhds (fun _ _ => isOpen_discrete _) fun x _ hx _ =>
@@ -886,18 +893,10 @@ topological bases on each of the parts of the space. -/
 theorem IsTopologicalBasis.sigma {s : ∀ i : ι, Set (Set (E i))}
     (hs : ∀ i, IsTopologicalBasis (s i)) :
     IsTopologicalBasis (⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σi, E i))) '' s i) := by
-  apply isTopologicalBasis_of_isOpen_of_nhds
-  · intro u hu
-    obtain ⟨i, t, ts, rfl⟩ : ∃ (i : ι) (t : Set (E i)), t ∈ s i ∧ Sigma.mk i '' t = u := by
-      simpa only [mem_iUnion, mem_image] using hu
-    exact isOpenMap_sigmaMk _ ((hs i).isOpen ts)
-  · rintro ⟨i, x⟩ u hxu u_open
-    have hx : x ∈ Sigma.mk i ⁻¹' u := hxu
-    obtain ⟨v, vs, xv, hv⟩ : ∃ (v : Set (E i)), v ∈ s i ∧ x ∈ v ∧ v ⊆ Sigma.mk i ⁻¹' u :=
-      (hs i).exists_subset_of_mem_open hx (isOpen_sigma_iff.1 u_open i)
-    exact
-      ⟨Sigma.mk i '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ vs⟩, mem_image_of_mem _ xv,
-        image_subset_iff.2 hv⟩
+  refine .of_hasBasis_nhds fun a ↦ ?_
+  rw [Sigma.nhds_eq]
+  convert (((hs a.1).nhds_hasBasis).map _).to_image_id
+  aesop
 #align topological_space.is_topological_basis.sigma TopologicalSpace.IsTopologicalBasis.sigma
 
 /-- A countable disjoint union of second countable spaces is second countable. -/

Mathlib/Topology/Basic.lean

@@ -1174,6 +1174,12 @@ theorem isOpen_iff_nhds : IsOpen s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s :=
     _ ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s := by simp_rw [interior_eq_nhds, subset_def, mem_setOf]
 #align is_open_iff_nhds isOpen_iff_nhds
 
+theorem TopologicalSpace.ext_iff_nhds {t t' : TopologicalSpace X} :
+    t = t' ↔ ∀ x, @nhds _ t x = @nhds _ t' x :=
+  ⟨fun H x ↦ congrFun (congrArg _ H) _, fun H ↦ by ext; simp_rw [@isOpen_iff_nhds _ _ _, H]⟩
+
+alias ⟨_, TopologicalSpace.ext_nhds⟩ := TopologicalSpace.ext_iff_nhds
+
 theorem isOpen_iff_mem_nhds : IsOpen s ↔ ∀ x ∈ s, s ∈ 𝓝 x :=
   isOpen_iff_nhds.trans <| forall_congr' fun _ => imp_congr_right fun _ => le_principal_iff
 #align is_open_iff_mem_nhds isOpen_iff_mem_nhds

Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean

@@ -64,7 +64,7 @@ theorem isTopologicalBasis_cofiltered_limit (T : ∀ j, Set (Set (F.obj j)))
       exact ⟨j, V, hV, rfl⟩
   -- Using `D`, we can apply the characterization of the topological basis of a
   -- topology defined as an infimum...
-  convert isTopologicalBasis_iInf hT fun j (x : D.pt) => D.π.app j x using 1
+  convert IsTopologicalBasis.iInf_induced hT fun j (x : D.pt) => D.π.app j x using 1
   ext U0
   constructor
   · rintro ⟨j, V, hV, rfl⟩

Mathlib/Topology/Maps.lean

@@ -84,6 +84,10 @@ theorem nhds_eq_comap (hf : Inducing f) : ∀ x : X, 𝓝 x = comap f (𝓝 <| f
   inducing_iff_nhds.1 hf
 #align inducing.nhds_eq_comap Inducing.nhds_eq_comap
 
+theorem basis_nhds {p : ι → Prop} {s : ι → Set Y} (hf : Inducing f) {x : X}
+    (h_basis : (𝓝 (f x)).HasBasis p s) : (𝓝 x).HasBasis p (preimage f ∘ s) :=
+  hf.nhds_eq_comap x ▸ h_basis.comap f
+
 theorem nhdsSet_eq_comap (hf : Inducing f) (s : Set X) :
     𝓝ˢ s = comap f (𝓝ˢ (f '' s)) := by
   simp only [nhdsSet, sSup_image, comap_iSup, hf.nhds_eq_comap, iSup_image]

Mathlib/Topology/Order.lean

@@ -321,10 +321,9 @@ theorem le_of_nhds_le_nhds (h : ∀ x, @nhds α t₁ x ≤ @nhds α t₂ x) : t
   exact fun hs a ha => h _ (hs _ ha)
 #align le_of_nhds_le_nhds le_of_nhds_le_nhds
 
-theorem eq_of_nhds_eq_nhds (h : ∀ x, @nhds α t₁ x = @nhds α t₂ x) : t₁ = t₂ :=
-  le_antisymm (le_of_nhds_le_nhds fun x => (h x).le)
-    (le_of_nhds_le_nhds fun x => (h x).ge)
-#align eq_of_nhds_eq_nhds eq_of_nhds_eq_nhds
+@[deprecated] -- Since 2024-03-01
+alias eq_of_nhds_eq_nhds := TopologicalSpace.ext_nhds
+#align eq_of_nhds_eq_nhds TopologicalSpace.ext_nhds
 
 theorem eq_bot_of_singletons_open {t : TopologicalSpace α} (h : ∀ x, IsOpen[t] {x}) : t = ⊥ :=
   bot_unique fun s _ => biUnion_of_singleton s ▸ isOpen_biUnion fun x _ => h x
@@ -814,7 +813,7 @@ theorem continuous_id_of_le {t t' : TopologicalSpace α} (h : t ≤ t') : Contin
 theorem mem_nhds_induced [T : TopologicalSpace α] (f : β → α) (a : β) (s : Set β) :
     s ∈ @nhds β (TopologicalSpace.induced f T) a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s := by
   letI := T.induced f
-  simp only [mem_nhds_iff, isOpen_induced_iff, exists_prop, Set.mem_setOf_eq]
+  simp_rw [mem_nhds_iff, isOpen_induced_iff]
   constructor
   · rintro ⟨u, usub, ⟨v, openv, rfl⟩, au⟩
     exact ⟨v, ⟨v, Subset.rfl, openv, au⟩, usub⟩
@@ -829,9 +828,8 @@ theorem nhds_induced [T : TopologicalSpace α] (f : β → α) (a : β) :
 #align nhds_induced nhds_induced
 
 theorem induced_iff_nhds_eq [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : β → α) :
-    tβ = tα.induced f ↔ ∀ b, 𝓝 b = comap f (𝓝 <| f b) :=
-  ⟨fun h a => h.symm ▸ nhds_induced f a, fun h =>
-    eq_of_nhds_eq_nhds fun x => by rw [h, nhds_induced]⟩
+    tβ = tα.induced f ↔ ∀ b, 𝓝 b = comap f (𝓝 <| f b) := by
+  simp only [ext_iff_nhds, nhds_induced]
 #align induced_iff_nhds_eq induced_iff_nhds_eq
 
 theorem map_nhds_induced_of_surjective [T : TopologicalSpace α] {f : β → α} (hf : Surjective f)

Mathlib/Topology/Order/Basic.lean

@@ -1102,7 +1102,7 @@ theorem nhds_eq_iInf_abs_sub (a : α) : 𝓝 a = ⨅ r > 0, 𝓟 { b | |a - b| <
 
 theorem orderTopology_of_nhds_abs {α : Type*} [TopologicalSpace α] [LinearOrderedAddCommGroup α]
     (h_nhds : ∀ a : α, 𝓝 a = ⨅ r > 0, 𝓟 { b | |a - b| < r }) : OrderTopology α := by
-  refine' ⟨eq_of_nhds_eq_nhds fun a => _⟩
+  refine' ⟨TopologicalSpace.ext_nhds fun a => _⟩
   rw [h_nhds]
   letI := Preorder.topology α; letI : OrderTopology α := ⟨rfl⟩
   exact (nhds_eq_iInf_abs_sub a).symm

Mathlib/Topology/UniformSpace/Basic.lean

@@ -1321,7 +1321,7 @@ theorem toTopologicalSpace_top : @UniformSpace.toTopologicalSpace α ⊤ = ⊤ :
 
 theorem toTopologicalSpace_iInf {ι : Sort*} {u : ι → UniformSpace α} :
     (iInf u).toTopologicalSpace = ⨅ i, (u i).toTopologicalSpace :=
-  eq_of_nhds_eq_nhds fun a => by simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf,
+  TopologicalSpace.ext_nhds fun a ↦ by simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf,
     iInf_uniformity, @nhds_eq_comap_uniformity _ (u _), Filter.comap_iInf]
 #align to_topological_space_infi UniformSpace.toTopologicalSpace_iInf
 

Mathlib/Topology/UniformSpace/CompactConvergence.lean

@@ -164,7 +164,7 @@ and replace the topology with `compactOpen` to avoid non-defeq diamonds,
 see Note [forgetful inheritance].  -/
 instance compactConvergenceUniformSpace : UniformSpace C(α, β) :=
   .replaceTopology (.comap toUniformOnFunIsCompact inferInstance) <| by
-    refine eq_of_nhds_eq_nhds fun f ↦ eq_of_forall_le_iff fun l ↦ ?_
+    refine TopologicalSpace.ext_nhds fun f ↦ eq_of_forall_le_iff fun l ↦ ?_
     simp_rw [← tendsto_id', tendsto_iff_forall_compact_tendstoUniformlyOn,
       nhds_induced, tendsto_comap_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]
     rfl