From 84b5683936c8d06c83c1f298ce7215cf31471bb5 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 23 Jan 2024 22:24:03 -0600
Subject: [PATCH 1/5] chore(Topology/Basic): rename variables

---
 Mathlib/Topology/Basic.lean | 737 ++++++++++++++++++------------------
 1 file changed, 367 insertions(+), 370 deletions(-)

diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean
index b1418ad62b6e9..9b702e014ce5f 100644
--- a/Mathlib/Topology/Basic.lean
+++ b/Mathlib/Topology/Basic.lean
@@ -13,14 +13,14 @@ import Mathlib.Tactic.Continuity
 /-!
 # Basic theory of topological spaces.
 
-The main definition is the type class `TopologicalSpace α` which endows a type `α` with a topology.
-Then `Set α` gets predicates `IsOpen`, `IsClosed` and functions `interior`, `closure` and
-`frontier`. Each point `x` of `α` gets a neighborhood filter `𝓝 x`. A filter `F` on `α` has
-`x` as a cluster point if `ClusterPt x F : 𝓝 x ⊓ F ≠ ⊥`. A map `f : ι → α` clusters at `x`
-along `F : Filter ι` if `MapClusterPt x F f : ClusterPt x (map f F)`. In particular
+The main definition is the type class `TopologicalSpace X` which endows a type `X` with a topology.
+Then `Set X` gets predicates `IsOpen`, `IsClosed` and functions `interior`, `closure` and
+`frontier`. Each point `x` of `X` gets a neighborhood filter `𝓝 x`. A filter `F` on `X` has
+`x` as a cluster point if `ClusterPt x F : 𝓝 x ⊓ F ≠ ⊥`. A map `f : α → X` clusters at `x`
+along `F : Filter α` if `MapClusterPt x F f : ClusterPt x (map f F)`. In particular
 the notion of cluster point of a sequence `u` is `MapClusterPt x atTop u`.
 
-For topological spaces `α` and `β`, a function `f : α → β` and a point `a : α`,
+For topological spaces `X` and `Y`, a function `f : X → Y` and a point `a : X`,
 `ContinuousAt f a` means `f` is continuous at `a`, and global continuity is
 `Continuous f`. There is also a version of continuity `PContinuous` for
 partially defined functions.
@@ -55,18 +55,18 @@ noncomputable section
 
 open Set Filter
 
-universe u v w
+universe u v w x
 
 /-!
 ### Topological spaces
 -/
 
 
-/-- A topology on `α`. -/
+/-- A topology on `X`. -/
 @[to_additive existing TopologicalSpace]
-class TopologicalSpace (α : Type u) where
+class TopologicalSpace (X : Type u) where
   /-- A predicate saying that a set is an open set. Use `IsOpen` in the root namespace instead. -/
-  protected IsOpen : Set α → Prop
+  protected IsOpen : Set X → Prop
   /-- The set representing the whole space is an open set. Use `isOpen_univ` in the root namespace
   instead. -/
   protected isOpen_univ : IsOpen univ
@@ -79,9 +79,9 @@ class TopologicalSpace (α : Type u) where
 
 /-- A constructor for topologies by specifying the closed sets,
 and showing that they satisfy the appropriate conditions. -/
-def TopologicalSpace.ofClosed {α : Type u} (T : Set (Set α)) (empty_mem : ∅ ∈ T)
+def TopologicalSpace.ofClosed {X : Type u} (T : Set (Set X)) (empty_mem : ∅ ∈ T)
     (sInter_mem : ∀ A, A ⊆ T → ⋂₀ A ∈ T)
-    (union_mem : ∀ A, A ∈ T → ∀ B, B ∈ T → A ∪ B ∈ T) : TopologicalSpace α where
+    (union_mem : ∀ A, A ∈ T → ∀ B, B ∈ T → A ∪ B ∈ T) : TopologicalSpace X where
   IsOpen X := Xᶜ ∈ T
   isOpen_univ := by simp [empty_mem]
   isOpen_inter s t hs ht := by simpa only [compl_inter] using union_mem sᶜ hs tᶜ ht
@@ -92,10 +92,11 @@ def TopologicalSpace.ofClosed {α : Type u} (T : Set (Set α)) (empty_mem : ∅
 
 section TopologicalSpace
 
-variable {α : Type u} {β : Type v} {ι : Sort w} {a : α} {s s₁ s₂ t : Set α} {p p₁ p₂ : α → Prop}
+variable {X : Type u} {Y : Type v} {ι : Sort w} {α β : Type*}
+  {a : X} {s s₁ s₂ t : Set X} {p p₁ p₂ : X → Prop}
 
-/-- `IsOpen s` means that `s` is open in the ambient topological space on `α` -/
-def IsOpen [TopologicalSpace α] : Set α → Prop := TopologicalSpace.IsOpen
+/-- `IsOpen s` means that `s` is open in the ambient topological space on `X` -/
+def IsOpen [TopologicalSpace X] : Set X → Prop := TopologicalSpace.IsOpen
 #align is_open IsOpen
 
 set_option quotPrecheck false in
@@ -104,48 +105,48 @@ scoped[Topology] notation (name := IsOpen_of) "IsOpen[" t "]" => @IsOpen _ t
 
 open Topology
 
-lemma isOpen_mk {p h₁ h₂ h₃} {s : Set α} : IsOpen[⟨p, h₁, h₂, h₃⟩] s ↔ p s := Iff.rfl
+lemma isOpen_mk {p h₁ h₂ h₃} {s : Set X} : IsOpen[⟨p, h₁, h₂, h₃⟩] s ↔ p s := Iff.rfl
 #align is_open_mk isOpen_mk
 
 @[ext]
 protected theorem TopologicalSpace.ext :
-    ∀ {f g : TopologicalSpace α}, IsOpen[f] = IsOpen[g] → f = g
+    ∀ {f g : TopologicalSpace X}, IsOpen[f] = IsOpen[g] → f = g
   | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl
 #align topological_space_eq TopologicalSpace.ext
 
 section
 
-variable [TopologicalSpace α]
+variable [TopologicalSpace X]
 
-@[simp] theorem isOpen_univ : IsOpen (univ : Set α) := TopologicalSpace.isOpen_univ
+@[simp] theorem isOpen_univ : IsOpen (univ : Set X) := TopologicalSpace.isOpen_univ
 #align is_open_univ isOpen_univ
 
 theorem IsOpen.inter (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∩ s₂) :=
   TopologicalSpace.isOpen_inter s₁ s₂ h₁ h₂
 #align is_open.inter IsOpen.inter
 
-theorem isOpen_sUnion {s : Set (Set α)} (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋃₀ s) :=
+theorem isOpen_sUnion {s : Set (Set X)} (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋃₀ s) :=
   TopologicalSpace.isOpen_sUnion s h
 #align is_open_sUnion isOpen_sUnion
 
 end
 
-protected theorem TopologicalSpace.ext_iff {t t' : TopologicalSpace α} :
+protected theorem TopologicalSpace.ext_iff {t t' : TopologicalSpace X} :
     t = t' ↔ ∀ s, IsOpen[t] s ↔ IsOpen[t'] s :=
   ⟨fun h s => h ▸ Iff.rfl, fun h => by ext; exact h _⟩
 #align topological_space_eq_iff TopologicalSpace.ext_iff
 
-theorem isOpen_fold {s : Set α} {t : TopologicalSpace α} : t.IsOpen s = IsOpen[t] s :=
+theorem isOpen_fold {s : Set X} {t : TopologicalSpace X} : t.IsOpen s = IsOpen[t] s :=
   rfl
 #align is_open_fold isOpen_fold
 
-variable [TopologicalSpace α]
+variable [TopologicalSpace X]
 
-theorem isOpen_iUnion {f : ι → Set α} (h : ∀ i, IsOpen (f i)) : IsOpen (⋃ i, f i) :=
+theorem isOpen_iUnion {f : ι → Set X} (h : ∀ i, IsOpen (f i)) : IsOpen (⋃ i, f i) :=
   isOpen_sUnion (forall_range_iff.2 h)
 #align is_open_Union isOpen_iUnion
 
-theorem isOpen_biUnion {s : Set β} {f : β → Set α} (h : ∀ i ∈ s, IsOpen (f i)) :
+theorem isOpen_biUnion {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) :
     IsOpen (⋃ i ∈ s, f i) :=
   isOpen_iUnion fun i => isOpen_iUnion fun hi => h i hi
 #align is_open_bUnion isOpen_biUnion
@@ -154,41 +155,41 @@ theorem IsOpen.union (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ 
   rw [union_eq_iUnion]; exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)
 #align is_open.union IsOpen.union
 
-lemma isOpen_iff_of_cover {ι : Type*} {f : ι → Set α} (ho : ∀ i, IsOpen (f i))
-    (hU : (⋃ i, f i) = univ) : IsOpen s ↔ ∀ i, IsOpen (f i ∩ s) := by
+lemma isOpen_iff_of_cover {f : α → Set X} (ho : ∀ i, IsOpen (f i)) (hU : (⋃ i, f i) = univ) :
+    IsOpen s ↔ ∀ i, IsOpen (f i ∩ s) := by
   refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩
   rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter]
   exact isOpen_iUnion fun i ↦ h i
 
-@[simp] theorem isOpen_empty : IsOpen (∅ : Set α) := by
+@[simp] theorem isOpen_empty : IsOpen (∅ : Set X) := by
   rw [← sUnion_empty]; exact isOpen_sUnion fun a => False.elim
 #align is_open_empty isOpen_empty
 
-theorem Set.Finite.isOpen_sInter {s : Set (Set α)} (hs : s.Finite) :
+theorem Set.Finite.isOpen_sInter {s : Set (Set X)} (hs : s.Finite) :
     (∀ t ∈ s, IsOpen t) → IsOpen (⋂₀ s) :=
   Finite.induction_on hs (fun _ => by rw [sInter_empty]; exact isOpen_univ) fun _ _ ih h => by
     simp only [sInter_insert, ball_insert_iff] at h ⊢
     exact h.1.inter (ih h.2)
 #align is_open_sInter Set.Finite.isOpen_sInter
 
-theorem Set.Finite.isOpen_biInter {s : Set β} {f : β → Set α} (hs : s.Finite)
+theorem Set.Finite.isOpen_biInter {s : Set α} {f : α → Set X} (hs : s.Finite)
     (h : ∀ i ∈ s, IsOpen (f i)) :
     IsOpen (⋂ i ∈ s, f i) :=
   sInter_image f s ▸ (hs.image _).isOpen_sInter (ball_image_iff.2 h)
 #align is_open_bInter Set.Finite.isOpen_biInter
 
-theorem isOpen_iInter_of_finite [Finite ι] {s : ι → Set α} (h : ∀ i, IsOpen (s i)) :
+theorem isOpen_iInter_of_finite [Finite ι] {s : ι → Set X} (h : ∀ i, IsOpen (s i)) :
     IsOpen (⋂ i, s i) :=
   (finite_range _).isOpen_sInter  (forall_range_iff.2 h)
 #align is_open_Inter isOpen_iInter_of_finite
 
-theorem isOpen_biInter_finset {s : Finset β} {f : β → Set α} (h : ∀ i ∈ s, IsOpen (f i)) :
+theorem isOpen_biInter_finset {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) :
     IsOpen (⋂ i ∈ s, f i) :=
   s.finite_toSet.isOpen_biInter h
 #align is_open_bInter_finset isOpen_biInter_finset
 
 @[simp] -- porting note: added `simp`
-theorem isOpen_const {p : Prop} : IsOpen { _a : α | p } := by by_cases p <;> simp [*]
+theorem isOpen_const {p : Prop} : IsOpen { _a : X | p } := by by_cases p <;> simp [*]
 #align is_open_const isOpen_const
 
 theorem IsOpen.and : IsOpen { a | p₁ a } → IsOpen { a | p₂ a } → IsOpen { a | p₁ a ∧ p₂ a } :=
@@ -196,7 +197,7 @@ theorem IsOpen.and : IsOpen { a | p₁ a } → IsOpen { a | p₂ a } → IsOpen
 #align is_open.and IsOpen.and
 
 /-- A set is closed if its complement is open -/
-class IsClosed (s : Set α) : Prop where
+class IsClosed (s : Set X) : Prop where
   /-- The complement of a closed set is an open set. -/
   isOpen_compl : IsOpen sᶜ
 #align is_closed IsClosed
@@ -205,45 +206,45 @@ set_option quotPrecheck false in
 /-- Notation for `IsClosed` with respect to a non-standard topology. -/
 scoped[Topology] notation (name := IsClosed_of) "IsClosed[" t "]" => @IsClosed _ t
 
-@[simp] theorem isOpen_compl_iff {s : Set α} : IsOpen sᶜ ↔ IsClosed s :=
+@[simp] theorem isOpen_compl_iff {s : Set X} : IsOpen sᶜ ↔ IsClosed s :=
   ⟨fun h => ⟨h⟩, fun h => h.isOpen_compl⟩
 #align is_open_compl_iff isOpen_compl_iff
 
 -- porting note: new lemma
-theorem isClosed_const {p : Prop} : IsClosed { _a : α | p } := ⟨isOpen_const (p := ¬p)⟩
+theorem isClosed_const {p : Prop} : IsClosed { _a : X | p } := ⟨isOpen_const (p := ¬p)⟩
 
-@[simp] theorem isClosed_empty : IsClosed (∅ : Set α) := isClosed_const
+@[simp] theorem isClosed_empty : IsClosed (∅ : Set X) := isClosed_const
 #align is_closed_empty isClosed_empty
 
-@[simp] theorem isClosed_univ : IsClosed (univ : Set α) := isClosed_const
+@[simp] theorem isClosed_univ : IsClosed (univ : Set X) := isClosed_const
 #align is_closed_univ isClosed_univ
 
 theorem IsClosed.union : IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂) := by
   simpa only [← isOpen_compl_iff, compl_union] using IsOpen.inter
 #align is_closed.union IsClosed.union
 
-theorem isClosed_sInter {s : Set (Set α)} : (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s) := by
+theorem isClosed_sInter {s : Set (Set X)} : (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s) := by
   simpa only [← isOpen_compl_iff, compl_sInter, sUnion_image] using isOpen_biUnion
 #align is_closed_sInter isClosed_sInter
 
-theorem isClosed_iInter {f : ι → Set α} (h : ∀ i, IsClosed (f i)) : IsClosed (⋂ i, f i) :=
+theorem isClosed_iInter {f : ι → Set X} (h : ∀ i, IsClosed (f i)) : IsClosed (⋂ i, f i) :=
   isClosed_sInter <| forall_range_iff.2 h
 #align is_closed_Inter isClosed_iInter
 
-theorem isClosed_biInter {s : Set β} {f : β → Set α} (h : ∀ i ∈ s, IsClosed (f i)) :
+theorem isClosed_biInter {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) :
     IsClosed (⋂ i ∈ s, f i) :=
   isClosed_iInter fun i => isClosed_iInter <| h i
 #align is_closed_bInter isClosed_biInter
 
 @[simp]
-theorem isClosed_compl_iff {s : Set α} : IsClosed sᶜ ↔ IsOpen s := by
+theorem isClosed_compl_iff {s : Set X} : IsClosed sᶜ ↔ IsOpen s := by
   rw [← isOpen_compl_iff, compl_compl]
 #align is_closed_compl_iff isClosed_compl_iff
 
 alias ⟨_, IsOpen.isClosed_compl⟩ := isClosed_compl_iff
 #align is_open.is_closed_compl IsOpen.isClosed_compl
 
-theorem IsOpen.sdiff {s t : Set α} (h₁ : IsOpen s) (h₂ : IsClosed t) : IsOpen (s \ t) :=
+theorem IsOpen.sdiff {s t : Set X} (h₁ : IsOpen s) (h₂ : IsClosed t) : IsOpen (s \ t) :=
   IsOpen.inter h₁ h₂.isOpen_compl
 #align is_open.sdiff IsOpen.sdiff
 
@@ -253,28 +254,28 @@ theorem IsClosed.inter (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) : IsClosed
   exact IsOpen.union h₁ h₂
 #align is_closed.inter IsClosed.inter
 
-theorem IsClosed.sdiff {s t : Set α} (h₁ : IsClosed s) (h₂ : IsOpen t) : IsClosed (s \ t) :=
+theorem IsClosed.sdiff {s t : Set X} (h₁ : IsClosed s) (h₂ : IsOpen t) : IsClosed (s \ t) :=
   IsClosed.inter h₁ (isClosed_compl_iff.mpr h₂)
 #align is_closed.sdiff IsClosed.sdiff
 
-theorem Set.Finite.isClosed_biUnion {s : Set β} {f : β → Set α} (hs : s.Finite)
+theorem Set.Finite.isClosed_biUnion {s : Set α} {f : α → Set X} (hs : s.Finite)
     (h : ∀ i ∈ s, IsClosed (f i)) :
     IsClosed (⋃ i ∈ s, f i) := by
   simp only [← isOpen_compl_iff, compl_iUnion] at *
   exact hs.isOpen_biInter h
 #align is_closed_bUnion Set.Finite.isClosed_biUnion
 
-lemma isClosed_biUnion_finset {s : Finset β} {f : β → Set α} (h : ∀ i ∈ s, IsClosed (f i)) :
+lemma isClosed_biUnion_finset {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) :
     IsClosed (⋃ i ∈ s, f i) :=
   s.finite_toSet.isClosed_biUnion h
 
-theorem isClosed_iUnion_of_finite [Finite ι] {s : ι → Set α} (h : ∀ i, IsClosed (s i)) :
+theorem isClosed_iUnion_of_finite [Finite ι] {s : ι → Set X} (h : ∀ i, IsClosed (s i)) :
     IsClosed (⋃ i, s i) := by
   simp only [← isOpen_compl_iff, compl_iUnion] at *
   exact isOpen_iInter_of_finite h
 #align is_closed_Union isClosed_iUnion_of_finite
 
-theorem isClosed_imp {p q : α → Prop} (hp : IsOpen { x | p x }) (hq : IsClosed { x | q x }) :
+theorem isClosed_imp {p q : X → Prop} (hp : IsOpen { x | p x }) (hq : IsClosed { x | q x }) :
     IsClosed { x | p x → q x } := by
   simpa only [imp_iff_not_or] using hp.isClosed_compl.union hq
 #align is_closed_imp isClosed_imp
@@ -288,45 +289,45 @@ theorem IsClosed.not : IsClosed { a | p a } → IsOpen { a | ¬p a } :=
 -/
 
 /-- The interior of a set `s` is the largest open subset of `s`. -/
-def interior (s : Set α) : Set α :=
+def interior (s : Set X) : Set X :=
   ⋃₀ { t | IsOpen t ∧ t ⊆ s }
 #align interior interior
 
 -- porting note: use `∃ t, t ⊆ s ∧ _` instead of `∃ t ⊆ s, _`
-theorem mem_interior {s : Set α} {x : α} : x ∈ interior s ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := by
+theorem mem_interior {s : Set X} {x : X} : x ∈ interior s ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := by
   simp only [interior, mem_sUnion, mem_setOf_eq, and_assoc, and_left_comm]
 #align mem_interior mem_interiorₓ
 
 @[simp]
-theorem isOpen_interior {s : Set α} : IsOpen (interior s) :=
+theorem isOpen_interior {s : Set X} : IsOpen (interior s) :=
   isOpen_sUnion fun _ => And.left
 #align is_open_interior isOpen_interior
 
-theorem interior_subset {s : Set α} : interior s ⊆ s :=
+theorem interior_subset {s : Set X} : interior s ⊆ s :=
   sUnion_subset fun _ => And.right
 #align interior_subset interior_subset
 
-theorem interior_maximal {s t : Set α} (h₁ : t ⊆ s) (h₂ : IsOpen t) : t ⊆ interior s :=
+theorem interior_maximal {s t : Set X} (h₁ : t ⊆ s) (h₂ : IsOpen t) : t ⊆ interior s :=
   subset_sUnion_of_mem ⟨h₂, h₁⟩
 #align interior_maximal interior_maximal
 
-theorem IsOpen.interior_eq {s : Set α} (h : IsOpen s) : interior s = s :=
+theorem IsOpen.interior_eq {s : Set X} (h : IsOpen s) : interior s = s :=
   interior_subset.antisymm (interior_maximal (Subset.refl s) h)
 #align is_open.interior_eq IsOpen.interior_eq
 
-theorem interior_eq_iff_isOpen {s : Set α} : interior s = s ↔ IsOpen s :=
+theorem interior_eq_iff_isOpen {s : Set X} : interior s = s ↔ IsOpen s :=
   ⟨fun h => h ▸ isOpen_interior, IsOpen.interior_eq⟩
 #align interior_eq_iff_is_open interior_eq_iff_isOpen
 
-theorem subset_interior_iff_isOpen {s : Set α} : s ⊆ interior s ↔ IsOpen s := by
+theorem subset_interior_iff_isOpen {s : Set X} : s ⊆ interior s ↔ IsOpen s := by
   simp only [interior_eq_iff_isOpen.symm, Subset.antisymm_iff, interior_subset, true_and]
 #align subset_interior_iff_is_open subset_interior_iff_isOpen
 
-theorem IsOpen.subset_interior_iff {s t : Set α} (h₁ : IsOpen s) : s ⊆ interior t ↔ s ⊆ t :=
+theorem IsOpen.subset_interior_iff {s t : Set X} (h₁ : IsOpen s) : s ⊆ interior t ↔ s ⊆ t :=
   ⟨fun h => Subset.trans h interior_subset, fun h₂ => interior_maximal h₂ h₁⟩
 #align is_open.subset_interior_iff IsOpen.subset_interior_iff
 
-theorem subset_interior_iff {s t : Set α} : t ⊆ interior s ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s :=
+theorem subset_interior_iff {s t : Set X} : t ⊆ interior s ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s :=
   ⟨fun h => ⟨interior s, isOpen_interior, h, interior_subset⟩, fun ⟨_U, hU, htU, hUs⟩ =>
     htU.trans (interior_maximal hUs hU)⟩
 #align subset_interior_iff subset_interior_iff
@@ -335,58 +336,58 @@ lemma interior_subset_iff : interior s ⊆ t ↔ ∀ U, IsOpen U → U ⊆ s →
   simp [interior]
 
 @[mono]
-theorem interior_mono {s t : Set α} (h : s ⊆ t) : interior s ⊆ interior t :=
+theorem interior_mono {s t : Set X} (h : s ⊆ t) : interior s ⊆ interior t :=
   interior_maximal (Subset.trans interior_subset h) isOpen_interior
 #align interior_mono interior_mono
 
 @[simp]
-theorem interior_empty : interior (∅ : Set α) = ∅ :=
+theorem interior_empty : interior (∅ : Set X) = ∅ :=
   isOpen_empty.interior_eq
 #align interior_empty interior_empty
 
 @[simp]
-theorem interior_univ : interior (univ : Set α) = univ :=
+theorem interior_univ : interior (univ : Set X) = univ :=
   isOpen_univ.interior_eq
 #align interior_univ interior_univ
 
 @[simp]
-theorem interior_eq_univ {s : Set α} : interior s = univ ↔ s = univ :=
+theorem interior_eq_univ {s : Set X} : interior s = univ ↔ s = univ :=
   ⟨fun h => univ_subset_iff.mp <| h.symm.trans_le interior_subset, fun h => h.symm ▸ interior_univ⟩
 #align interior_eq_univ interior_eq_univ
 
 @[simp]
-theorem interior_interior {s : Set α} : interior (interior s) = interior s :=
+theorem interior_interior {s : Set X} : interior (interior s) = interior s :=
   isOpen_interior.interior_eq
 #align interior_interior interior_interior
 
 @[simp]
-theorem interior_inter {s t : Set α} : interior (s ∩ t) = interior s ∩ interior t :=
+theorem interior_inter {s t : Set X} : interior (s ∩ t) = interior s ∩ interior t :=
   (Monotone.map_inf_le (fun _ _ ↦ interior_mono) s t).antisymm <|
     interior_maximal (inter_subset_inter interior_subset interior_subset) <|
       isOpen_interior.inter isOpen_interior
 #align interior_inter interior_inter
 
-theorem Set.Finite.interior_biInter {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set α) :
+theorem Set.Finite.interior_biInter {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set X) :
     interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i) :=
   hs.induction_on (by simp) <| by intros; simp [*]
 
-theorem Set.Finite.interior_sInter {S : Set (Set α)} (hS : S.Finite) :
+theorem Set.Finite.interior_sInter {S : Set (Set X)} (hS : S.Finite) :
     interior (⋂₀ S) = ⋂ s ∈ S, interior s := by
   rw [sInter_eq_biInter, hS.interior_biInter]
 
 @[simp]
-theorem Finset.interior_iInter {ι : Type*} (s : Finset ι) (f : ι → Set α) :
+theorem Finset.interior_iInter {ι : Type*} (s : Finset ι) (f : ι → Set X) :
     interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i) :=
   s.finite_toSet.interior_biInter f
 #align finset.interior_Inter Finset.interior_iInter
 
 @[simp]
-theorem interior_iInter_of_finite [Finite ι] (f : ι → Set α) :
+theorem interior_iInter_of_finite [Finite ι] (f : ι → Set X) :
     interior (⋂ i, f i) = ⋂ i, interior (f i) := by
   rw [← sInter_range, (finite_range f).interior_sInter, biInter_range]
 #align interior_Inter interior_iInter_of_finite
 
-theorem interior_union_isClosed_of_interior_empty {s t : Set α} (h₁ : IsClosed s)
+theorem interior_union_isClosed_of_interior_empty {s t : Set X} (h₁ : IsClosed s)
     (h₂ : interior t = ∅) : interior (s ∪ t) = interior s :=
   have : interior (s ∪ t) ⊆ s := fun x ⟨u, ⟨(hu₁ : IsOpen u), (hu₂ : u ⊆ s ∪ t)⟩, (hx₁ : x ∈ u)⟩ =>
     by_contradiction fun hx₂ : x ∉ s =>
@@ -402,16 +403,16 @@ theorem isOpen_iff_forall_mem_open : IsOpen s ↔ ∀ x ∈ s, ∃ t, t ⊆ s 
   simp only [subset_def, mem_interior]
 #align is_open_iff_forall_mem_open isOpen_iff_forall_mem_open
 
-theorem interior_iInter_subset (s : ι → Set α) : interior (⋂ i, s i) ⊆ ⋂ i, interior (s i) :=
+theorem interior_iInter_subset (s : ι → Set X) : interior (⋂ i, s i) ⊆ ⋂ i, interior (s i) :=
   subset_iInter fun _ => interior_mono <| iInter_subset _ _
 #align interior_Inter_subset interior_iInter_subset
 
-theorem interior_iInter₂_subset (p : ι → Sort*) (s : ∀ i, p i → Set α) :
+theorem interior_iInter₂_subset (p : ι → Sort*) (s : ∀ i, p i → Set X) :
     interior (⋂ (i) (j), s i j) ⊆ ⋂ (i) (j), interior (s i j) :=
   (interior_iInter_subset _).trans <| iInter_mono fun _ => interior_iInter_subset _
 #align interior_Inter₂_subset interior_iInter₂_subset
 
-theorem interior_sInter_subset (S : Set (Set α)) : interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s :=
+theorem interior_sInter_subset (S : Set (Set X)) : interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s :=
   calc
     interior (⋂₀ S) = interior (⋂ s ∈ S, s) := by rw [sInter_eq_biInter]
     _ ⊆ ⋂ s ∈ S, interior s := interior_iInter₂_subset _ _
@@ -423,7 +424,7 @@ theorem interior_sInter_subset (S : Set (Set α)) : interior (⋂₀ S) ⊆ ⋂
 
 
 /-- The closure of `s` is the smallest closed set containing `s`. -/
-def closure (s : Set α) : Set α :=
+def closure (s : Set X) : Set X :=
   ⋂₀ { t | IsClosed t ∧ s ⊆ t }
 #align closure closure
 
@@ -432,91 +433,91 @@ set_option quotPrecheck false in
 scoped[Topology] notation (name := closure_of) "closure[" t "]" => @closure _ t
 
 @[simp]
-theorem isClosed_closure {s : Set α} : IsClosed (closure s) :=
+theorem isClosed_closure {s : Set X} : IsClosed (closure s) :=
   isClosed_sInter fun _ => And.left
 #align is_closed_closure isClosed_closure
 
-theorem subset_closure {s : Set α} : s ⊆ closure s :=
+theorem subset_closure {s : Set X} : s ⊆ closure s :=
   subset_sInter fun _ => And.right
 #align subset_closure subset_closure
 
-theorem not_mem_of_not_mem_closure {s : Set α} {P : α} (hP : P ∉ closure s) : P ∉ s := fun h =>
+theorem not_mem_of_not_mem_closure {s : Set X} {P : X} (hP : P ∉ closure s) : P ∉ s := fun h =>
   hP (subset_closure h)
 #align not_mem_of_not_mem_closure not_mem_of_not_mem_closure
 
-theorem closure_minimal {s t : Set α} (h₁ : s ⊆ t) (h₂ : IsClosed t) : closure s ⊆ t :=
+theorem closure_minimal {s t : Set X} (h₁ : s ⊆ t) (h₂ : IsClosed t) : closure s ⊆ t :=
   sInter_subset_of_mem ⟨h₂, h₁⟩
 #align closure_minimal closure_minimal
 
-theorem Disjoint.closure_left {s t : Set α} (hd : Disjoint s t) (ht : IsOpen t) :
+theorem Disjoint.closure_left {s t : Set X} (hd : Disjoint s t) (ht : IsOpen t) :
     Disjoint (closure s) t :=
   disjoint_compl_left.mono_left <| closure_minimal hd.subset_compl_right ht.isClosed_compl
 #align disjoint.closure_left Disjoint.closure_left
 
-theorem Disjoint.closure_right {s t : Set α} (hd : Disjoint s t) (hs : IsOpen s) :
+theorem Disjoint.closure_right {s t : Set X} (hd : Disjoint s t) (hs : IsOpen s) :
     Disjoint s (closure t) :=
   (hd.symm.closure_left hs).symm
 #align disjoint.closure_right Disjoint.closure_right
 
-theorem IsClosed.closure_eq {s : Set α} (h : IsClosed s) : closure s = s :=
+theorem IsClosed.closure_eq {s : Set X} (h : IsClosed s) : closure s = s :=
   Subset.antisymm (closure_minimal (Subset.refl s) h) subset_closure
 #align is_closed.closure_eq IsClosed.closure_eq
 
-theorem IsClosed.closure_subset {s : Set α} (hs : IsClosed s) : closure s ⊆ s :=
+theorem IsClosed.closure_subset {s : Set X} (hs : IsClosed s) : closure s ⊆ s :=
   closure_minimal (Subset.refl _) hs
 #align is_closed.closure_subset IsClosed.closure_subset
 
-theorem IsClosed.closure_subset_iff {s t : Set α} (h₁ : IsClosed t) : closure s ⊆ t ↔ s ⊆ t :=
+theorem IsClosed.closure_subset_iff {s t : Set X} (h₁ : IsClosed t) : closure s ⊆ t ↔ s ⊆ t :=
   ⟨Subset.trans subset_closure, fun h => closure_minimal h h₁⟩
 #align is_closed.closure_subset_iff IsClosed.closure_subset_iff
 
-theorem IsClosed.mem_iff_closure_subset {s : Set α} (hs : IsClosed s) {x : α} :
-    x ∈ s ↔ closure ({x} : Set α) ⊆ s :=
+theorem IsClosed.mem_iff_closure_subset {s : Set X} (hs : IsClosed s) {x : X} :
+    x ∈ s ↔ closure ({x} : Set X) ⊆ s :=
   (hs.closure_subset_iff.trans Set.singleton_subset_iff).symm
 #align is_closed.mem_iff_closure_subset IsClosed.mem_iff_closure_subset
 
 @[mono]
-theorem closure_mono {s t : Set α} (h : s ⊆ t) : closure s ⊆ closure t :=
+theorem closure_mono {s t : Set X} (h : s ⊆ t) : closure s ⊆ closure t :=
   closure_minimal (Subset.trans h subset_closure) isClosed_closure
 #align closure_mono closure_mono
 
-theorem monotone_closure (α : Type*) [TopologicalSpace α] : Monotone (@closure α _) := fun _ _ =>
+theorem monotone_closure (X : Type*) [TopologicalSpace X] : Monotone (@closure X _) := fun _ _ =>
   closure_mono
 #align monotone_closure monotone_closure
 
-theorem diff_subset_closure_iff {s t : Set α} : s \ t ⊆ closure t ↔ s ⊆ closure t := by
+theorem diff_subset_closure_iff {s t : Set X} : s \ t ⊆ closure t ↔ s ⊆ closure t := by
   rw [diff_subset_iff, union_eq_self_of_subset_left subset_closure]
 #align diff_subset_closure_iff diff_subset_closure_iff
 
-theorem closure_inter_subset_inter_closure (s t : Set α) :
+theorem closure_inter_subset_inter_closure (s t : Set X) :
     closure (s ∩ t) ⊆ closure s ∩ closure t :=
-  (monotone_closure α).map_inf_le s t
+  (monotone_closure X).map_inf_le s t
 #align closure_inter_subset_inter_closure closure_inter_subset_inter_closure
 
-theorem isClosed_of_closure_subset {s : Set α} (h : closure s ⊆ s) : IsClosed s := by
+theorem isClosed_of_closure_subset {s : Set X} (h : closure s ⊆ s) : IsClosed s := by
   rw [subset_closure.antisymm h]; exact isClosed_closure
 #align is_closed_of_closure_subset isClosed_of_closure_subset
 
-theorem closure_eq_iff_isClosed {s : Set α} : closure s = s ↔ IsClosed s :=
+theorem closure_eq_iff_isClosed {s : Set X} : closure s = s ↔ IsClosed s :=
   ⟨fun h => h ▸ isClosed_closure, IsClosed.closure_eq⟩
 #align closure_eq_iff_is_closed closure_eq_iff_isClosed
 
-theorem closure_subset_iff_isClosed {s : Set α} : closure s ⊆ s ↔ IsClosed s :=
+theorem closure_subset_iff_isClosed {s : Set X} : closure s ⊆ s ↔ IsClosed s :=
   ⟨isClosed_of_closure_subset, IsClosed.closure_subset⟩
 #align closure_subset_iff_is_closed closure_subset_iff_isClosed
 
 @[simp]
-theorem closure_empty : closure (∅ : Set α) = ∅ :=
+theorem closure_empty : closure (∅ : Set X) = ∅ :=
   isClosed_empty.closure_eq
 #align closure_empty closure_empty
 
 @[simp]
-theorem closure_empty_iff (s : Set α) : closure s = ∅ ↔ s = ∅ :=
+theorem closure_empty_iff (s : Set X) : closure s = ∅ ↔ s = ∅ :=
   ⟨subset_eq_empty subset_closure, fun h => h.symm ▸ closure_empty⟩
 #align closure_empty_iff closure_empty_iff
 
 @[simp]
-theorem closure_nonempty_iff {s : Set α} : (closure s).Nonempty ↔ s.Nonempty := by
+theorem closure_nonempty_iff {s : Set X} : (closure s).Nonempty ↔ s.Nonempty := by
   simp only [nonempty_iff_ne_empty, Ne.def, closure_empty_iff]
 #align closure_nonempty_iff closure_nonempty_iff
 
@@ -525,60 +526,60 @@ alias ⟨Set.Nonempty.of_closure, Set.Nonempty.closure⟩ := closure_nonempty_if
 #align set.nonempty.closure Set.Nonempty.closure
 
 @[simp]
-theorem closure_univ : closure (univ : Set α) = univ :=
+theorem closure_univ : closure (univ : Set X) = univ :=
   isClosed_univ.closure_eq
 #align closure_univ closure_univ
 
 @[simp]
-theorem closure_closure {s : Set α} : closure (closure s) = closure s :=
+theorem closure_closure {s : Set X} : closure (closure s) = closure s :=
   isClosed_closure.closure_eq
 #align closure_closure closure_closure
 
-theorem closure_eq_compl_interior_compl {s : Set α} : closure s = (interior sᶜ)ᶜ := by
+theorem closure_eq_compl_interior_compl {s : Set X} : closure s = (interior sᶜ)ᶜ := by
   rw [interior, closure, compl_sUnion, compl_image_set_of]
   simp only [compl_subset_compl, isOpen_compl_iff]
 #align closure_eq_compl_interior_compl closure_eq_compl_interior_compl
 
 @[simp]
-theorem closure_union {s t : Set α} : closure (s ∪ t) = closure s ∪ closure t := by
+theorem closure_union {s t : Set X} : closure (s ∪ t) = closure s ∪ closure t := by
   simp [closure_eq_compl_interior_compl, compl_inter]
 #align closure_union closure_union
 
-theorem Set.Finite.closure_biUnion {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set α) :
+theorem Set.Finite.closure_biUnion {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set X) :
     closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i) := by
   simp [closure_eq_compl_interior_compl, hs.interior_biInter]
 
-theorem Set.Finite.closure_sUnion {S : Set (Set α)} (hS : S.Finite) :
+theorem Set.Finite.closure_sUnion {S : Set (Set X)} (hS : S.Finite) :
     closure (⋃₀ S) = ⋃ s ∈ S, closure s := by
   rw [sUnion_eq_biUnion, hS.closure_biUnion]
 
 @[simp]
-theorem Finset.closure_biUnion {ι : Type*} (s : Finset ι) (f : ι → Set α) :
+theorem Finset.closure_biUnion {ι : Type*} (s : Finset ι) (f : ι → Set X) :
     closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i) :=
   s.finite_toSet.closure_biUnion f
 #align finset.closure_bUnion Finset.closure_biUnion
 
 @[simp]
-theorem closure_iUnion_of_finite [Finite ι] (f : ι → Set α) :
+theorem closure_iUnion_of_finite [Finite ι] (f : ι → Set X) :
     closure (⋃ i, f i) = ⋃ i, closure (f i) := by
   rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range]
 #align closure_Union closure_iUnion_of_finite
 
-theorem interior_subset_closure {s : Set α} : interior s ⊆ closure s :=
+theorem interior_subset_closure {s : Set X} : interior s ⊆ closure s :=
   Subset.trans interior_subset subset_closure
 #align interior_subset_closure interior_subset_closure
 
 @[simp]
-theorem interior_compl {s : Set α} : interior sᶜ = (closure s)ᶜ := by
+theorem interior_compl {s : Set X} : interior sᶜ = (closure s)ᶜ := by
   simp [closure_eq_compl_interior_compl]
 #align interior_compl interior_compl
 
 @[simp]
-theorem closure_compl {s : Set α} : closure sᶜ = (interior s)ᶜ := by
+theorem closure_compl {s : Set X} : closure sᶜ = (interior s)ᶜ := by
   simp [closure_eq_compl_interior_compl]
 #align closure_compl closure_compl
 
-theorem mem_closure_iff {s : Set α} {a : α} :
+theorem mem_closure_iff {s : Set X} {a : X} :
     a ∈ closure s ↔ ∀ o, IsOpen o → a ∈ o → (o ∩ s).Nonempty :=
   ⟨fun h o oo ao =>
     by_contradiction fun os =>
@@ -590,56 +591,56 @@ theorem mem_closure_iff {s : Set α} {a : α} :
       hc (h₂ hs)⟩
 #align mem_closure_iff mem_closure_iff
 
-theorem closure_inter_open_nonempty_iff {s t : Set α} (h : IsOpen t) :
+theorem closure_inter_open_nonempty_iff {s t : Set X} (h : IsOpen t) :
     (closure s ∩ t).Nonempty ↔ (s ∩ t).Nonempty :=
   ⟨fun ⟨_x, hxcs, hxt⟩ => inter_comm t s ▸ mem_closure_iff.1 hxcs t h hxt, fun h =>
     h.mono <| inf_le_inf_right t subset_closure⟩
 #align closure_inter_open_nonempty_iff closure_inter_open_nonempty_iff
 
-theorem Filter.le_lift'_closure (l : Filter α) : l ≤ l.lift' closure :=
+theorem Filter.le_lift'_closure (l : Filter X) : l ≤ l.lift' closure :=
   le_lift'.2 fun _ h => mem_of_superset h subset_closure
 #align filter.le_lift'_closure Filter.le_lift'_closure
 
-theorem Filter.HasBasis.lift'_closure {l : Filter α} {p : ι → Prop} {s : ι → Set α}
+theorem Filter.HasBasis.lift'_closure {l : Filter X} {p : ι → Prop} {s : ι → Set X}
     (h : l.HasBasis p s) : (l.lift' closure).HasBasis p fun i => closure (s i) :=
-  h.lift' (monotone_closure α)
+  h.lift' (monotone_closure X)
 #align filter.has_basis.lift'_closure Filter.HasBasis.lift'_closure
 
-theorem Filter.HasBasis.lift'_closure_eq_self {l : Filter α} {p : ι → Prop} {s : ι → Set α}
+theorem Filter.HasBasis.lift'_closure_eq_self {l : Filter X} {p : ι → Prop} {s : ι → Set X}
     (h : l.HasBasis p s) (hc : ∀ i, p i → IsClosed (s i)) : l.lift' closure = l :=
   le_antisymm (h.ge_iff.2 fun i hi => (hc i hi).closure_eq ▸ mem_lift' (h.mem_of_mem hi))
     l.le_lift'_closure
 #align filter.has_basis.lift'_closure_eq_self Filter.HasBasis.lift'_closure_eq_self
 
 @[simp]
-theorem Filter.lift'_closure_eq_bot {l : Filter α} : l.lift' closure = ⊥ ↔ l = ⊥ :=
+theorem Filter.lift'_closure_eq_bot {l : Filter X} : l.lift' closure = ⊥ ↔ l = ⊥ :=
   ⟨fun h => bot_unique <| h ▸ l.le_lift'_closure, fun h =>
     h.symm ▸ by rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]⟩
 #align filter.lift'_closure_eq_bot Filter.lift'_closure_eq_bot
 
 /-- A set is dense in a topological space if every point belongs to its closure. -/
-def Dense (s : Set α) : Prop :=
+def Dense (s : Set X) : Prop :=
   ∀ x, x ∈ closure s
 #align dense Dense
 
-theorem dense_iff_closure_eq {s : Set α} : Dense s ↔ closure s = univ :=
+theorem dense_iff_closure_eq {s : Set X} : Dense s ↔ closure s = univ :=
   eq_univ_iff_forall.symm
 #align dense_iff_closure_eq dense_iff_closure_eq
 
 alias ⟨Dense.closure_eq, _⟩ := dense_iff_closure_eq
 #align dense.closure_eq Dense.closure_eq
 
-theorem interior_eq_empty_iff_dense_compl {s : Set α} : interior s = ∅ ↔ Dense sᶜ := by
+theorem interior_eq_empty_iff_dense_compl {s : Set X} : interior s = ∅ ↔ Dense sᶜ := by
   rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]
 #align interior_eq_empty_iff_dense_compl interior_eq_empty_iff_dense_compl
 
-theorem Dense.interior_compl {s : Set α} (h : Dense s) : interior sᶜ = ∅ :=
+theorem Dense.interior_compl {s : Set X} (h : Dense s) : interior sᶜ = ∅ :=
   interior_eq_empty_iff_dense_compl.2 <| by rwa [compl_compl]
 #align dense.interior_compl Dense.interior_compl
 
 /-- The closure of a set `s` is dense if and only if `s` is dense. -/
 @[simp]
-theorem dense_closure {s : Set α} : Dense (closure s) ↔ Dense s := by
+theorem dense_closure {s : Set X} : Dense (closure s) ↔ Dense s := by
   rw [Dense, Dense, closure_closure]
 #align dense_closure dense_closure
 
@@ -649,11 +650,11 @@ alias ⟨Dense.of_closure, _⟩ := dense_closure
 #align dense.closure Dense.closure
 
 @[simp]
-theorem dense_univ : Dense (univ : Set α) := fun _ => subset_closure trivial
+theorem dense_univ : Dense (univ : Set X) := fun _ => subset_closure trivial
 #align dense_univ dense_univ
 
 /-- A set is dense if and only if it has a nonempty intersection with each nonempty open set. -/
-theorem dense_iff_inter_open {s : Set α} :
+theorem dense_iff_inter_open {s : Set X} :
     Dense s ↔ ∀ U, IsOpen U → U.Nonempty → (U ∩ s).Nonempty := by
   constructor <;> intro h
   · rintro U U_op ⟨x, x_in⟩
@@ -667,30 +668,30 @@ theorem dense_iff_inter_open {s : Set α} :
 alias ⟨Dense.inter_open_nonempty, _⟩ := dense_iff_inter_open
 #align dense.inter_open_nonempty Dense.inter_open_nonempty
 
-theorem Dense.exists_mem_open {s : Set α} (hs : Dense s) {U : Set α} (ho : IsOpen U)
+theorem Dense.exists_mem_open {s : Set X} (hs : Dense s) {U : Set X} (ho : IsOpen U)
     (hne : U.Nonempty) : ∃ x ∈ s, x ∈ U :=
   let ⟨x, hx⟩ := hs.inter_open_nonempty U ho hne
   ⟨x, hx.2, hx.1⟩
 #align dense.exists_mem_open Dense.exists_mem_open
 
-theorem Dense.nonempty_iff {s : Set α} (hs : Dense s) : s.Nonempty ↔ Nonempty α :=
+theorem Dense.nonempty_iff {s : Set X} (hs : Dense s) : s.Nonempty ↔ Nonempty X :=
   ⟨fun ⟨x, _⟩ => ⟨x⟩, fun ⟨x⟩ =>
     let ⟨y, hy⟩ := hs.inter_open_nonempty _ isOpen_univ ⟨x, trivial⟩
     ⟨y, hy.2⟩⟩
 #align dense.nonempty_iff Dense.nonempty_iff
 
-theorem Dense.nonempty [h : Nonempty α] {s : Set α} (hs : Dense s) : s.Nonempty :=
+theorem Dense.nonempty [h : Nonempty X] {s : Set X} (hs : Dense s) : s.Nonempty :=
   hs.nonempty_iff.2 h
 #align dense.nonempty Dense.nonempty
 
 @[mono]
-theorem Dense.mono {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) (hd : Dense s₁) : Dense s₂ := fun x =>
+theorem Dense.mono {s₁ s₂ : Set X} (h : s₁ ⊆ s₂) (hd : Dense s₁) : Dense s₂ := fun x =>
   closure_mono h (hd x)
 #align dense.mono Dense.mono
 
 /-- Complement to a singleton is dense if and only if the singleton is not an open set. -/
-theorem dense_compl_singleton_iff_not_open {x : α} :
-    Dense ({x}ᶜ : Set α) ↔ ¬IsOpen ({x} : Set α) := by
+theorem dense_compl_singleton_iff_not_open {x : X} :
+    Dense ({x}ᶜ : Set X) ↔ ¬IsOpen ({x} : Set X) := by
   constructor
   · intro hd ho
     exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)
@@ -705,12 +706,12 @@ theorem dense_compl_singleton_iff_not_open {x : α} :
 -/
 
 /-- The frontier of a set is the set of points between the closure and interior. -/
-def frontier (s : Set α) : Set α :=
+def frontier (s : Set X) : Set X :=
   closure s \ interior s
 #align frontier frontier
 
 @[simp]
-theorem closure_diff_interior (s : Set α) : closure s \ interior s = frontier s :=
+theorem closure_diff_interior (s : Set X) : closure s \ interior s = frontier s :=
   rfl
 #align closure_diff_interior closure_diff_interior
 
@@ -720,21 +721,21 @@ lemma disjoint_interior_frontier : Disjoint (interior s) (frontier s) := by
     ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]
 
 @[simp]
-theorem closure_diff_frontier (s : Set α) : closure s \ frontier s = interior s := by
+theorem closure_diff_frontier (s : Set X) : closure s \ frontier s = interior s := by
   rw [frontier, diff_diff_right_self, inter_eq_self_of_subset_right interior_subset_closure]
 #align closure_diff_frontier closure_diff_frontier
 
 @[simp]
-theorem self_diff_frontier (s : Set α) : s \ frontier s = interior s := by
+theorem self_diff_frontier (s : Set X) : s \ frontier s = interior s := by
   rw [frontier, diff_diff_right, diff_eq_empty.2 subset_closure,
     inter_eq_self_of_subset_right interior_subset, empty_union]
 #align self_diff_frontier self_diff_frontier
 
-theorem frontier_eq_closure_inter_closure {s : Set α} : frontier s = closure s ∩ closure sᶜ := by
+theorem frontier_eq_closure_inter_closure {s : Set X} : frontier s = closure s ∩ closure sᶜ := by
   rw [closure_compl, frontier, diff_eq]
 #align frontier_eq_closure_inter_closure frontier_eq_closure_inter_closure
 
-theorem frontier_subset_closure {s : Set α} : frontier s ⊆ closure s :=
+theorem frontier_subset_closure {s : Set X} : frontier s ⊆ closure s :=
   diff_subset _ _
 #align frontier_subset_closure frontier_subset_closure
 
@@ -742,59 +743,59 @@ theorem IsClosed.frontier_subset (hs : IsClosed s) : frontier s ⊆ s :=
   frontier_subset_closure.trans hs.closure_eq.subset
 #align is_closed.frontier_subset IsClosed.frontier_subset
 
-theorem frontier_closure_subset {s : Set α} : frontier (closure s) ⊆ frontier s :=
+theorem frontier_closure_subset {s : Set X} : frontier (closure s) ⊆ frontier s :=
   diff_subset_diff closure_closure.subset <| interior_mono subset_closure
 #align frontier_closure_subset frontier_closure_subset
 
-theorem frontier_interior_subset {s : Set α} : frontier (interior s) ⊆ frontier s :=
+theorem frontier_interior_subset {s : Set X} : frontier (interior s) ⊆ frontier s :=
   diff_subset_diff (closure_mono interior_subset) interior_interior.symm.subset
 #align frontier_interior_subset frontier_interior_subset
 
 /-- The complement of a set has the same frontier as the original set. -/
 @[simp]
-theorem frontier_compl (s : Set α) : frontier sᶜ = frontier s := by
+theorem frontier_compl (s : Set X) : frontier sᶜ = frontier s := by
   simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm]
 #align frontier_compl frontier_compl
 
 @[simp]
-theorem frontier_univ : frontier (univ : Set α) = ∅ := by simp [frontier]
+theorem frontier_univ : frontier (univ : Set X) = ∅ := by simp [frontier]
 #align frontier_univ frontier_univ
 
 @[simp]
-theorem frontier_empty : frontier (∅ : Set α) = ∅ := by simp [frontier]
+theorem frontier_empty : frontier (∅ : Set X) = ∅ := by simp [frontier]
 #align frontier_empty frontier_empty
 
-theorem frontier_inter_subset (s t : Set α) :
+theorem frontier_inter_subset (s t : Set X) :
     frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t := by
   simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union]
   refine' (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq _
   simp only [inter_distrib_left, inter_distrib_right, inter_assoc, inter_comm (closure t)]
 #align frontier_inter_subset frontier_inter_subset
 
-theorem frontier_union_subset (s t : Set α) :
+theorem frontier_union_subset (s t : Set X) :
     frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t := by
   simpa only [frontier_compl, ← compl_union] using frontier_inter_subset sᶜ tᶜ
 #align frontier_union_subset frontier_union_subset
 
-theorem IsClosed.frontier_eq {s : Set α} (hs : IsClosed s) : frontier s = s \ interior s := by
+theorem IsClosed.frontier_eq {s : Set X} (hs : IsClosed s) : frontier s = s \ interior s := by
   rw [frontier, hs.closure_eq]
 #align is_closed.frontier_eq IsClosed.frontier_eq
 
-theorem IsOpen.frontier_eq {s : Set α} (hs : IsOpen s) : frontier s = closure s \ s := by
+theorem IsOpen.frontier_eq {s : Set X} (hs : IsOpen s) : frontier s = closure s \ s := by
   rw [frontier, hs.interior_eq]
 #align is_open.frontier_eq IsOpen.frontier_eq
 
-theorem IsOpen.inter_frontier_eq {s : Set α} (hs : IsOpen s) : s ∩ frontier s = ∅ := by
+theorem IsOpen.inter_frontier_eq {s : Set X} (hs : IsOpen s) : s ∩ frontier s = ∅ := by
   rw [hs.frontier_eq, inter_diff_self]
 #align is_open.inter_frontier_eq IsOpen.inter_frontier_eq
 
 /-- The frontier of a set is closed. -/
-theorem isClosed_frontier {s : Set α} : IsClosed (frontier s) := by
+theorem isClosed_frontier {s : Set X} : IsClosed (frontier s) := by
   rw [frontier_eq_closure_inter_closure]; exact IsClosed.inter isClosed_closure isClosed_closure
 #align is_closed_frontier isClosed_frontier
 
 /-- The frontier of a closed set has no interior point. -/
-theorem interior_frontier {s : Set α} (h : IsClosed s) : interior (frontier s) = ∅ := by
+theorem interior_frontier {s : Set X} (h : IsClosed s) : interior (frontier s) = ∅ := by
   have A : frontier s = s \ interior s := h.frontier_eq
   have B : interior (frontier s) ⊆ interior s := by rw [A]; exact interior_mono (diff_subset _ _)
   have C : interior (frontier s) ⊆ frontier s := interior_subset
@@ -803,11 +804,11 @@ theorem interior_frontier {s : Set α} (h : IsClosed s) : interior (frontier s)
   rwa [inter_diff_self, subset_empty_iff] at this
 #align interior_frontier interior_frontier
 
-theorem closure_eq_interior_union_frontier (s : Set α) : closure s = interior s ∪ frontier s :=
+theorem closure_eq_interior_union_frontier (s : Set X) : closure s = interior s ∪ frontier s :=
   (union_diff_cancel interior_subset_closure).symm
 #align closure_eq_interior_union_frontier closure_eq_interior_union_frontier
 
-theorem closure_eq_self_union_frontier (s : Set α) : closure s = s ∪ frontier s :=
+theorem closure_eq_self_union_frontier (s : Set X) : closure s = s ∪ frontier s :=
   (union_diff_cancel' interior_subset subset_closure).symm
 #align closure_eq_self_union_frontier closure_eq_self_union_frontier
 
@@ -820,12 +821,12 @@ theorem Disjoint.frontier_right (hs : IsOpen s) (hd : Disjoint s t) : Disjoint s
   (hd.symm.frontier_left hs).symm
 #align disjoint.frontier_right Disjoint.frontier_right
 
-theorem frontier_eq_inter_compl_interior {s : Set α} :
+theorem frontier_eq_inter_compl_interior {s : Set X} :
     frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ := by
   rw [← frontier_compl, ← closure_compl, ← diff_eq, closure_diff_interior]
 #align frontier_eq_inter_compl_interior frontier_eq_inter_compl_interior
 
-theorem compl_frontier_eq_union_interior {s : Set α} :
+theorem compl_frontier_eq_union_interior {s : Set X} :
     (frontier s)ᶜ = interior s ∪ interior sᶜ := by
   rw [frontier_eq_inter_compl_interior]
   simp only [compl_inter, compl_compl]
@@ -838,14 +839,14 @@ theorem compl_frontier_eq_union_interior {s : Set α} :
 /-- A set is called a neighborhood of `a` if it contains an open set around `a`. The set of all
 neighborhoods of `a` forms a filter, the neighborhood filter at `a`, is here defined as the
 infimum over the principal filters of all open sets containing `a`. -/
-irreducible_def nhds (a : α) : Filter α :=
-  ⨅ s ∈ { s : Set α | a ∈ s ∧ IsOpen s }, 𝓟 s
+irreducible_def nhds (a : X) : Filter X :=
+  ⨅ s ∈ { s : Set X | a ∈ s ∧ IsOpen s }, 𝓟 s
 #align nhds nhds
 #align nhds_def nhds_def
 
 /-- The "neighborhood within" filter. Elements of `𝓝[s] a` are sets containing the
 intersection of `s` and a neighborhood of `a`. -/
-def nhdsWithin (a : α) (s : Set α) : Filter α :=
+def nhdsWithin (a : X) (s : Set X) : Filter X :=
   nhds a ⊓ 𝓟 s
 #align nhds_within nhdsWithin
 
@@ -874,14 +875,14 @@ scoped[Topology] notation3 "𝓝[<] " x:100 => nhdsWithin x (Set.Iio x)
 
 end
 
-theorem nhds_def' (a : α) : 𝓝 a = ⨅ (s : Set α) (_ : IsOpen s) (_ : a ∈ s), 𝓟 s := by
+theorem nhds_def' (a : X) : 𝓝 a = ⨅ (s : Set X) (_ : IsOpen s) (_ : a ∈ s), 𝓟 s := by
   simp only [nhds_def, mem_setOf_eq, @and_comm (a ∈ _), iInf_and]
 #align nhds_def' nhds_def'
 
 /-- The open sets containing `a` are a basis for the neighborhood filter. See `nhds_basis_opens'`
 for a variant using open neighborhoods instead. -/
-theorem nhds_basis_opens (a : α) :
-    (𝓝 a).HasBasis (fun s : Set α => a ∈ s ∧ IsOpen s) fun s => s := by
+theorem nhds_basis_opens (a : X) :
+    (𝓝 a).HasBasis (fun s : Set X => a ∈ s ∧ IsOpen s) fun s => s := by
   rw [nhds_def]
   exact hasBasis_biInf_principal
     (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ =>
@@ -889,114 +890,114 @@ theorem nhds_basis_opens (a : α) :
     ⟨univ, ⟨mem_univ a, isOpen_univ⟩⟩
 #align nhds_basis_opens nhds_basis_opens
 
-theorem nhds_basis_closeds (a : α) : (𝓝 a).HasBasis (fun s : Set α => a ∉ s ∧ IsClosed s) compl :=
+theorem nhds_basis_closeds (a : X) : (𝓝 a).HasBasis (fun s : Set X => a ∉ s ∧ IsClosed s) compl :=
   ⟨fun t => (nhds_basis_opens a).mem_iff.trans <|
     compl_surjective.exists.trans <| by simp only [isOpen_compl_iff, mem_compl_iff]⟩
 #align nhds_basis_closeds nhds_basis_closeds
 
 /-- A filter lies below the neighborhood filter at `a` iff it contains every open set around `a`. -/
-theorem le_nhds_iff {f a} : f ≤ 𝓝 a ↔ ∀ s : Set α, a ∈ s → IsOpen s → s ∈ f := by simp [nhds_def]
+theorem le_nhds_iff {f a} : f ≤ 𝓝 a ↔ ∀ s : Set X, a ∈ s → IsOpen s → s ∈ f := by simp [nhds_def]
 #align le_nhds_iff le_nhds_iff
 
 /-- To show a filter is above the neighborhood filter at `a`, it suffices to show that it is above
 the principal filter of some open set `s` containing `a`. -/
-theorem nhds_le_of_le {f a} {s : Set α} (h : a ∈ s) (o : IsOpen s) (sf : 𝓟 s ≤ f) : 𝓝 a ≤ f := by
+theorem nhds_le_of_le {f a} {s : Set X} (h : a ∈ s) (o : IsOpen s) (sf : 𝓟 s ≤ f) : 𝓝 a ≤ f := by
   rw [nhds_def]; exact iInf₂_le_of_le s ⟨h, o⟩ sf
 #align nhds_le_of_le nhds_le_of_le
 
 -- porting note: use `∃ t, t ⊆ s ∧ _` instead of `∃ t ⊆ s, _`
-theorem mem_nhds_iff {a : α} {s : Set α} : s ∈ 𝓝 a ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ a ∈ t :=
+theorem mem_nhds_iff {a : X} {s : Set X} : s ∈ 𝓝 a ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ a ∈ t :=
   (nhds_basis_opens a).mem_iff.trans <| exists_congr fun _ =>
     ⟨fun h => ⟨h.2, h.1.2, h.1.1⟩, fun h => ⟨⟨h.2.2, h.2.1⟩, h.1⟩⟩
 #align mem_nhds_iff mem_nhds_iffₓ
 
 /-- A predicate is true in a neighborhood of `a` iff it is true for all the points in an open set
 containing `a`. -/
-theorem eventually_nhds_iff {a : α} {p : α → Prop} :
-    (∀ᶠ x in 𝓝 a, p x) ↔ ∃ t : Set α, (∀ x ∈ t, p x) ∧ IsOpen t ∧ a ∈ t :=
+theorem eventually_nhds_iff {a : X} {p : X → Prop} :
+    (∀ᶠ x in 𝓝 a, p x) ↔ ∃ t : Set X, (∀ x ∈ t, p x) ∧ IsOpen t ∧ a ∈ t :=
   mem_nhds_iff.trans <| by simp only [subset_def, exists_prop, mem_setOf_eq]
 #align eventually_nhds_iff eventually_nhds_iff
 
-theorem mem_interior_iff_mem_nhds {s : Set α} {a : α} : a ∈ interior s ↔ s ∈ 𝓝 a :=
+theorem mem_interior_iff_mem_nhds {s : Set X} {a : X} : a ∈ interior s ↔ s ∈ 𝓝 a :=
   mem_interior.trans mem_nhds_iff.symm
 #align mem_interior_iff_mem_nhds mem_interior_iff_mem_nhds
 
-theorem map_nhds {a : α} {f : α → β} :
-    map f (𝓝 a) = ⨅ s ∈ { s : Set α | a ∈ s ∧ IsOpen s }, 𝓟 (image f s) :=
+theorem map_nhds {a : X} {f : X → α} :
+    map f (𝓝 a) = ⨅ s ∈ { s : Set X | a ∈ s ∧ IsOpen s }, 𝓟 (f '' s) :=
   ((nhds_basis_opens a).map f).eq_biInf
 #align map_nhds map_nhds
 
-theorem mem_of_mem_nhds {a : α} {s : Set α} : s ∈ 𝓝 a → a ∈ s := fun H =>
+theorem mem_of_mem_nhds {a : X} {s : Set X} : s ∈ 𝓝 a → a ∈ s := fun H =>
   let ⟨_t, ht, _, hs⟩ := mem_nhds_iff.1 H; ht hs
 #align mem_of_mem_nhds mem_of_mem_nhds
 
 /-- If a predicate is true in a neighborhood of `a`, then it is true for `a`. -/
-theorem Filter.Eventually.self_of_nhds {p : α → Prop} {a : α} (h : ∀ᶠ y in 𝓝 a, p y) : p a :=
+theorem Filter.Eventually.self_of_nhds {p : X → Prop} {a : X} (h : ∀ᶠ y in 𝓝 a, p y) : p a :=
   mem_of_mem_nhds h
 #align filter.eventually.self_of_nhds Filter.Eventually.self_of_nhds
 
-theorem IsOpen.mem_nhds {a : α} {s : Set α} (hs : IsOpen s) (ha : a ∈ s) : s ∈ 𝓝 a :=
+theorem IsOpen.mem_nhds {a : X} {s : Set X} (hs : IsOpen s) (ha : a ∈ s) : s ∈ 𝓝 a :=
   mem_nhds_iff.2 ⟨s, Subset.refl _, hs, ha⟩
 #align is_open.mem_nhds IsOpen.mem_nhds
 
-protected theorem IsOpen.mem_nhds_iff {a : α} {s : Set α} (hs : IsOpen s) : s ∈ 𝓝 a ↔ a ∈ s :=
+protected theorem IsOpen.mem_nhds_iff {a : X} {s : Set X} (hs : IsOpen s) : s ∈ 𝓝 a ↔ a ∈ s :=
   ⟨mem_of_mem_nhds, fun ha => mem_nhds_iff.2 ⟨s, Subset.rfl, hs, ha⟩⟩
 #align is_open.mem_nhds_iff IsOpen.mem_nhds_iff
 
-theorem IsClosed.compl_mem_nhds {a : α} {s : Set α} (hs : IsClosed s) (ha : a ∉ s) : sᶜ ∈ 𝓝 a :=
+theorem IsClosed.compl_mem_nhds {a : X} {s : Set X} (hs : IsClosed s) (ha : a ∉ s) : sᶜ ∈ 𝓝 a :=
   hs.isOpen_compl.mem_nhds (mem_compl ha)
 #align is_closed.compl_mem_nhds IsClosed.compl_mem_nhds
 
-theorem IsOpen.eventually_mem {a : α} {s : Set α} (hs : IsOpen s) (ha : a ∈ s) :
+theorem IsOpen.eventually_mem {a : X} {s : Set X} (hs : IsOpen s) (ha : a ∈ s) :
     ∀ᶠ x in 𝓝 a, x ∈ s :=
   IsOpen.mem_nhds hs ha
 #align is_open.eventually_mem IsOpen.eventually_mem
 
 /-- The open neighborhoods of `a` are a basis for the neighborhood filter. See `nhds_basis_opens`
 for a variant using open sets around `a` instead. -/
-theorem nhds_basis_opens' (a : α) :
-    (𝓝 a).HasBasis (fun s : Set α => s ∈ 𝓝 a ∧ IsOpen s) fun x => x := by
+theorem nhds_basis_opens' (a : X) :
+    (𝓝 a).HasBasis (fun s : Set X => s ∈ 𝓝 a ∧ IsOpen s) fun x => x := by
   convert nhds_basis_opens a using 2
   exact and_congr_left_iff.2 IsOpen.mem_nhds_iff
 #align nhds_basis_opens' nhds_basis_opens'
 
 /-- If `U` is a neighborhood of each point of a set `s` then it is a neighborhood of `s`:
 it contains an open set containing `s`. -/
-theorem exists_open_set_nhds {s U : Set α} (h : ∀ x ∈ s, U ∈ 𝓝 x) :
-    ∃ V : Set α, s ⊆ V ∧ IsOpen V ∧ V ⊆ U :=
+theorem exists_open_set_nhds {s U : Set X} (h : ∀ x ∈ s, U ∈ 𝓝 x) :
+    ∃ V : Set X, s ⊆ V ∧ IsOpen V ∧ V ⊆ U :=
   ⟨interior U, fun x hx => mem_interior_iff_mem_nhds.2 <| h x hx, isOpen_interior, interior_subset⟩
 #align exists_open_set_nhds exists_open_set_nhds
 
 /-- If `U` is a neighborhood of each point of a set `s` then it is a neighborhood of s:
 it contains an open set containing `s`. -/
-theorem exists_open_set_nhds' {s U : Set α} (h : U ∈ ⨆ x ∈ s, 𝓝 x) :
-    ∃ V : Set α, s ⊆ V ∧ IsOpen V ∧ V ⊆ U :=
+theorem exists_open_set_nhds' {s U : Set X} (h : U ∈ ⨆ x ∈ s, 𝓝 x) :
+    ∃ V : Set X, s ⊆ V ∧ IsOpen V ∧ V ⊆ U :=
   exists_open_set_nhds (by simpa using h)
 #align exists_open_set_nhds' exists_open_set_nhds'
 
 /-- If a predicate is true in a neighbourhood of `a`, then for `y` sufficiently close
 to `a` this predicate is true in a neighbourhood of `y`. -/
-theorem Filter.Eventually.eventually_nhds {p : α → Prop} {a : α} (h : ∀ᶠ y in 𝓝 a, p y) :
+theorem Filter.Eventually.eventually_nhds {p : X → Prop} {a : X} (h : ∀ᶠ y in 𝓝 a, p y) :
     ∀ᶠ y in 𝓝 a, ∀ᶠ x in 𝓝 y, p x :=
   let ⟨t, htp, hto, ha⟩ := eventually_nhds_iff.1 h
   eventually_nhds_iff.2 ⟨t, fun _x hx => eventually_nhds_iff.2 ⟨t, htp, hto, hx⟩, hto, ha⟩
 #align filter.eventually.eventually_nhds Filter.Eventually.eventually_nhds
 
 @[simp]
-theorem eventually_eventually_nhds {p : α → Prop} {a : α} :
+theorem eventually_eventually_nhds {p : X → Prop} {a : X} :
     (∀ᶠ y in 𝓝 a, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝 a, p x :=
   ⟨fun h => h.self_of_nhds, fun h => h.eventually_nhds⟩
 #align eventually_eventually_nhds eventually_eventually_nhds
 
 @[simp]
-theorem frequently_frequently_nhds {p : α → Prop} {a : α} :
+theorem frequently_frequently_nhds {p : X → Prop} {a : X} :
     (∃ᶠ y in 𝓝 a, ∃ᶠ x in 𝓝 y, p x) ↔ ∃ᶠ x in 𝓝 a, p x := by
   rw [← not_iff_not]
   simp only [not_frequently, eventually_eventually_nhds]
 #align frequently_frequently_nhds frequently_frequently_nhds
 
 @[simp]
-theorem eventually_mem_nhds {s : Set α} {a : α} : (∀ᶠ x in 𝓝 a, s ∈ 𝓝 x) ↔ s ∈ 𝓝 a :=
+theorem eventually_mem_nhds {s : Set X} {a : X} : (∀ᶠ x in 𝓝 a, s ∈ 𝓝 x) ↔ s ∈ 𝓝 a :=
   eventually_eventually_nhds
 #align eventually_mem_nhds eventually_mem_nhds
 
@@ -1006,93 +1007,92 @@ theorem nhds_bind_nhds : (𝓝 a).bind 𝓝 = 𝓝 a :=
 #align nhds_bind_nhds nhds_bind_nhds
 
 @[simp]
-theorem eventually_eventuallyEq_nhds {f g : α → β} {a : α} :
+theorem eventually_eventuallyEq_nhds {f g : X → α} {a : X} :
     (∀ᶠ y in 𝓝 a, f =ᶠ[𝓝 y] g) ↔ f =ᶠ[𝓝 a] g :=
   eventually_eventually_nhds
 #align eventually_eventually_eq_nhds eventually_eventuallyEq_nhds
 
-theorem Filter.EventuallyEq.eq_of_nhds {f g : α → β} {a : α} (h : f =ᶠ[𝓝 a] g) : f a = g a :=
+theorem Filter.EventuallyEq.eq_of_nhds {f g : X → α} {a : X} (h : f =ᶠ[𝓝 a] g) : f a = g a :=
   h.self_of_nhds
 #align filter.eventually_eq.eq_of_nhds Filter.EventuallyEq.eq_of_nhds
 
 @[simp]
-theorem eventually_eventuallyLE_nhds [LE β] {f g : α → β} {a : α} :
+theorem eventually_eventuallyLE_nhds [LE α] {f g : X → α} {a : X} :
     (∀ᶠ y in 𝓝 a, f ≤ᶠ[𝓝 y] g) ↔ f ≤ᶠ[𝓝 a] g :=
   eventually_eventually_nhds
 #align eventually_eventually_le_nhds eventually_eventuallyLE_nhds
 
 /-- If two functions are equal in a neighbourhood of `a`, then for `y` sufficiently close
 to `a` these functions are equal in a neighbourhood of `y`. -/
-theorem Filter.EventuallyEq.eventuallyEq_nhds {f g : α → β} {a : α} (h : f =ᶠ[𝓝 a] g) :
+theorem Filter.EventuallyEq.eventuallyEq_nhds {f g : X → α} {a : X} (h : f =ᶠ[𝓝 a] g) :
     ∀ᶠ y in 𝓝 a, f =ᶠ[𝓝 y] g :=
   h.eventually_nhds
 #align filter.eventually_eq.eventually_eq_nhds Filter.EventuallyEq.eventuallyEq_nhds
 
 /-- If `f x ≤ g x` in a neighbourhood of `a`, then for `y` sufficiently close to `a` we have
 `f x ≤ g x` in a neighbourhood of `y`. -/
-theorem Filter.EventuallyLE.eventuallyLE_nhds [LE β] {f g : α → β} {a : α} (h : f ≤ᶠ[𝓝 a] g) :
+theorem Filter.EventuallyLE.eventuallyLE_nhds [LE α] {f g : X → α} {a : X} (h : f ≤ᶠ[𝓝 a] g) :
     ∀ᶠ y in 𝓝 a, f ≤ᶠ[𝓝 y] g :=
   h.eventually_nhds
 #align filter.eventually_le.eventually_le_nhds Filter.EventuallyLE.eventuallyLE_nhds
 
-theorem all_mem_nhds (x : α) (P : Set α → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) :
+theorem all_mem_nhds (x : X) (P : Set X → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) :
     (∀ s ∈ 𝓝 x, P s) ↔ ∀ s, IsOpen s → x ∈ s → P s :=
   ((nhds_basis_opens x).forall_iff hP).trans <| by simp only [@and_comm (x ∈ _), and_imp]
 #align all_mem_nhds all_mem_nhds
 
-theorem all_mem_nhds_filter (x : α) (f : Set α → Set β) (hf : ∀ s t, s ⊆ t → f s ⊆ f t)
-    (l : Filter β) : (∀ s ∈ 𝓝 x, f s ∈ l) ↔ ∀ s, IsOpen s → x ∈ s → f s ∈ l :=
+theorem all_mem_nhds_filter (x : X) (f : Set X → Set α) (hf : ∀ s t, s ⊆ t → f s ⊆ f t)
+    (l : Filter α) : (∀ s ∈ 𝓝 x, f s ∈ l) ↔ ∀ s, IsOpen s → x ∈ s → f s ∈ l :=
   all_mem_nhds _ _ fun s t ssubt h => mem_of_superset h (hf s t ssubt)
 #align all_mem_nhds_filter all_mem_nhds_filter
 
-theorem tendsto_nhds {f : β → α} {l : Filter β} {a : α} :
+theorem tendsto_nhds {f : α → X} {l : Filter α} {a : X} :
     Tendsto f l (𝓝 a) ↔ ∀ s, IsOpen s → a ∈ s → f ⁻¹' s ∈ l :=
   all_mem_nhds_filter _ _ (fun _ _ h => preimage_mono h) _
 #align tendsto_nhds tendsto_nhds
 
-theorem tendsto_atTop_nhds [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} :
-    Tendsto f atTop (𝓝 a) ↔ ∀ U : Set α, a ∈ U → IsOpen U → ∃ N, ∀ n, N ≤ n → f n ∈ U :=
+theorem tendsto_atTop_nhds [Nonempty α] [SemilatticeSup α] {f : α → X} {a : X} :
+    Tendsto f atTop (𝓝 a) ↔ ∀ U : Set X, a ∈ U → IsOpen U → ∃ N, ∀ n, N ≤ n → f n ∈ U :=
   (atTop_basis.tendsto_iff (nhds_basis_opens a)).trans <| by
     simp only [and_imp, exists_prop, true_and_iff, mem_Ici, ge_iff_le]
 #align tendsto_at_top_nhds tendsto_atTop_nhds
 
-theorem tendsto_const_nhds {a : α} {f : Filter β} : Tendsto (fun _ : β => a) f (𝓝 a) :=
+theorem tendsto_const_nhds {a : X} {f : Filter α} : Tendsto (fun _ : α => a) f (𝓝 a) :=
   tendsto_nhds.mpr fun _ _ ha => univ_mem' fun _ => ha
 #align tendsto_const_nhds tendsto_const_nhds
 
-theorem tendsto_atTop_of_eventually_const {ι : Type*} [SemilatticeSup ι] [Nonempty ι] {x : α}
-    {u : ι → α} {i₀ : ι} (h : ∀ i ≥ i₀, u i = x) : Tendsto u atTop (𝓝 x) :=
+theorem tendsto_atTop_of_eventually_const {ι : Type*} [SemilatticeSup ι] [Nonempty ι] {x : X}
+    {u : ι → X} {i₀ : ι} (h : ∀ i ≥ i₀, u i = x) : Tendsto u atTop (𝓝 x) :=
   Tendsto.congr' (EventuallyEq.symm (eventually_atTop.mpr ⟨i₀, h⟩)) tendsto_const_nhds
 #align tendsto_at_top_of_eventually_const tendsto_atTop_of_eventually_const
 
-theorem tendsto_atBot_of_eventually_const {ι : Type*} [SemilatticeInf ι] [Nonempty ι] {x : α}
-    {u : ι → α} {i₀ : ι} (h : ∀ i ≤ i₀, u i = x) : Tendsto u atBot (𝓝 x) :=
+theorem tendsto_atBot_of_eventually_const {ι : Type*} [SemilatticeInf ι] [Nonempty ι] {x : X}
+    {u : ι → X} {i₀ : ι} (h : ∀ i ≤ i₀, u i = x) : Tendsto u atBot (𝓝 x) :=
   Tendsto.congr' (EventuallyEq.symm (eventually_atBot.mpr ⟨i₀, h⟩)) tendsto_const_nhds
 #align tendsto_at_bot_of_eventually_const tendsto_atBot_of_eventually_const
 
-theorem pure_le_nhds : pure ≤ (𝓝 : α → Filter α) := fun _ _ hs => mem_pure.2 <| mem_of_mem_nhds hs
+theorem pure_le_nhds : pure ≤ (𝓝 : X → Filter X) := fun _ _ hs => mem_pure.2 <| mem_of_mem_nhds hs
 #align pure_le_nhds pure_le_nhds
 
-theorem tendsto_pure_nhds {α : Type*} [TopologicalSpace β] (f : α → β) (a : α) :
-    Tendsto f (pure a) (𝓝 (f a)) :=
+theorem tendsto_pure_nhds (f : α → X) (a : α) : Tendsto f (pure a) (𝓝 (f a)) :=
   (tendsto_pure_pure f a).mono_right (pure_le_nhds _)
 #align tendsto_pure_nhds tendsto_pure_nhds
 
-theorem OrderTop.tendsto_atTop_nhds {α : Type*} [PartialOrder α] [OrderTop α] [TopologicalSpace β]
-    (f : α → β) : Tendsto f atTop (𝓝 (f ⊤)) :=
+theorem OrderTop.tendsto_atTop_nhds [PartialOrder α] [OrderTop α] (f : α → X) :
+    Tendsto f atTop (𝓝 (f ⊤)) :=
   (tendsto_atTop_pure f).mono_right (pure_le_nhds _)
 #align order_top.tendsto_at_top_nhds OrderTop.tendsto_atTop_nhds
 
 @[simp]
-instance nhds_neBot {a : α} : NeBot (𝓝 a) :=
+instance nhds_neBot {a : X} : NeBot (𝓝 a) :=
   neBot_of_le (pure_le_nhds a)
 #align nhds_ne_bot nhds_neBot
 
-theorem tendsto_nhds_of_eventually_eq {l : Filter β} {f : β → α} {a : α} (h : ∀ᶠ x in l, f x = a) :
+theorem tendsto_nhds_of_eventually_eq {l : Filter α} {f : α → X} {a : X} (h : ∀ᶠ x in l, f x = a) :
     Tendsto f l (𝓝 a) :=
   tendsto_const_nhds.congr' (.symm h)
 
-theorem Filter.EventuallyEq.tendsto {l : Filter β} {f : β → α} {a : α} (hf : f =ᶠ[l] fun _ ↦ a) :
+theorem Filter.EventuallyEq.tendsto {l : Filter α} {f : α → X} {a : X} (hf : f =ᶠ[l] fun _ ↦ a) :
     Tendsto f l (𝓝 a) :=
   tendsto_nhds_of_eventually_eq hf
 
@@ -1107,85 +1107,85 @@ In this section we define [cluster points](https://en.wikipedia.org/wiki/Limit_p
 /-- A point `x` is a cluster point of a filter `F` if `𝓝 x ⊓ F ≠ ⊥`. Also known as
 an accumulation point or a limit point, but beware that terminology varies. This
 is *not* the same as asking `𝓝[≠] x ⊓ F ≠ ⊥`. See `mem_closure_iff_clusterPt` in particular. -/
-def ClusterPt (x : α) (F : Filter α) : Prop :=
+def ClusterPt (x : X) (F : Filter X) : Prop :=
   NeBot (𝓝 x ⊓ F)
 #align cluster_pt ClusterPt
 
-theorem ClusterPt.neBot {x : α} {F : Filter α} (h : ClusterPt x F) : NeBot (𝓝 x ⊓ F) :=
+theorem ClusterPt.neBot {x : X} {F : Filter X} (h : ClusterPt x F) : NeBot (𝓝 x ⊓ F) :=
   h
 #align cluster_pt.ne_bot ClusterPt.neBot
 
-theorem Filter.HasBasis.clusterPt_iff {ιa ιF} {pa : ιa → Prop} {sa : ιa → Set α} {pF : ιF → Prop}
-    {sF : ιF → Set α} {F : Filter α} (ha : (𝓝 a).HasBasis pa sa) (hF : F.HasBasis pF sF) :
+theorem Filter.HasBasis.clusterPt_iff {ιa ιF} {pa : ιa → Prop} {sa : ιa → Set X} {pF : ιF → Prop}
+    {sF : ιF → Set X} {F : Filter X} (ha : (𝓝 a).HasBasis pa sa) (hF : F.HasBasis pF sF) :
     ClusterPt a F ↔ ∀ ⦃i⦄, pa i → ∀ ⦃j⦄, pF j → (sa i ∩ sF j).Nonempty :=
   ha.inf_basis_neBot_iff hF
 #align filter.has_basis.cluster_pt_iff Filter.HasBasis.clusterPt_iff
 
-theorem clusterPt_iff {x : α} {F : Filter α} :
-    ClusterPt x F ↔ ∀ ⦃U : Set α⦄, U ∈ 𝓝 x → ∀ ⦃V⦄, V ∈ F → (U ∩ V).Nonempty :=
+theorem clusterPt_iff {x : X} {F : Filter X} :
+    ClusterPt x F ↔ ∀ ⦃U : Set X⦄, U ∈ 𝓝 x → ∀ ⦃V⦄, V ∈ F → (U ∩ V).Nonempty :=
   inf_neBot_iff
 #align cluster_pt_iff clusterPt_iff
 
-theorem clusterPt_iff_not_disjoint {x : α} {F : Filter α} :
+theorem clusterPt_iff_not_disjoint {x : X} {F : Filter X} :
     ClusterPt x F ↔ ¬Disjoint (𝓝 x) F := by
   rw [disjoint_iff, ClusterPt, neBot_iff]
 
 /-- `x` is a cluster point of a set `s` if every neighbourhood of `x` meets `s` on a nonempty
 set. See also `mem_closure_iff_clusterPt`. -/
-theorem clusterPt_principal_iff {x : α} {s : Set α} :
+theorem clusterPt_principal_iff {x : X} {s : Set X} :
     ClusterPt x (𝓟 s) ↔ ∀ U ∈ 𝓝 x, (U ∩ s).Nonempty :=
   inf_principal_neBot_iff
 #align cluster_pt_principal_iff clusterPt_principal_iff
 
-theorem clusterPt_principal_iff_frequently {x : α} {s : Set α} :
+theorem clusterPt_principal_iff_frequently {x : X} {s : Set X} :
     ClusterPt x (𝓟 s) ↔ ∃ᶠ y in 𝓝 x, y ∈ s := by
   simp only [clusterPt_principal_iff, frequently_iff, Set.Nonempty, exists_prop, mem_inter_iff]
 #align cluster_pt_principal_iff_frequently clusterPt_principal_iff_frequently
 
-theorem ClusterPt.of_le_nhds {x : α} {f : Filter α} (H : f ≤ 𝓝 x) [NeBot f] : ClusterPt x f := by
+theorem ClusterPt.of_le_nhds {x : X} {f : Filter X} (H : f ≤ 𝓝 x) [NeBot f] : ClusterPt x f := by
   rwa [ClusterPt, inf_eq_right.mpr H]
 #align cluster_pt.of_le_nhds ClusterPt.of_le_nhds
 
-theorem ClusterPt.of_le_nhds' {x : α} {f : Filter α} (H : f ≤ 𝓝 x) (_hf : NeBot f) :
+theorem ClusterPt.of_le_nhds' {x : X} {f : Filter X} (H : f ≤ 𝓝 x) (_hf : NeBot f) :
     ClusterPt x f :=
   ClusterPt.of_le_nhds H
 #align cluster_pt.of_le_nhds' ClusterPt.of_le_nhds'
 
-theorem ClusterPt.of_nhds_le {x : α} {f : Filter α} (H : 𝓝 x ≤ f) : ClusterPt x f := by
+theorem ClusterPt.of_nhds_le {x : X} {f : Filter X} (H : 𝓝 x ≤ f) : ClusterPt x f := by
   simp only [ClusterPt, inf_eq_left.mpr H, nhds_neBot]
 #align cluster_pt.of_nhds_le ClusterPt.of_nhds_le
 
-theorem ClusterPt.mono {x : α} {f g : Filter α} (H : ClusterPt x f) (h : f ≤ g) : ClusterPt x g :=
+theorem ClusterPt.mono {x : X} {f g : Filter X} (H : ClusterPt x f) (h : f ≤ g) : ClusterPt x g :=
   NeBot.mono H <| inf_le_inf_left _ h
 #align cluster_pt.mono ClusterPt.mono
 
-theorem ClusterPt.of_inf_left {x : α} {f g : Filter α} (H : ClusterPt x <| f ⊓ g) : ClusterPt x f :=
+theorem ClusterPt.of_inf_left {x : X} {f g : Filter X} (H : ClusterPt x <| f ⊓ g) : ClusterPt x f :=
   H.mono inf_le_left
 #align cluster_pt.of_inf_left ClusterPt.of_inf_left
 
-theorem ClusterPt.of_inf_right {x : α} {f g : Filter α} (H : ClusterPt x <| f ⊓ g) :
+theorem ClusterPt.of_inf_right {x : X} {f g : Filter X} (H : ClusterPt x <| f ⊓ g) :
     ClusterPt x g :=
   H.mono inf_le_right
 #align cluster_pt.of_inf_right ClusterPt.of_inf_right
 
-theorem Ultrafilter.clusterPt_iff {x : α} {f : Ultrafilter α} : ClusterPt x f ↔ ↑f ≤ 𝓝 x :=
+theorem Ultrafilter.clusterPt_iff {x : X} {f : Ultrafilter X} : ClusterPt x f ↔ ↑f ≤ 𝓝 x :=
   ⟨f.le_of_inf_neBot', fun h => ClusterPt.of_le_nhds h⟩
 #align ultrafilter.cluster_pt_iff Ultrafilter.clusterPt_iff
 
 /-- A point `x` is a cluster point of a sequence `u` along a filter `F` if it is a cluster point
 of `map u F`. -/
-def MapClusterPt {ι : Type*} (x : α) (F : Filter ι) (u : ι → α) : Prop :=
+def MapClusterPt {ι : Type*} (x : X) (F : Filter ι) (u : ι → X) : Prop :=
   ClusterPt x (map u F)
 #align map_cluster_pt MapClusterPt
 
-theorem mapClusterPt_iff {ι : Type*} (x : α) (F : Filter ι) (u : ι → α) :
+theorem mapClusterPt_iff {ι : Type*} (x : X) (F : Filter ι) (u : ι → X) :
     MapClusterPt x F u ↔ ∀ s ∈ 𝓝 x, ∃ᶠ a in F, u a ∈ s := by
   simp_rw [MapClusterPt, ClusterPt, inf_neBot_iff_frequently_left, frequently_map]
   rfl
 #align map_cluster_pt_iff mapClusterPt_iff
 
-theorem mapClusterPt_of_comp {ι δ : Type*} {F : Filter ι} {φ : δ → ι} {p : Filter δ} {x : α}
-    {u : ι → α} [NeBot p] (h : Tendsto φ p F) (H : Tendsto (u ∘ φ) p (𝓝 x)) :
+theorem mapClusterPt_of_comp {F : Filter α} {φ : β → α} {p : Filter β} {x : X}
+    {u : α → X} [NeBot p] (h : Tendsto φ p F) (H : Tendsto (u ∘ φ) p (𝓝 x)) :
     MapClusterPt x F u := by
   have :=
     calc
@@ -1196,36 +1196,36 @@ theorem mapClusterPt_of_comp {ι δ : Type*} {F : Filter ι} {φ : δ → ι} {p
 #align map_cluster_pt_of_comp mapClusterPt_of_comp
 
 /-- A point `x` is an accumulation point of a filter `F` if `𝓝[≠] x ⊓ F ≠ ⊥`.-/
-def AccPt (x : α) (F : Filter α) : Prop :=
+def AccPt (x : X) (F : Filter X) : Prop :=
   NeBot (𝓝[≠] x ⊓ F)
 #align acc_pt AccPt
 
-theorem acc_iff_cluster (x : α) (F : Filter α) : AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F) := by
+theorem acc_iff_cluster (x : X) (F : Filter X) : AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F) := by
   rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]
 #align acc_iff_cluster acc_iff_cluster
 
 /-- `x` is an accumulation point of a set `C` iff it is a cluster point of `C ∖ {x}`.-/
-theorem acc_principal_iff_cluster (x : α) (C : Set α) :
+theorem acc_principal_iff_cluster (x : X) (C : Set X) :
     AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x})) := by
   rw [acc_iff_cluster, inf_principal, inter_comm, diff_eq]
 #align acc_principal_iff_cluster acc_principal_iff_cluster
 
 /-- `x` is an accumulation point of a set `C` iff every neighborhood
 of `x` contains a point of `C` other than `x`. -/
-theorem accPt_iff_nhds (x : α) (C : Set α) : AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x := by
+theorem accPt_iff_nhds (x : X) (C : Set X) : AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x := by
   simp [acc_principal_iff_cluster, clusterPt_principal_iff, Set.Nonempty, exists_prop, and_assoc,
     @and_comm (¬_ = x)]
 #align acc_pt_iff_nhds accPt_iff_nhds
 
 /-- `x` is an accumulation point of a set `C` iff
 there are points near `x` in `C` and different from `x`.-/
-theorem accPt_iff_frequently (x : α) (C : Set α) : AccPt x (𝓟 C) ↔ ∃ᶠ y in 𝓝 x, y ≠ x ∧ y ∈ C := by
+theorem accPt_iff_frequently (x : X) (C : Set X) : AccPt x (𝓟 C) ↔ ∃ᶠ y in 𝓝 x, y ≠ x ∧ y ∈ C := by
   simp [acc_principal_iff_cluster, clusterPt_principal_iff_frequently, and_comm]
 #align acc_pt_iff_frequently accPt_iff_frequently
 
 /-- If `x` is an accumulation point of `F` and `F ≤ G`, then
 `x` is an accumulation point of `D`. -/
-theorem AccPt.mono {x : α} {F G : Filter α} (h : AccPt x F) (hFG : F ≤ G) : AccPt x G :=
+theorem AccPt.mono {x : X} {F G : Filter X} (h : AccPt x F) (hFG : F ≤ G) : AccPt x G :=
   NeBot.mono h (inf_le_inf_left _ hFG)
 #align acc_pt.mono AccPt.mono
 
@@ -1233,53 +1233,53 @@ theorem AccPt.mono {x : α} {F G : Filter α} (h : AccPt x F) (hFG : F ≤ G) :
 ### Interior, closure and frontier in terms of neighborhoods
 -/
 
-theorem interior_eq_nhds' {s : Set α} : interior s = { a | s ∈ 𝓝 a } :=
+theorem interior_eq_nhds' {s : Set X} : interior s = { a | s ∈ 𝓝 a } :=
   Set.ext fun x => by simp only [mem_interior, mem_nhds_iff, mem_setOf_eq]
 #align interior_eq_nhds' interior_eq_nhds'
 
-theorem interior_eq_nhds {s : Set α} : interior s = { a | 𝓝 a ≤ 𝓟 s } :=
+theorem interior_eq_nhds {s : Set X} : interior s = { a | 𝓝 a ≤ 𝓟 s } :=
   interior_eq_nhds'.trans <| by simp only [le_principal_iff]
 #align interior_eq_nhds interior_eq_nhds
 
 @[simp]
-theorem interior_mem_nhds {s : Set α} {a : α} : interior s ∈ 𝓝 a ↔ s ∈ 𝓝 a :=
+theorem interior_mem_nhds {s : Set X} {a : X} : interior s ∈ 𝓝 a ↔ s ∈ 𝓝 a :=
   ⟨fun h => mem_of_superset h interior_subset, fun h =>
     IsOpen.mem_nhds isOpen_interior (mem_interior_iff_mem_nhds.2 h)⟩
 #align interior_mem_nhds interior_mem_nhds
 
-theorem interior_setOf_eq {p : α → Prop} : interior { x | p x } = { x | ∀ᶠ y in 𝓝 x, p y } :=
+theorem interior_setOf_eq {p : X → Prop} : interior { x | p x } = { x | ∀ᶠ y in 𝓝 x, p y } :=
   interior_eq_nhds'
 #align interior_set_of_eq interior_setOf_eq
 
-theorem isOpen_setOf_eventually_nhds {p : α → Prop} : IsOpen { x | ∀ᶠ y in 𝓝 x, p y } := by
+theorem isOpen_setOf_eventually_nhds {p : X → Prop} : IsOpen { x | ∀ᶠ y in 𝓝 x, p y } := by
   simp only [← interior_setOf_eq, isOpen_interior]
 #align is_open_set_of_eventually_nhds isOpen_setOf_eventually_nhds
 
-theorem subset_interior_iff_nhds {s V : Set α} : s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x := by
+theorem subset_interior_iff_nhds {s V : Set X} : s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x := by
   simp_rw [subset_def, mem_interior_iff_mem_nhds]
 #align subset_interior_iff_nhds subset_interior_iff_nhds
 
-theorem isOpen_iff_nhds {s : Set α} : IsOpen s ↔ ∀ a ∈ s, 𝓝 a ≤ 𝓟 s :=
+theorem isOpen_iff_nhds {s : Set X} : IsOpen s ↔ ∀ a ∈ s, 𝓝 a ≤ 𝓟 s :=
   calc
     IsOpen s ↔ s ⊆ interior s := subset_interior_iff_isOpen.symm
     _ ↔ ∀ a ∈ s, 𝓝 a ≤ 𝓟 s := by simp_rw [interior_eq_nhds, subset_def, mem_setOf]
 #align is_open_iff_nhds isOpen_iff_nhds
 
-theorem isOpen_iff_mem_nhds {s : Set α} : IsOpen s ↔ ∀ a ∈ s, s ∈ 𝓝 a :=
+theorem isOpen_iff_mem_nhds {s : Set X} : IsOpen s ↔ ∀ a ∈ s, s ∈ 𝓝 a :=
   isOpen_iff_nhds.trans <| forall_congr' fun _ => imp_congr_right fun _ => le_principal_iff
 #align is_open_iff_mem_nhds isOpen_iff_mem_nhds
 
 /-- A set `s` is open iff for every point `x` in `s` and every `y` close to `x`, `y` is in `s`. -/
-theorem isOpen_iff_eventually {s : Set α} : IsOpen s ↔ ∀ x, x ∈ s → ∀ᶠ y in 𝓝 x, y ∈ s :=
+theorem isOpen_iff_eventually {s : Set X} : IsOpen s ↔ ∀ x, x ∈ s → ∀ᶠ y in 𝓝 x, y ∈ s :=
   isOpen_iff_mem_nhds
 #align is_open_iff_eventually isOpen_iff_eventually
 
-theorem isOpen_iff_ultrafilter {s : Set α} :
-    IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter α), ↑l ≤ 𝓝 x → s ∈ l := by
+theorem isOpen_iff_ultrafilter {s : Set X} :
+    IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → s ∈ l := by
   simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter]
 #align is_open_iff_ultrafilter isOpen_iff_ultrafilter
 
-theorem isOpen_singleton_iff_nhds_eq_pure (a : α) : IsOpen ({a} : Set α) ↔ 𝓝 a = pure a := by
+theorem isOpen_singleton_iff_nhds_eq_pure (a : X) : IsOpen ({a} : Set X) ↔ 𝓝 a = pure a := by
   constructor
   · intro h
     apply le_antisymm _ (pure_le_nhds a)
@@ -1289,13 +1289,12 @@ theorem isOpen_singleton_iff_nhds_eq_pure (a : α) : IsOpen ({a} : Set α) ↔ 
     simp [isOpen_iff_nhds, h]
 #align is_open_singleton_iff_nhds_eq_pure isOpen_singleton_iff_nhds_eq_pure
 
-theorem isOpen_singleton_iff_punctured_nhds {α : Type*} [TopologicalSpace α] (a : α) :
-    IsOpen ({a} : Set α) ↔ 𝓝[≠] a = ⊥ := by
+theorem isOpen_singleton_iff_punctured_nhds (a : X) : IsOpen ({a} : Set X) ↔ 𝓝[≠] a = ⊥ := by
   rw [isOpen_singleton_iff_nhds_eq_pure, nhdsWithin, ← mem_iff_inf_principal_compl, ← le_pure_iff,
     nhds_neBot.le_pure_iff]
 #align is_open_singleton_iff_punctured_nhds isOpen_singleton_iff_punctured_nhds
 
-theorem mem_closure_iff_frequently {s : Set α} {a : α} : a ∈ closure s ↔ ∃ᶠ x in 𝓝 a, x ∈ s := by
+theorem mem_closure_iff_frequently {s : Set X} {a : X} : a ∈ closure s ↔ ∃ᶠ x in 𝓝 a, x ∈ s := by
   rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
     closure_eq_compl_interior_compl, mem_compl_iff, compl_def]
 #align mem_closure_iff_frequently mem_closure_iff_frequently
@@ -1305,7 +1304,7 @@ alias ⟨_, Filter.Frequently.mem_closure⟩ := mem_closure_iff_frequently
 
 /-- A set `s` is closed iff for every point `x`, if there is a point `y` close to `x` that belongs
 to `s` then `x` is in `s`. -/
-theorem isClosed_iff_frequently {s : Set α} : IsClosed s ↔ ∀ x, (∃ᶠ y in 𝓝 x, y ∈ s) → x ∈ s := by
+theorem isClosed_iff_frequently {s : Set X} : IsClosed s ↔ ∀ x, (∃ᶠ y in 𝓝 x, y ∈ s) → x ∈ s := by
   rw [← closure_subset_iff_isClosed]
   refine' forall_congr' fun x => _
   rw [mem_closure_iff_frequently]
@@ -1313,30 +1312,30 @@ theorem isClosed_iff_frequently {s : Set α} : IsClosed s ↔ ∀ x, (∃ᶠ y i
 
 /-- The set of cluster points of a filter is closed. In particular, the set of limit points
 of a sequence is closed. -/
-theorem isClosed_setOf_clusterPt {f : Filter α} : IsClosed { x | ClusterPt x f } := by
+theorem isClosed_setOf_clusterPt {f : Filter X} : IsClosed { x | ClusterPt x f } := by
   simp only [ClusterPt, inf_neBot_iff_frequently_left, setOf_forall, imp_iff_not_or]
   refine' isClosed_iInter fun p => IsClosed.union _ _ <;> apply isClosed_compl_iff.2
   exacts [isOpen_setOf_eventually_nhds, isOpen_const]
 #align is_closed_set_of_cluster_pt isClosed_setOf_clusterPt
 
-theorem mem_closure_iff_clusterPt {s : Set α} {a : α} : a ∈ closure s ↔ ClusterPt a (𝓟 s) :=
+theorem mem_closure_iff_clusterPt {s : Set X} {a : X} : a ∈ closure s ↔ ClusterPt a (𝓟 s) :=
   mem_closure_iff_frequently.trans clusterPt_principal_iff_frequently.symm
 #align mem_closure_iff_cluster_pt mem_closure_iff_clusterPt
 
-theorem mem_closure_iff_nhds_neBot {s : Set α} : a ∈ closure s ↔ 𝓝 a ⊓ 𝓟 s ≠ ⊥ :=
+theorem mem_closure_iff_nhds_neBot {s : Set X} : a ∈ closure s ↔ 𝓝 a ⊓ 𝓟 s ≠ ⊥ :=
   mem_closure_iff_clusterPt.trans neBot_iff
 #align mem_closure_iff_nhds_ne_bot mem_closure_iff_nhds_neBot
 
-theorem mem_closure_iff_nhdsWithin_neBot {s : Set α} {x : α} : x ∈ closure s ↔ NeBot (𝓝[s] x) :=
+theorem mem_closure_iff_nhdsWithin_neBot {s : Set X} {x : X} : x ∈ closure s ↔ NeBot (𝓝[s] x) :=
   mem_closure_iff_clusterPt
 #align mem_closure_iff_nhds_within_ne_bot mem_closure_iff_nhdsWithin_neBot
 
-lemma not_mem_closure_iff_nhdsWithin_eq_bot {s : Set α} {x : α} : x ∉ closure s ↔ 𝓝[s] x = ⊥ := by
+lemma not_mem_closure_iff_nhdsWithin_eq_bot {s : Set X} {x : X} : x ∉ closure s ↔ 𝓝[s] x = ⊥ := by
   rw [mem_closure_iff_nhdsWithin_neBot, not_neBot]
 
 /-- If `x` is not an isolated point of a topological space, then `{x}ᶜ` is dense in the whole
 space. -/
-theorem dense_compl_singleton (x : α) [NeBot (𝓝[≠] x)] : Dense ({x}ᶜ : Set α) := by
+theorem dense_compl_singleton (x : X) [NeBot (𝓝[≠] x)] : Dense ({x}ᶜ : Set X) := by
   intro y
   rcases eq_or_ne y x with (rfl | hne)
   · rwa [mem_closure_iff_nhdsWithin_neBot]
@@ -1346,95 +1345,95 @@ theorem dense_compl_singleton (x : α) [NeBot (𝓝[≠] x)] : Dense ({x}ᶜ : S
 /-- If `x` is not an isolated point of a topological space, then the closure of `{x}ᶜ` is the whole
 space. -/
 -- porting note: was a `@[simp]` lemma but `simp` can prove it
-theorem closure_compl_singleton (x : α) [NeBot (𝓝[≠] x)] : closure {x}ᶜ = (univ : Set α) :=
+theorem closure_compl_singleton (x : X) [NeBot (𝓝[≠] x)] : closure {x}ᶜ = (univ : Set X) :=
   (dense_compl_singleton x).closure_eq
 #align closure_compl_singleton closure_compl_singleton
 
 /-- If `x` is not an isolated point of a topological space, then the interior of `{x}` is empty. -/
 @[simp]
-theorem interior_singleton (x : α) [NeBot (𝓝[≠] x)] : interior {x} = (∅ : Set α) :=
+theorem interior_singleton (x : X) [NeBot (𝓝[≠] x)] : interior {x} = (∅ : Set X) :=
   interior_eq_empty_iff_dense_compl.2 (dense_compl_singleton x)
 #align interior_singleton interior_singleton
 
-theorem not_isOpen_singleton (x : α) [NeBot (𝓝[≠] x)] : ¬IsOpen ({x} : Set α) :=
+theorem not_isOpen_singleton (x : X) [NeBot (𝓝[≠] x)] : ¬IsOpen ({x} : Set X) :=
   dense_compl_singleton_iff_not_open.1 (dense_compl_singleton x)
 #align not_is_open_singleton not_isOpen_singleton
 
-theorem closure_eq_cluster_pts {s : Set α} : closure s = { a | ClusterPt a (𝓟 s) } :=
+theorem closure_eq_cluster_pts {s : Set X} : closure s = { a | ClusterPt a (𝓟 s) } :=
   Set.ext fun _ => mem_closure_iff_clusterPt
 #align closure_eq_cluster_pts closure_eq_cluster_pts
 
-theorem mem_closure_iff_nhds {s : Set α} {a : α} : a ∈ closure s ↔ ∀ t ∈ 𝓝 a, (t ∩ s).Nonempty :=
+theorem mem_closure_iff_nhds {s : Set X} {a : X} : a ∈ closure s ↔ ∀ t ∈ 𝓝 a, (t ∩ s).Nonempty :=
   mem_closure_iff_clusterPt.trans clusterPt_principal_iff
 #align mem_closure_iff_nhds mem_closure_iff_nhds
 
-theorem mem_closure_iff_nhds' {s : Set α} {a : α} : a ∈ closure s ↔ ∀ t ∈ 𝓝 a, ∃ y : s, ↑y ∈ t := by
+theorem mem_closure_iff_nhds' {s : Set X} {a : X} : a ∈ closure s ↔ ∀ t ∈ 𝓝 a, ∃ y : s, ↑y ∈ t := by
   simp only [mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]
 #align mem_closure_iff_nhds' mem_closure_iff_nhds'
 
-theorem mem_closure_iff_comap_neBot {A : Set α} {x : α} :
-    x ∈ closure A ↔ NeBot (comap ((↑) : A → α) (𝓝 x)) := by
+theorem mem_closure_iff_comap_neBot {A : Set X} {x : X} :
+    x ∈ closure A ↔ NeBot (comap ((↑) : A → X) (𝓝 x)) := by
   simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
     SetCoe.exists, exists_prop]
 #align mem_closure_iff_comap_ne_bot mem_closure_iff_comap_neBot
 
-theorem mem_closure_iff_nhds_basis' {a : α} {p : ι → Prop} {s : ι → Set α} (h : (𝓝 a).HasBasis p s)
-    {t : Set α} : a ∈ closure t ↔ ∀ i, p i → (s i ∩ t).Nonempty :=
+theorem mem_closure_iff_nhds_basis' {a : X} {p : ι → Prop} {s : ι → Set X} (h : (𝓝 a).HasBasis p s)
+    {t : Set X} : a ∈ closure t ↔ ∀ i, p i → (s i ∩ t).Nonempty :=
   mem_closure_iff_clusterPt.trans <|
     (h.clusterPt_iff (hasBasis_principal _)).trans <| by simp only [exists_prop, forall_const]
 #align mem_closure_iff_nhds_basis' mem_closure_iff_nhds_basis'
 
-theorem mem_closure_iff_nhds_basis {a : α} {p : ι → Prop} {s : ι → Set α} (h : (𝓝 a).HasBasis p s)
-    {t : Set α} : a ∈ closure t ↔ ∀ i, p i → ∃ y ∈ t, y ∈ s i :=
+theorem mem_closure_iff_nhds_basis {a : X} {p : ι → Prop} {s : ι → Set X} (h : (𝓝 a).HasBasis p s)
+    {t : Set X} : a ∈ closure t ↔ ∀ i, p i → ∃ y ∈ t, y ∈ s i :=
   (mem_closure_iff_nhds_basis' h).trans <| by
     simp only [Set.Nonempty, mem_inter_iff, exists_prop, and_comm]
 #align mem_closure_iff_nhds_basis mem_closure_iff_nhds_basis
 
-theorem clusterPt_iff_forall_mem_closure {F : Filter α} {a : α} :
+theorem clusterPt_iff_forall_mem_closure {F : Filter X} {a : X} :
     ClusterPt a F ↔ ∀ s ∈ F, a ∈ closure s := by
   simp_rw [ClusterPt, inf_neBot_iff, mem_closure_iff_nhds]
   rw [forall₂_swap]
 
-theorem clusterPt_iff_lift'_closure {F : Filter α} {a : α} :
+theorem clusterPt_iff_lift'_closure {F : Filter X} {a : X} :
     ClusterPt a F ↔ pure a ≤ (F.lift' closure) := by
   simp_rw [clusterPt_iff_forall_mem_closure,
     (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
     exists_const]
 
-theorem clusterPt_iff_lift'_closure' {F : Filter α} {a : α} :
+theorem clusterPt_iff_lift'_closure' {F : Filter X} {a : X} :
     ClusterPt a F ↔ (F.lift' closure ⊓ pure a).NeBot := by
   rw [clusterPt_iff_lift'_closure, ← Ultrafilter.coe_pure, inf_comm, Ultrafilter.inf_neBot_iff]
 
 @[simp]
-theorem clusterPt_lift'_closure_iff {F : Filter α} {a : α} :
+theorem clusterPt_lift'_closure_iff {F : Filter X} {a : X} :
     ClusterPt a (F.lift' closure) ↔ ClusterPt a F := by
-  simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure α) (monotone_closure α)]
+  simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure X) (monotone_closure X)]
 
 /-- `x` belongs to the closure of `s` if and only if some ultrafilter
   supported on `s` converges to `x`. -/
-theorem mem_closure_iff_ultrafilter {s : Set α} {x : α} :
-    x ∈ closure s ↔ ∃ u : Ultrafilter α, s ∈ u ∧ ↑u ≤ 𝓝 x := by
+theorem mem_closure_iff_ultrafilter {s : Set X} {x : X} :
+    x ∈ closure s ↔ ∃ u : Ultrafilter X, s ∈ u ∧ ↑u ≤ 𝓝 x := by
   simp [closure_eq_cluster_pts, ClusterPt, ← exists_ultrafilter_iff, and_comm]
 #align mem_closure_iff_ultrafilter mem_closure_iff_ultrafilter
 
-theorem isClosed_iff_clusterPt {s : Set α} : IsClosed s ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s :=
+theorem isClosed_iff_clusterPt {s : Set X} : IsClosed s ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s :=
   calc
     IsClosed s ↔ closure s ⊆ s := closure_subset_iff_isClosed.symm
     _ ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s := by simp only [subset_def, mem_closure_iff_clusterPt]
 #align is_closed_iff_cluster_pt isClosed_iff_clusterPt
 
-theorem isClosed_iff_nhds {s : Set α} :
+theorem isClosed_iff_nhds {s : Set X} :
     IsClosed s ↔ ∀ x, (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s := by
   simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff]
 #align is_closed_iff_nhds isClosed_iff_nhds
 
-lemma isClosed_iff_forall_filter {s : Set α} :
-    IsClosed s ↔ ∀ x, ∀ F : Filter α, F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s := by
+lemma isClosed_iff_forall_filter {s : Set X} :
+    IsClosed s ↔ ∀ x, ∀ F : Filter X, F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s := by
   simp_rw [isClosed_iff_clusterPt]
   exact ⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS),
          fun hs x hx ↦ hs x (𝓝 x ⊓ 𝓟 s) hx inf_le_right inf_le_left⟩
 
-theorem IsClosed.interior_union_left {s t : Set α} (_ : IsClosed s) :
+theorem IsClosed.interior_union_left {s t : Set X} (_ : IsClosed s) :
     interior (s ∪ t) ⊆ s ∪ interior t := fun a ⟨u, ⟨⟨hu₁, hu₂⟩, ha⟩⟩ =>
   (Classical.em (a ∈ s)).imp_right fun h =>
     mem_interior.mpr
@@ -1442,28 +1441,28 @@ theorem IsClosed.interior_union_left {s t : Set α} (_ : IsClosed s) :
         ⟨ha, h⟩⟩
 #align is_closed.interior_union_left IsClosed.interior_union_left
 
-theorem IsClosed.interior_union_right {s t : Set α} (h : IsClosed t) :
+theorem IsClosed.interior_union_right {s t : Set X} (h : IsClosed t) :
     interior (s ∪ t) ⊆ interior s ∪ t := by
   simpa only [union_comm _ t] using h.interior_union_left
 #align is_closed.interior_union_right IsClosed.interior_union_right
 
-theorem IsOpen.inter_closure {s t : Set α} (h : IsOpen s) : s ∩ closure t ⊆ closure (s ∩ t) :=
+theorem IsOpen.inter_closure {s t : Set X} (h : IsOpen s) : s ∩ closure t ⊆ closure (s ∩ t) :=
   compl_subset_compl.mp <| by
     simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl
 #align is_open.inter_closure IsOpen.inter_closure
 
-theorem IsOpen.closure_inter {s t : Set α} (h : IsOpen t) : closure s ∩ t ⊆ closure (s ∩ t) := by
+theorem IsOpen.closure_inter {s t : Set X} (h : IsOpen t) : closure s ∩ t ⊆ closure (s ∩ t) := by
   simpa only [inter_comm t] using h.inter_closure
 #align is_open.closure_inter IsOpen.closure_inter
 
-theorem Dense.open_subset_closure_inter {s t : Set α} (hs : Dense s) (ht : IsOpen t) :
+theorem Dense.open_subset_closure_inter {s t : Set X} (hs : Dense s) (ht : IsOpen t) :
     t ⊆ closure (t ∩ s) :=
   calc
     t = t ∩ closure s := by rw [hs.closure_eq, inter_univ]
     _ ⊆ closure (t ∩ s) := ht.inter_closure
 #align dense.open_subset_closure_inter Dense.open_subset_closure_inter
 
-theorem mem_closure_of_mem_closure_union {s₁ s₂ : Set α} {x : α} (h : x ∈ closure (s₁ ∪ s₂))
+theorem mem_closure_of_mem_closure_union {s₁ s₂ : Set X} {x : X} (h : x ∈ closure (s₁ ∪ s₂))
     (h₁ : s₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂ := by
   rw [mem_closure_iff_nhds_neBot] at *
   rwa [←
@@ -1476,24 +1475,24 @@ theorem mem_closure_of_mem_closure_union {s₁ s₂ : Set α} {x : α} (h : x 
 #align mem_closure_of_mem_closure_union mem_closure_of_mem_closure_union
 
 /-- The intersection of an open dense set with a dense set is a dense set. -/
-theorem Dense.inter_of_isOpen_left {s t : Set α} (hs : Dense s) (ht : Dense t) (hso : IsOpen s) :
+theorem Dense.inter_of_isOpen_left {s t : Set X} (hs : Dense s) (ht : Dense t) (hso : IsOpen s) :
     Dense (s ∩ t) := fun x =>
   closure_minimal hso.inter_closure isClosed_closure <| by simp [hs.closure_eq, ht.closure_eq]
 #align dense.inter_of_open_left Dense.inter_of_isOpen_left
 
 /-- The intersection of a dense set with an open dense set is a dense set. -/
-theorem Dense.inter_of_isOpen_right {s t : Set α} (hs : Dense s) (ht : Dense t) (hto : IsOpen t) :
+theorem Dense.inter_of_isOpen_right {s t : Set X} (hs : Dense s) (ht : Dense t) (hto : IsOpen t) :
     Dense (s ∩ t) :=
   inter_comm t s ▸ ht.inter_of_isOpen_left hs hto
 #align dense.inter_of_open_right Dense.inter_of_isOpen_right
 
-theorem Dense.inter_nhds_nonempty {s t : Set α} (hs : Dense s) {x : α} (ht : t ∈ 𝓝 x) :
+theorem Dense.inter_nhds_nonempty {s t : Set X} (hs : Dense s) {x : X} (ht : t ∈ 𝓝 x) :
     (s ∩ t).Nonempty :=
   let ⟨U, hsub, ho, hx⟩ := mem_nhds_iff.1 ht
   (hs.inter_open_nonempty U ho ⟨x, hx⟩).mono fun _y hy => ⟨hy.2, hsub hy.1⟩
 #align dense.inter_nhds_nonempty Dense.inter_nhds_nonempty
 
-theorem closure_diff {s t : Set α} : closure s \ closure t ⊆ closure (s \ t) :=
+theorem closure_diff {s t : Set X} : closure s \ closure t ⊆ closure (s \ t) :=
   calc
     closure s \ closure t = (closure t)ᶜ ∩ closure s := by simp only [diff_eq, inter_comm]
     _ ⊆ closure ((closure t)ᶜ ∩ s) := (isOpen_compl_iff.mpr <| isClosed_closure).inter_closure
@@ -1501,35 +1500,35 @@ theorem closure_diff {s t : Set α} : closure s \ closure t ⊆ closure (s \ t)
     _ ⊆ closure (s \ t) := closure_mono <| diff_subset_diff (Subset.refl s) subset_closure
 #align closure_diff closure_diff
 
-theorem Filter.Frequently.mem_of_closed {a : α} {s : Set α} (h : ∃ᶠ x in 𝓝 a, x ∈ s)
+theorem Filter.Frequently.mem_of_closed {a : X} {s : Set X} (h : ∃ᶠ x in 𝓝 a, x ∈ s)
     (hs : IsClosed s) : a ∈ s :=
   hs.closure_subset h.mem_closure
 #align filter.frequently.mem_of_closed Filter.Frequently.mem_of_closed
 
-theorem IsClosed.mem_of_frequently_of_tendsto {f : β → α} {b : Filter β} {a : α} {s : Set α}
+theorem IsClosed.mem_of_frequently_of_tendsto {f : α → X} {b : Filter α} {a : X} {s : Set X}
     (hs : IsClosed s) (h : ∃ᶠ x in b, f x ∈ s) (hf : Tendsto f b (𝓝 a)) : a ∈ s :=
   (hf.frequently <| show ∃ᶠ x in b, (fun y => y ∈ s) (f x) from h).mem_of_closed hs
 #align is_closed.mem_of_frequently_of_tendsto IsClosed.mem_of_frequently_of_tendsto
 
-theorem IsClosed.mem_of_tendsto {f : β → α} {b : Filter β} {a : α} {s : Set α} [NeBot b]
+theorem IsClosed.mem_of_tendsto {f : α → X} {b : Filter α} {a : X} {s : Set X} [NeBot b]
     (hs : IsClosed s) (hf : Tendsto f b (𝓝 a)) (h : ∀ᶠ x in b, f x ∈ s) : a ∈ s :=
   hs.mem_of_frequently_of_tendsto h.frequently hf
 #align is_closed.mem_of_tendsto IsClosed.mem_of_tendsto
 
-theorem mem_closure_of_frequently_of_tendsto {f : β → α} {b : Filter β} {a : α} {s : Set α}
+theorem mem_closure_of_frequently_of_tendsto {f : α → X} {b : Filter α} {a : X} {s : Set X}
     (h : ∃ᶠ x in b, f x ∈ s) (hf : Tendsto f b (𝓝 a)) : a ∈ closure s :=
   (hf.frequently h).mem_closure
 #align mem_closure_of_frequently_of_tendsto mem_closure_of_frequently_of_tendsto
 
-theorem mem_closure_of_tendsto {f : β → α} {b : Filter β} {a : α} {s : Set α} [NeBot b]
+theorem mem_closure_of_tendsto {f : α → X} {b : Filter α} {a : X} {s : Set X} [NeBot b]
     (hf : Tendsto f b (𝓝 a)) (h : ∀ᶠ x in b, f x ∈ s) : a ∈ closure s :=
   mem_closure_of_frequently_of_tendsto h.frequently hf
 #align mem_closure_of_tendsto mem_closure_of_tendsto
 
 /-- Suppose that `f` sends the complement to `s` to a single point `a`, and `l` is some filter.
 Then `f` tends to `a` along `l` restricted to `s` if and only if it tends to `a` along `l`. -/
-theorem tendsto_inf_principal_nhds_iff_of_forall_eq {f : β → α} {l : Filter β} {s : Set β} {a : α}
-    (h : ∀ (x) (_ : x ∉ s), f x = a) : Tendsto f (l ⊓ 𝓟 s) (𝓝 a) ↔ Tendsto f l (𝓝 a) := by
+theorem tendsto_inf_principal_nhds_iff_of_forall_eq {f : α → X} {l : Filter α} {s : Set α} {a : X}
+    (h : ∀ x ∉ s, f x = a) : Tendsto f (l ⊓ 𝓟 s) (𝓝 a) ↔ Tendsto f l (𝓝 a) := by
   rw [tendsto_iff_comap, tendsto_iff_comap]
   replace h : 𝓟 sᶜ ≤ comap f (𝓝 a)
   · rintro U ⟨t, ht, htU⟩ x hx
@@ -1558,37 +1557,37 @@ section lim
 set_option linter.uppercaseLean3 false
 
 /-- If `f` is a filter, then `Filter.lim f` is a limit of the filter, if it exists. -/
-noncomputable def lim [Nonempty α] (f : Filter α) : α :=
+noncomputable def lim [Nonempty X] (f : Filter X) : X :=
   Classical.epsilon fun a => f ≤ 𝓝 a
 #align Lim lim
 
 /--
 If `F` is an ultrafilter, then `Filter.Ultrafilter.lim F` is a limit of the filter, if it exists.
-Note that dot notation `F.lim` can be used for `F : Filter.Ultrafilter α`.
+Note that dot notation `F.lim` can be used for `F : Filter.Ultrafilter X`.
 -/
-noncomputable nonrec def Ultrafilter.lim (F : Ultrafilter α) : α :=
-  @lim α _ (nonempty_of_neBot F) F
+noncomputable nonrec def Ultrafilter.lim (F : Ultrafilter X) : X :=
+  @lim X _ (nonempty_of_neBot F) F
 #align ultrafilter.Lim Ultrafilter.lim
 
-/-- If `f` is a filter in `β` and `g : β → α` is a function, then `limUnder f g` is a limit of `g`
+/-- If `f` is a filter in `α` and `g : α → X` is a function, then `limUnder f g` is a limit of `g`
 at `f`, if it exists. -/
-noncomputable def limUnder [Nonempty α] (f : Filter β) (g : β → α) : α :=
+noncomputable def limUnder [Nonempty X] (f : Filter α) (g : α → X) : X :=
   lim (f.map g)
 #align lim limUnder
 
 /-- If a filter `f` is majorated by some `𝓝 a`, then it is majorated by `𝓝 (Filter.lim f)`. We
-formulate this lemma with a `[Nonempty α]` argument of `lim` derived from `h` to make it useful for
-types without a `[Nonempty α]` instance. Because of the built-in proof irrelevance, Lean will unify
+formulate this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for
+types without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify
 this instance with any other instance. -/
-theorem le_nhds_lim {f : Filter α} (h : ∃ a, f ≤ 𝓝 a) : f ≤ 𝓝 (@lim _ _ (nonempty_of_exists h) f) :=
+theorem le_nhds_lim {f : Filter X} (h : ∃ a, f ≤ 𝓝 a) : f ≤ 𝓝 (@lim _ _ (nonempty_of_exists h) f) :=
   Classical.epsilon_spec h
 #align le_nhds_Lim le_nhds_lim
 
 /-- If `g` tends to some `𝓝 a` along `f`, then it tends to `𝓝 (Filter.limUnder f g)`. We formulate
-this lemma with a `[Nonempty α]` argument of `lim` derived from `h` to make it useful for types
-without a `[Nonempty α]` instance. Because of the built-in proof irrelevance, Lean will unify this
+this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for types
+without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify this
 instance with any other instance. -/
-theorem tendsto_nhds_limUnder {f : Filter β} {g : β → α} (h : ∃ a, Tendsto g f (𝓝 a)) :
+theorem tendsto_nhds_limUnder {f : Filter α} {g : α → X} (h : ∃ a, Tendsto g f (𝓝 a)) :
     Tendsto g f (𝓝 (@limUnder _ _ _ (nonempty_of_exists h) f g)) :=
   le_nhds_lim h
 #align tendsto_nhds_lim tendsto_nhds_limUnder
@@ -1605,15 +1604,13 @@ open Topology
 
 section Continuous
 
-variable {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
-
-variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]
+variable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
 
 open TopologicalSpace
 
 /-- A function between topological spaces is continuous if the preimage
   of every open set is open. Registered as a structure to make sure it is not unfolded by Lean. -/
-structure Continuous (f : α → β) : Prop where
+structure Continuous (f : X → Y) : Prop where
   /-- The preimage of an open set under a continuous function is an open set. Use `IsOpen.preimage`
   instead. -/
   isOpen_preimage : ∀ s, IsOpen s → IsOpen (f ⁻¹' s)
@@ -1624,227 +1621,227 @@ set_option quotPrecheck false in
 scoped[Topology] notation (name := Continuous_of) "Continuous[" t₁ ", " t₂ "]" =>
   @Continuous _ _ t₁ t₂
 
-theorem continuous_def {_ : TopologicalSpace α} {_ : TopologicalSpace β} {f : α → β} :
+theorem continuous_def {_ : TopologicalSpace X} {_ : TopologicalSpace Y} {f : X → Y} :
     Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) :=
   ⟨fun hf => hf.1, fun h => ⟨h⟩⟩
 #align continuous_def continuous_def
 
-theorem IsOpen.preimage {f : α → β} (hf : Continuous f) {s : Set β} (h : IsOpen s) :
+theorem IsOpen.preimage {f : X → Y} (hf : Continuous f) {s : Set Y} (h : IsOpen s) :
     IsOpen (f ⁻¹' s) :=
   hf.isOpen_preimage s h
 #align is_open.preimage IsOpen.preimage
 
-theorem continuous_congr {f g : α → β} (h : ∀ x, f x = g x) :
+theorem continuous_congr {f g : X → Y} (h : ∀ x, f x = g x) :
     Continuous f ↔ Continuous g :=
   .of_eq <| congrArg _ <| funext h
 
-theorem Continuous.congr {f g : α → β} (h : Continuous f) (h' : ∀ x, f x = g x) : Continuous g :=
+theorem Continuous.congr {f g : X → Y} (h : Continuous f) (h' : ∀ x, f x = g x) : Continuous g :=
   continuous_congr h' |>.mp h
 #align continuous.congr Continuous.congr
 
 /-- A function between topological spaces is continuous at a point `x₀`
 if `f x` tends to `f x₀` when `x` tends to `x₀`. -/
-def ContinuousAt (f : α → β) (x : α) :=
+def ContinuousAt (f : X → Y) (x : X) :=
   Tendsto f (𝓝 x) (𝓝 (f x))
 #align continuous_at ContinuousAt
 
-theorem ContinuousAt.tendsto {f : α → β} {x : α} (h : ContinuousAt f x) :
+theorem ContinuousAt.tendsto {f : X → Y} {x : X} (h : ContinuousAt f x) :
     Tendsto f (𝓝 x) (𝓝 (f x)) :=
   h
 #align continuous_at.tendsto ContinuousAt.tendsto
 
-theorem continuousAt_def {f : α → β} {x : α} : ContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x :=
+theorem continuousAt_def {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x :=
   Iff.rfl
 #align continuous_at_def continuousAt_def
 
-theorem continuousAt_congr {f g : α → β} {x : α} (h : f =ᶠ[𝓝 x] g) :
+theorem continuousAt_congr {f g : X → Y} {x : X} (h : f =ᶠ[𝓝 x] g) :
     ContinuousAt f x ↔ ContinuousAt g x := by
   simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds]
 #align continuous_at_congr continuousAt_congr
 
-theorem ContinuousAt.congr {f g : α → β} {x : α} (hf : ContinuousAt f x) (h : f =ᶠ[𝓝 x] g) :
+theorem ContinuousAt.congr {f g : X → Y} {x : X} (hf : ContinuousAt f x) (h : f =ᶠ[𝓝 x] g) :
     ContinuousAt g x :=
   (continuousAt_congr h).1 hf
 #align continuous_at.congr ContinuousAt.congr
 
-theorem ContinuousAt.preimage_mem_nhds {f : α → β} {x : α} {t : Set β} (h : ContinuousAt f x)
+theorem ContinuousAt.preimage_mem_nhds {f : X → Y} {x : X} {t : Set Y} (h : ContinuousAt f x)
     (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝 x :=
   h ht
 #align continuous_at.preimage_mem_nhds ContinuousAt.preimage_mem_nhds
 
 /-- Deprecated, please use `not_mem_tsupport_iff_eventuallyEq` instead. -/
 @[deprecated] -- 15 January 2024
-theorem eventuallyEq_zero_nhds {M₀} [Zero M₀] {a : α} {f : α → M₀} :
+theorem eventuallyEq_zero_nhds {M₀} [Zero M₀] {a : X} {f : X → M₀} :
     f =ᶠ[𝓝 a] 0 ↔ a ∉ closure (Function.support f) := by
   rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds, Function.compl_support,
     EventuallyEq, eventually_iff]
   simp only [Pi.zero_apply]
 #align eventually_eq_zero_nhds eventuallyEq_zero_nhds
 
-theorem ClusterPt.map {x : α} {la : Filter α} {lb : Filter β} (H : ClusterPt x la) {f : α → β}
+theorem ClusterPt.map {x : X} {la : Filter X} {lb : Filter Y} (H : ClusterPt x la) {f : X → Y}
     (hfc : ContinuousAt f x) (hf : Tendsto f la lb) : ClusterPt (f x) lb :=
   (NeBot.map H f).mono <| hfc.tendsto.inf hf
 #align cluster_pt.map ClusterPt.map
 
 /-- See also `interior_preimage_subset_preimage_interior`. -/
-theorem preimage_interior_subset_interior_preimage {f : α → β} {s : Set β} (hf : Continuous f) :
+theorem preimage_interior_subset_interior_preimage {f : X → Y} {s : Set Y} (hf : Continuous f) :
     f ⁻¹' interior s ⊆ interior (f ⁻¹' s) :=
   interior_maximal (preimage_mono interior_subset) (isOpen_interior.preimage hf)
 #align preimage_interior_subset_interior_preimage preimage_interior_subset_interior_preimage
 
 @[continuity]
-theorem continuous_id : Continuous (id : α → α) :=
+theorem continuous_id : Continuous (id : X → X) :=
   continuous_def.2 fun _ => id
 #align continuous_id continuous_id
 
 -- This is needed due to reducibility issues with the `continuity` tactic.
 @[continuity]
-theorem continuous_id' : Continuous (fun (x : α) => x) := continuous_id
+theorem continuous_id' : Continuous (fun (x : X) => x) := continuous_id
 
-theorem Continuous.comp {g : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) :
+theorem Continuous.comp {g : Y → Z} {f : X → Y} (hg : Continuous g) (hf : Continuous f) :
     Continuous (g ∘ f) :=
   continuous_def.2 fun _ h => (h.preimage hg).preimage hf
 #align continuous.comp Continuous.comp
 
 -- This is needed due to reducibility issues with the `continuity` tactic.
 @[continuity]
-theorem Continuous.comp' {g : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) :
+theorem Continuous.comp' {g : Y → Z} {f : X → Y} (hg : Continuous g) (hf : Continuous f) :
     Continuous (fun x => g (f x)) := hg.comp hf
 
-theorem Continuous.iterate {f : α → α} (h : Continuous f) (n : ℕ) : Continuous f^[n] :=
+theorem Continuous.iterate {f : X → X} (h : Continuous f) (n : ℕ) : Continuous f^[n] :=
   Nat.recOn n continuous_id fun _ ihn => ihn.comp h
 #align continuous.iterate Continuous.iterate
 
-nonrec theorem ContinuousAt.comp {g : β → γ} {f : α → β} {x : α} (hg : ContinuousAt g (f x))
+nonrec theorem ContinuousAt.comp {g : Y → Z} {f : X → Y} {x : X} (hg : ContinuousAt g (f x))
     (hf : ContinuousAt f x) : ContinuousAt (g ∘ f) x :=
   hg.comp hf
 #align continuous_at.comp ContinuousAt.comp
 
 /-- See note [comp_of_eq lemmas] -/
-theorem ContinuousAt.comp_of_eq {g : β → γ} {f : α → β} {x : α} {y : β} (hg : ContinuousAt g y)
+theorem ContinuousAt.comp_of_eq {g : Y → Z} {f : X → Y} {x : X} {y : Y} (hg : ContinuousAt g y)
     (hf : ContinuousAt f x) (hy : f x = y) : ContinuousAt (g ∘ f) x := by subst hy; exact hg.comp hf
 #align continuous_at.comp_of_eq ContinuousAt.comp_of_eq
 
-theorem Continuous.tendsto {f : α → β} (hf : Continuous f) (x) : Tendsto f (𝓝 x) (𝓝 (f x)) :=
+theorem Continuous.tendsto {f : X → Y} (hf : Continuous f) (x) : Tendsto f (𝓝 x) (𝓝 (f x)) :=
   ((nhds_basis_opens x).tendsto_iff <| nhds_basis_opens <| f x).2 fun t ⟨hxt, ht⟩ =>
     ⟨f ⁻¹' t, ⟨hxt, ht.preimage hf⟩, Subset.rfl⟩
 #align continuous.tendsto Continuous.tendsto
 
 /-- A version of `Continuous.tendsto` that allows one to specify a simpler form of the limit.
 E.g., one can write `continuous_exp.tendsto' 0 1 exp_zero`. -/
-theorem Continuous.tendsto' {f : α → β} (hf : Continuous f) (x : α) (y : β) (h : f x = y) :
+theorem Continuous.tendsto' {f : X → Y} (hf : Continuous f) (x : X) (y : Y) (h : f x = y) :
     Tendsto f (𝓝 x) (𝓝 y) :=
   h ▸ hf.tendsto x
 #align continuous.tendsto' Continuous.tendsto'
 
-theorem Continuous.continuousAt {f : α → β} {x : α} (h : Continuous f) : ContinuousAt f x :=
+theorem Continuous.continuousAt {f : X → Y} {x : X} (h : Continuous f) : ContinuousAt f x :=
   h.tendsto x
 #align continuous.continuous_at Continuous.continuousAt
 
-theorem continuous_iff_continuousAt {f : α → β} : Continuous f ↔ ∀ x, ContinuousAt f x :=
+theorem continuous_iff_continuousAt {f : X → Y} : Continuous f ↔ ∀ x, ContinuousAt f x :=
   ⟨Continuous.tendsto, fun hf => continuous_def.2 fun _U hU => isOpen_iff_mem_nhds.2 fun x hx =>
     hf x <| hU.mem_nhds hx⟩
 #align continuous_iff_continuous_at continuous_iff_continuousAt
 
-theorem continuousAt_const {x : α} {b : β} : ContinuousAt (fun _ : α => b) x :=
+theorem continuousAt_const {x : X} {b : Y} : ContinuousAt (fun _ : X => b) x :=
   tendsto_const_nhds
 #align continuous_at_const continuousAt_const
 
 @[continuity]
-theorem continuous_const {b : β} : Continuous fun _ : α => b :=
+theorem continuous_const {b : Y} : Continuous fun _ : X => b :=
   continuous_iff_continuousAt.mpr fun _ => continuousAt_const
 #align continuous_const continuous_const
 
-theorem Filter.EventuallyEq.continuousAt {x : α} {f : α → β} {y : β} (h : f =ᶠ[𝓝 x] fun _ => y) :
+theorem Filter.EventuallyEq.continuousAt {x : X} {f : X → Y} {y : Y} (h : f =ᶠ[𝓝 x] fun _ => y) :
     ContinuousAt f x :=
   (continuousAt_congr h).2 tendsto_const_nhds
 #align filter.eventually_eq.continuous_at Filter.EventuallyEq.continuousAt
 
-theorem continuous_of_const {f : α → β} (h : ∀ x y, f x = f y) : Continuous f :=
+theorem continuous_of_const {f : X → Y} (h : ∀ x y, f x = f y) : Continuous f :=
   continuous_iff_continuousAt.mpr fun x =>
     Filter.EventuallyEq.continuousAt <| eventually_of_forall fun y => h y x
 #align continuous_of_const continuous_of_const
 
-theorem continuousAt_id {x : α} : ContinuousAt id x :=
+theorem continuousAt_id {x : X} : ContinuousAt id x :=
   continuous_id.continuousAt
 #align continuous_at_id continuousAt_id
 
-theorem ContinuousAt.iterate {f : α → α} {x : α} (hf : ContinuousAt f x) (hx : f x = x) (n : ℕ) :
+theorem ContinuousAt.iterate {f : X → X} {x : X} (hf : ContinuousAt f x) (hx : f x = x) (n : ℕ) :
     ContinuousAt f^[n] x :=
   Nat.recOn n continuousAt_id fun n ihn =>
     show ContinuousAt (f^[n] ∘ f) x from ContinuousAt.comp (hx.symm ▸ ihn) hf
 #align continuous_at.iterate ContinuousAt.iterate
 
-theorem continuous_iff_isClosed {f : α → β} : Continuous f ↔ ∀ s, IsClosed s → IsClosed (f ⁻¹' s) :=
+theorem continuous_iff_isClosed {f : X → Y} : Continuous f ↔ ∀ s, IsClosed s → IsClosed (f ⁻¹' s) :=
   continuous_def.trans <| compl_surjective.forall.trans <| by
     simp only [isOpen_compl_iff, preimage_compl]
 #align continuous_iff_is_closed continuous_iff_isClosed
 
-theorem IsClosed.preimage {f : α → β} (hf : Continuous f) {s : Set β} (h : IsClosed s) :
+theorem IsClosed.preimage {f : X → Y} (hf : Continuous f) {s : Set Y} (h : IsClosed s) :
     IsClosed (f ⁻¹' s) :=
   continuous_iff_isClosed.mp hf s h
 #align is_closed.preimage IsClosed.preimage
 
-theorem mem_closure_image {f : α → β} {x : α} {s : Set α} (hf : ContinuousAt f x)
+theorem mem_closure_image {f : X → Y} {x : X} {s : Set X} (hf : ContinuousAt f x)
     (hx : x ∈ closure s) : f x ∈ closure (f '' s) :=
   mem_closure_of_frequently_of_tendsto
     ((mem_closure_iff_frequently.1 hx).mono fun _ => mem_image_of_mem _) hf
 #align mem_closure_image mem_closure_image
 
-theorem continuousAt_iff_ultrafilter {f : α → β} {x} :
-    ContinuousAt f x ↔ ∀ g : Ultrafilter α, ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x)) :=
+theorem continuousAt_iff_ultrafilter {f : X → Y} {x} :
+    ContinuousAt f x ↔ ∀ g : Ultrafilter X, ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x)) :=
   tendsto_iff_ultrafilter f (𝓝 x) (𝓝 (f x))
 #align continuous_at_iff_ultrafilter continuousAt_iff_ultrafilter
 
-theorem continuous_iff_ultrafilter {f : α → β} :
-    Continuous f ↔ ∀ (x) (g : Ultrafilter α), ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x)) := by
+theorem continuous_iff_ultrafilter {f : X → Y} :
+    Continuous f ↔ ∀ (x) (g : Ultrafilter X), ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x)) := by
   simp only [continuous_iff_continuousAt, continuousAt_iff_ultrafilter]
 #align continuous_iff_ultrafilter continuous_iff_ultrafilter
 
-theorem Continuous.closure_preimage_subset {f : α → β} (hf : Continuous f) (t : Set β) :
+theorem Continuous.closure_preimage_subset {f : X → Y} (hf : Continuous f) (t : Set Y) :
     closure (f ⁻¹' t) ⊆ f ⁻¹' closure t := by
   rw [← (isClosed_closure.preimage hf).closure_eq]
   exact closure_mono (preimage_mono subset_closure)
 #align continuous.closure_preimage_subset Continuous.closure_preimage_subset
 
-theorem Continuous.frontier_preimage_subset {f : α → β} (hf : Continuous f) (t : Set β) :
+theorem Continuous.frontier_preimage_subset {f : X → Y} (hf : Continuous f) (t : Set Y) :
     frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t :=
   diff_subset_diff (hf.closure_preimage_subset t) (preimage_interior_subset_interior_preimage hf)
 #align continuous.frontier_preimage_subset Continuous.frontier_preimage_subset
 
 /-- If a continuous map `f` maps `s` to `t`, then it maps `closure s` to `closure t`. -/
-protected theorem Set.MapsTo.closure {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t)
+protected theorem Set.MapsTo.closure {s : Set X} {t : Set Y} {f : X → Y} (h : MapsTo f s t)
     (hc : Continuous f) : MapsTo f (closure s) (closure t) := by
   simp only [MapsTo, mem_closure_iff_clusterPt]
   exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)
 #align set.maps_to.closure Set.MapsTo.closure
 
 /-- See also `IsClosedMap.closure_image_eq_of_continuous`. -/
-theorem image_closure_subset_closure_image {f : α → β} {s : Set α} (h : Continuous f) :
+theorem image_closure_subset_closure_image {f : X → Y} {s : Set X} (h : Continuous f) :
     f '' closure s ⊆ closure (f '' s) :=
   ((mapsTo_image f s).closure h).image_subset
 #align image_closure_subset_closure_image image_closure_subset_closure_image
 
 -- porting note: new lemma
-theorem closure_image_closure {f : α → β} {s : Set α} (h : Continuous f) :
+theorem closure_image_closure {f : X → Y} {s : Set X} (h : Continuous f) :
     closure (f '' closure s) = closure (f '' s) :=
   Subset.antisymm
     (closure_minimal (image_closure_subset_closure_image h) isClosed_closure)
     (closure_mono <| image_subset _ subset_closure)
 
-theorem closure_subset_preimage_closure_image {f : α → β} {s : Set α} (h : Continuous f) :
+theorem closure_subset_preimage_closure_image {f : X → Y} {s : Set X} (h : Continuous f) :
     closure s ⊆ f ⁻¹' closure (f '' s) := by
   rw [← Set.image_subset_iff]
   exact image_closure_subset_closure_image h
 #align closure_subset_preimage_closure_image closure_subset_preimage_closure_image
 
-theorem map_mem_closure {s : Set α} {t : Set β} {f : α → β} {a : α} (hf : Continuous f)
+theorem map_mem_closure {s : Set X} {t : Set Y} {f : X → Y} {a : X} (hf : Continuous f)
     (ha : a ∈ closure s) (ht : MapsTo f s t) : f a ∈ closure t :=
   ht.closure hf ha
 #align map_mem_closure map_mem_closure
 
 /-- If a continuous map `f` maps `s` to a closed set `t`, then it maps `closure s` to `t`. -/
-theorem Set.MapsTo.closure_left {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t)
+theorem Set.MapsTo.closure_left {s : Set X} {t : Set Y} {f : X → Y} (h : MapsTo f s t)
     (hc : Continuous f) (ht : IsClosed t) : MapsTo f (closure s) t :=
   ht.closure_eq ▸ h.closure hc
 #align set.maps_to.closure_left Set.MapsTo.closure_left
@@ -1855,9 +1852,9 @@ theorem Set.MapsTo.closure_left {s : Set α} {t : Set β} {f : α → β} (h : M
 
 section DenseRange
 
-variable {κ ι : Type*} (f : κ → β) (g : β → γ)
+variable {α ι : Type*} (f : α → X) (g : X → Y)
 
-/-- `f : ι → β` has dense range if its range (image) is a dense subset of β. -/
+/-- `f : α → X` has dense range if its range (image) is a dense subset of `X`. -/
 def DenseRange := Dense (range f)
 #align dense_range DenseRange
 
@@ -1868,7 +1865,7 @@ theorem Function.Surjective.denseRange (hf : Function.Surjective f) : DenseRange
   simp [hf.range_eq]
 #align function.surjective.dense_range Function.Surjective.denseRange
 
-theorem denseRange_id : DenseRange (id : α → α) :=
+theorem denseRange_id : DenseRange (id : X → X) :=
   Function.Surjective.denseRange Function.surjective_id
 #align dense_range_id denseRange_id
 
@@ -1880,25 +1877,25 @@ theorem DenseRange.closure_range (h : DenseRange f) : closure (range f) = univ :
   h.closure_eq
 #align dense_range.closure_range DenseRange.closure_range
 
-theorem Dense.denseRange_val {s : Set α} (h : Dense s) : DenseRange ((↑) : s → α) := by
+theorem Dense.denseRange_val {s : Set X} (h : Dense s) : DenseRange ((↑) : s → X) := by
   simpa only [DenseRange, Subtype.range_coe_subtype]
 #align dense.dense_range_coe Dense.denseRange_val
 
-theorem Continuous.range_subset_closure_image_dense {f : α → β} (hf : Continuous f) {s : Set α}
+theorem Continuous.range_subset_closure_image_dense {f : X → Y} (hf : Continuous f) {s : Set X}
     (hs : Dense s) : range f ⊆ closure (f '' s) := by
   rw [← image_univ, ← hs.closure_eq]
   exact image_closure_subset_closure_image hf
 #align continuous.range_subset_closure_image_dense Continuous.range_subset_closure_image_dense
 
 /-- The image of a dense set under a continuous map with dense range is a dense set. -/
-theorem DenseRange.dense_image {f : α → β} (hf' : DenseRange f) (hf : Continuous f) {s : Set α}
+theorem DenseRange.dense_image {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) {s : Set X}
     (hs : Dense s) : Dense (f '' s) :=
   (hf'.mono <| hf.range_subset_closure_image_dense hs).of_closure
 #align dense_range.dense_image DenseRange.dense_image
 
 /-- If `f` has dense range and `s` is an open set in the codomain of `f`, then the image of the
 preimage of `s` under `f` is dense in `s`. -/
-theorem DenseRange.subset_closure_image_preimage_of_isOpen (hf : DenseRange f) {s : Set β}
+theorem DenseRange.subset_closure_image_preimage_of_isOpen (hf : DenseRange f) {s : Set X}
     (hs : IsOpen s) : s ⊆ closure (f '' (f ⁻¹' s)) := by
   rw [image_preimage_eq_inter_range]
   exact hf.open_subset_closure_inter hs
@@ -1906,38 +1903,38 @@ theorem DenseRange.subset_closure_image_preimage_of_isOpen (hf : DenseRange f) {
 
 /-- If a continuous map with dense range maps a dense set to a subset of `t`, then `t` is a dense
 set. -/
-theorem DenseRange.dense_of_mapsTo {f : α → β} (hf' : DenseRange f) (hf : Continuous f) {s : Set α}
-    (hs : Dense s) {t : Set β} (ht : MapsTo f s t) : Dense t :=
+theorem DenseRange.dense_of_mapsTo {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) {s : Set X}
+    (hs : Dense s) {t : Set Y} (ht : MapsTo f s t) : Dense t :=
   (hf'.dense_image hf hs).mono ht.image_subset
 #align dense_range.dense_of_maps_to DenseRange.dense_of_mapsTo
 
 /-- Composition of a continuous map with dense range and a function with dense range has dense
 range. -/
-theorem DenseRange.comp {g : β → γ} {f : κ → β} (hg : DenseRange g) (hf : DenseRange f)
+theorem DenseRange.comp {g : Y → Z} {f : α → Y} (hg : DenseRange g) (hf : DenseRange f)
     (cg : Continuous g) : DenseRange (g ∘ f) := by
   rw [DenseRange, range_comp]
   exact hg.dense_image cg hf
 #align dense_range.comp DenseRange.comp
 
-nonrec theorem DenseRange.nonempty_iff (hf : DenseRange f) : Nonempty κ ↔ Nonempty β :=
+nonrec theorem DenseRange.nonempty_iff (hf : DenseRange f) : Nonempty α ↔ Nonempty X :=
   range_nonempty_iff_nonempty.symm.trans hf.nonempty_iff
 #align dense_range.nonempty_iff DenseRange.nonempty_iff
 
-theorem DenseRange.nonempty [h : Nonempty β] (hf : DenseRange f) : Nonempty κ :=
+theorem DenseRange.nonempty [h : Nonempty X] (hf : DenseRange f) : Nonempty α :=
   hf.nonempty_iff.mpr h
 #align dense_range.nonempty DenseRange.nonempty
 
-/-- Given a function `f : α → β` with dense range and `b : β`, returns some `a : α`. -/
-def DenseRange.some (hf : DenseRange f) (b : β) : κ :=
+/-- Given a function `f : X → Y` with dense range and `b : Y`, returns some `a : X`. -/
+def DenseRange.some (hf : DenseRange f) (b : X) : α :=
   Classical.choice <| hf.nonempty_iff.mpr ⟨b⟩
 #align dense_range.some DenseRange.some
 
-nonrec theorem DenseRange.exists_mem_open (hf : DenseRange f) {s : Set β} (ho : IsOpen s)
+nonrec theorem DenseRange.exists_mem_open (hf : DenseRange f) {s : Set X} (ho : IsOpen s)
     (hs : s.Nonempty) : ∃ a, f a ∈ s :=
   exists_range_iff.1 <| hf.exists_mem_open ho hs
 #align dense_range.exists_mem_open DenseRange.exists_mem_open
 
-theorem DenseRange.mem_nhds {f : κ → β} (h : DenseRange f) {b : β} {U : Set β} (U_in : U ∈ 𝓝 b) :
+theorem DenseRange.mem_nhds (h : DenseRange f) {b : X} {U : Set X} (U_in : U ∈ 𝓝 b) :
     ∃ a, f a ∈ U :=
   let ⟨a, ha⟩ := h.exists_mem_open isOpen_interior ⟨b, mem_interior_iff_mem_nhds.2 U_in⟩
   ⟨a, interior_subset ha⟩
@@ -1991,7 +1988,7 @@ This has the following advantages
 
 As an example for a unary operation, we have `Continuous.neg`.
 ```
-Continuous.neg {f : α → G} (hf : Continuous f) : Continuous (fun x ↦ -f x)
+Continuous.neg {f : X → G} (hf : Continuous f) : Continuous (fun x ↦ -f x)
 ```
 For unary functions, the elaborator is not confused when applying the traditional lemma
 (like `continuous_neg`), but it's still convenient to have the short version available (compare
@@ -2063,7 +2060,7 @@ Only after elaborating the two `ContinuousAt` arguments, Lean will try to unify
 which is often easy after having chosen the correct functions for `f` and `g`.
 Here is an example that shows the difference:
 ```
-example [TopologicalSpace α] [TopologicalSpace β] {x₀ : α} (f : α → α → β)
+example [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} (f : X → X → Y)
     (hf : ContinuousAt (Function.uncurry f) (x₀, x₀)) :
     ContinuousAt (fun x ↦ f x x) x₀ :=
   -- hf.comp (continuousAt_id.prod continuousAt_id) -- type mismatch

From 3edf9a838b7e9ae619a982c45dc32328e39e5f61 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 23 Jan 2024 23:06:07 -0600
Subject: [PATCH 2/5] Fix, golf a bit

---
 Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean | 2 +-
 Mathlib/Topology/Algebra/InfiniteSum/Basic.lean    | 6 ++----
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
index 861dedace3e67..4f4c3d8d2614e 100644
--- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
+++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
@@ -642,7 +642,7 @@ theorem localization_comap_inducing [Algebra R S] (M : Submonoid R) [IsLocalizat
   constructor
   rw [TopologicalSpace.ext_iff]
   intro U
-  rw [← isClosed_compl_iff, ← @isClosed_compl_iff (α := PrimeSpectrum S) (s := U)]
+  rw [← isClosed_compl_iff, ← @isClosed_compl_iff (X := PrimeSpectrum S) (s := U)]
   generalize Uᶜ = Z
   simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus]
   constructor
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
index 23a6b5c68250c..6a611f49ab007 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
@@ -1028,10 +1028,8 @@ theorem tendsto_sum_nat_add [T2Space α] (f : ℕ → α) :
       rw [sub_eq_iff_eq_add, add_comm, sum_add_tsum_nat_add i hf]
     have h₁ : Tendsto (fun _ : ℕ => ∑' i, f i) atTop (𝓝 (∑' i, f i)) := tendsto_const_nhds
     simpa only [h₀, sub_self] using Tendsto.sub h₁ hf.hasSum.tendsto_sum_nat
-  · convert tendsto_const_nhds (α := α) (β := ℕ) (a := 0) (f := atTop)
-    rename_i i
-    rw [← summable_nat_add_iff i] at hf
-    exact tsum_eq_zero_of_not_summable hf
+  · refine tendsto_const_nhds.congr fun n ↦ (tsum_eq_zero_of_not_summable ?_).symm
+    rwa [summable_nat_add_iff n]
 #align tendsto_sum_nat_add tendsto_sum_nat_add
 
 /-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both convergent then so is the `ℤ`-indexed

From 2a3488594def71e2eb97c09a9df61b09bca79908 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 23 Jan 2024 23:26:52 -0600
Subject: [PATCH 3/5] Fix, golf

---
 Mathlib/Topology/Algebra/InfiniteSum/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
index 6a611f49ab007..e8f00715ed372 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
@@ -1315,8 +1315,7 @@ theorem tendsto_tsum_compl_atTop_zero (f : α → G) :
     obtain ⟨s, hs⟩ := H.tsum_vanishing he
     rw [Filter.mem_map, mem_atTop_sets]
     exact ⟨s, fun t hts ↦ hs _ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩
-  · convert tendsto_const_nhds (α := G) (β := Finset α) (f := atTop) (a := 0)
-    apply tsum_eq_zero_of_not_summable
+  · refine tendsto_const_nhds.congr fun _ ↦ (tsum_eq_zero_of_not_summable ?_).symm
     rwa [Finset.summable_compl_iff]
 #align tendsto_tsum_compl_at_top_zero tendsto_tsum_compl_atTop_zero
 

From 9997e759c676e3005a4a303cec5638258506dce2 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 24 Jan 2024 00:02:02 -0600
Subject: [PATCH 4/5] Fix

---
 Mathlib/Topology/MetricSpace/Polish.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Topology/MetricSpace/Polish.lean b/Mathlib/Topology/MetricSpace/Polish.lean
index a4df6bfea158c..232d2b160fe09 100644
--- a/Mathlib/Topology/MetricSpace/Polish.lean
+++ b/Mathlib/Topology/MetricSpace/Polish.lean
@@ -406,8 +406,7 @@ theorem _root_.IsClosed.isClopenable [TopologicalSpace α] [PolishSpace α] {s :
   · rw [← f.induced_symm]
     exact f.symm.polishSpace_induced
   · rw [isOpen_coinduced, isOpen_sum_iff]
-    convert And.intro (isOpen_univ (α := s)) (isOpen_empty (α := (sᶜ : Set α)))
-      <;> ext ⟨x, hx⟩ <;> simpa using hx
+    simp [preimage_preimage]
 #align is_closed.is_clopenable IsClosed.isClopenable
 
 theorem IsClopenable.compl [TopologicalSpace α] {s : Set α} (hs : IsClopenable s) :

From 7c3c1947ca8893bc00c1f0d2947896e76e80ef55 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 24 Jan 2024 00:18:05 -0600
Subject: [PATCH 5/5] Fix more

---
 Mathlib/AlgebraicGeometry/Limits.lean                     | 2 +-
 Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean     | 2 +-
 .../MeasureTheory/Function/StronglyMeasurable/Basic.lean  | 8 ++------
 3 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Limits.lean b/Mathlib/AlgebraicGeometry/Limits.lean
index 29a3e37e415e9..918b1807523fb 100644
--- a/Mathlib/AlgebraicGeometry/Limits.lean
+++ b/Mathlib/AlgebraicGeometry/Limits.lean
@@ -96,7 +96,7 @@ instance (priority := 100) isOpenImmersion_of_isEmpty {X Y : Scheme} (f : X ⟶
   · apply openEmbedding_of_continuous_injective_open
     · continuity
     · rintro (i : X.carrier); exact isEmptyElim i
-    · intro U _; convert isOpen_empty (α := Y); ext; rw [Set.mem_empty_iff_false, iff_false_iff]
+    · intro U _; convert isOpen_empty (X := Y); ext; rw [Set.mem_empty_iff_false, iff_false_iff]
       exact fun x => isEmptyElim (show X.carrier from x.choose)
   · rintro (i : X.carrier); exact isEmptyElim i
 #align algebraic_geometry.is_open_immersion_of_is_empty AlgebraicGeometry.isOpenImmersion_of_isEmpty
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
index 88c23a19a310e..c9a2a657eda95 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
@@ -390,7 +390,7 @@ theorem continuousAt_ofReal_cpow (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0)
       tauto
     have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ :=
       continuous_ofReal.continuousAt.prod_map continuousAt_id
-    exact ContinuousAt.comp (α := ℝ × ℂ) (f := fun p => ⟨↑p.1, p.2⟩) (x := ⟨0, y⟩) A B
+    exact A.comp_of_eq B rfl
   · -- x < 0 : difficult case
     suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y) by
       refine' this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) _)
diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
index 75192b66184b9..7569c2c1bfd94 100644
--- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
@@ -1658,14 +1658,10 @@ theorem _root_.Embedding.aestronglyMeasurable_comp_iff [PseudoMetrizableSpace β
   refine'
     ⟨fun H => aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨_, _⟩, fun H =>
       hg.continuous.comp_aestronglyMeasurable H⟩
-  · let G : β → range g := codRestrict g (range g) mem_range_self
+  · let G : β → range g := rangeFactorization g
     have hG : ClosedEmbedding G :=
       { hg.codRestrict _ _ with
-        closed_range := by
-          convert isClosed_univ (α := ↥(range g))
-          apply eq_univ_of_forall
-          rintro ⟨-, ⟨x, rfl⟩⟩
-          exact mem_range_self x }
+        closed_range := by rw [surjective_onto_range.range_eq]; exact isClosed_univ }
     have : AEMeasurable (G ∘ f) μ := AEMeasurable.subtype_mk H.aemeasurable
     exact hG.measurableEmbedding.aemeasurable_comp_iff.1 this
   · rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 H).2 with ⟨t, ht, h't⟩