diff --git a/Counterexamples/SorgenfreyLine.lean b/Counterexamples/SorgenfreyLine.lean
index 5b1742059d159e..8f441f057a736a 100644
--- a/Counterexamples/SorgenfreyLine.lean
+++ b/Counterexamples/SorgenfreyLine.lean
@@ -179,8 +179,8 @@ theorem isClopen_Ico (a b : ℝₗ) : IsClopen (Ico a b) :=
 
 instance : TotallyDisconnectedSpace ℝₗ :=
   ⟨fun _ _ hs x hx y hy =>
-    le_antisymm (hs.subset_clopen (isClopen_Ici x) ⟨x, hx, left_mem_Ici⟩ hy)
-      (hs.subset_clopen (isClopen_Ici y) ⟨y, hy, left_mem_Ici⟩ hx)⟩
+    le_antisymm (hs.subset_isClopen (isClopen_Ici x) ⟨x, hx, left_mem_Ici⟩ hy)
+      (hs.subset_isClopen (isClopen_Ici y) ⟨y, hy, left_mem_Ici⟩ hx)⟩
 
 instance : FirstCountableTopology ℝₗ :=
   ⟨fun x => (nhds_basis_Ico_rat x).isCountablyGenerated⟩
diff --git a/Mathlib/Analysis/Calculus/MeanValue.lean b/Mathlib/Analysis/Calculus/MeanValue.lean
index db15bf51383581..da20d7d4441d9f 100644
--- a/Mathlib/Analysis/Calculus/MeanValue.lean
+++ b/Mathlib/Analysis/Calculus/MeanValue.lean
@@ -103,7 +103,7 @@ theorem image_le_of_liminf_slope_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {
   have A : ContinuousOn (fun x => (f x, B x)) (Icc a b) := hf.prod hB
   have : IsClosed s := by
     simp only [inter_comm]
-    exact A.preimage_closed_of_closed isClosed_Icc OrderClosedTopology.isClosed_le'
+    exact A.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'
   apply this.Icc_subset_of_forall_exists_gt ha
   rintro x ⟨hxB : f x ≤ B x, xab⟩ y hy
   cases' hxB.lt_or_eq with hxB hxB
diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 81492e85b55556..b7fcd0b8b3dc8c 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -260,7 +260,7 @@ section TotallyDisconnected
   totally disconnected. -/
 theorem krullTopology_totallyDisconnected {K L : Type*} [Field K] [Field L] [Algebra K L]
     (h_int : Algebra.IsIntegral K L) : IsTotallyDisconnected (Set.univ : Set (L ≃ₐ[K] L)) := by
-  apply isTotallyDisconnected_of_clopen_set
+  apply isTotallyDisconnected_of_isClopen_set
   intro σ τ h_diff
   have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne.def, inv_mul_eq_one]
   rcases FunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩
diff --git a/Mathlib/Geometry/Manifold/BumpFunction.lean b/Mathlib/Geometry/Manifold/BumpFunction.lean
index de6cfa1df23d81..0af43aa15172ff 100644
--- a/Mathlib/Geometry/Manifold/BumpFunction.lean
+++ b/Mathlib/Geometry/Manifold/BumpFunction.lean
@@ -214,7 +214,7 @@ theorem nhdsWithin_range_basis :
 theorem isClosed_image_of_isClosed {s : Set M} (hsc : IsClosed s) (hs : s ⊆ support f) :
     IsClosed (extChartAt I c '' s) := by
   rw [f.image_eq_inter_preimage_of_subset_support hs]
-  refine' ContinuousOn.preimage_closed_of_closed
+  refine' ContinuousOn.preimage_isClosed_of_isClosed
     ((continuousOn_extChartAt_symm _ _).mono f.closedBall_subset) _ hsc
   exact IsClosed.inter isClosed_ball I.closed_range
 #align smooth_bump_function.is_closed_image_of_is_closed SmoothBumpFunction.isClosed_image_of_isClosed
diff --git a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
index 14f3deef15f7fb..7b36a4391a5b52 100644
--- a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
+++ b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
@@ -1031,7 +1031,7 @@ theorem sub_le_integral_of_hasDeriv_right_of_le_Ico (hab : a ≤ b)
       rw [← uIcc_of_le hab] at G'int hcont ⊢
       exact (hcont.sub continuousOn_const).prod (continuousOn_primitive_interval G'int)
     simp only [inter_comm]
-    exact this.preimage_closed_of_closed isClosed_Icc OrderClosedTopology.isClosed_le'
+    exact this.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'
   have main : Icc a b ⊆ {t | g t - g a ≤ ∫ u in a..t, (G' u).toReal} := by
     -- to show that the set `s` is all `[a, b]`, it suffices to show that any point `t` in `s`
     -- with `t < b` admits another point in `s` slightly to its right
@@ -1129,7 +1129,7 @@ theorem sub_le_integral_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : Continu
       rw [← uIcc_of_le hab] at hcont φint ⊢
       exact (continuousOn_const.sub hcont).prod (continuousOn_primitive_interval_left φint)
     simp only [inter_comm]
-    exact this.preimage_closed_of_closed isClosed_Icc isClosed_le_prod
+    exact this.preimage_isClosed_of_isClosed isClosed_Icc isClosed_le_prod
   have A : closure (Ioc a b) ⊆ s := by
     apply s_closed.closure_subset_iff.2
     intro t ht
diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean
index bf4a73b35c3b06..af8cebc9db5cc1 100644
--- a/Mathlib/Topology/Category/Profinite/Basic.lean
+++ b/Mathlib/Topology/Category/Profinite/Basic.lean
@@ -382,20 +382,20 @@ theorem epi_iff_surjective {X Y : Profinite.{u}} (f : X ⟶ Y) : Epi f ↔ Funct
     obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_clopen.mem_nhds_iff.mp hUy
     classical
       let Z := of (ULift.{u} <| Fin 2)
-      let g : Y ⟶ Z := ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
+      let g : Y ⟶ Z := ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
       let h : Y ⟶ Z := ⟨fun _ => ⟨1⟩, continuous_const⟩
       have H : h = g := by
         rw [← cancel_epi f]
         ext x
         apply ULift.ext
-        dsimp [LocallyConstant.ofClopen]
+        dsimp [LocallyConstant.ofIsClopen]
         -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
         erw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk,
           Function.comp_apply, if_neg]
         refine' mt (fun α => hVU α) _
         simp only [Set.mem_range_self, not_true, not_false_iff, Set.mem_compl_iff]
       apply_fun fun e => (e y).down at H
-      dsimp [LocallyConstant.ofClopen] at H
+      dsimp [LocallyConstant.ofIsClopen] at H
       -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
       erw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
       exact top_ne_bot H
diff --git a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
index 495e15fcf3a485..fb41cbcb2a4c3b 100644
--- a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
+++ b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
@@ -18,7 +18,7 @@ This file contains some theorems about cofiltered limits of profinite sets.
 
 ## Main Results
 
-- `exists_clopen_of_cofiltered` shows that any clopen set in a cofiltered limit of profinite
+- `exists_isClopen_of_cofiltered` shows that any clopen set in a cofiltered limit of profinite
   sets is the pullback of a clopen set from one of the factors in the limit.
 - `exists_locally_constant` shows that any locally constant function from a cofiltered limit
   of profinite sets factors through one of the components.
@@ -47,7 +47,7 @@ instance preserves_smaller_limits_toTopCat :
 /-- If `X` is a cofiltered limit of profinite sets, then any clopen subset of `X` arises from
 a clopen set in one of the terms in the limit.
 -/
-theorem exists_clopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClopen U) :
+theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClopen U) :
     ∃ (j : J) (V : Set (F.obj j)) (_ : IsClopen V), U = C.π.app j ⁻¹' V := by
   have := preserves_smaller_limits_toTopCat.{u, v}
   -- First, we have the topological basis of the cofiltered limit obtained by pulling back
@@ -118,20 +118,20 @@ theorem exists_clopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClop
       rw [(hV s).2]
       rwa [dif_pos hs, ← Set.preimage_comp, ← Profinite.coe_comp, ← Functor.map_comp, C.w] at hx
 set_option linter.uppercaseLean3 false in
-#align Profinite.exists_clopen_of_cofiltered Profinite.exists_clopen_of_cofiltered
+#align Profinite.exists_clopen_of_cofiltered Profinite.exists_isClopen_of_cofiltered
 
 theorem exists_locallyConstant_fin_two (hC : IsLimit C) (f : LocallyConstant C.pt (Fin 2)) :
     ∃ (j : J) (g : LocallyConstant (F.obj j) (Fin 2)), f = g.comap (C.π.app _) := by
   let U := f ⁻¹' {0}
   have hU : IsClopen U := f.isLocallyConstant.isClopen_fiber _
-  obtain ⟨j, V, hV, h⟩ := exists_clopen_of_cofiltered C hC hU
-  use j, LocallyConstant.ofClopen hV
+  obtain ⟨j, V, hV, h⟩ := exists_isClopen_of_cofiltered C hC hU
+  use j, LocallyConstant.ofIsClopen hV
   apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq
   -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
   erw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous]
   conv_rhs => rw [Set.preimage_comp]
   -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-  erw [LocallyConstant.ofClopen_fiber_zero hV, ← h]
+  erw [LocallyConstant.ofIsClopen_fiber_zero hV, ← h]
 set_option linter.uppercaseLean3 false in
 #align Profinite.exists_locally_constant_fin_two Profinite.exists_locallyConstant_fin_two
 
diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean
index a075acbf3e40c4..3c3fabb1a78a88 100644
--- a/Mathlib/Topology/Category/Profinite/Nobeling.lean
+++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean
@@ -1814,7 +1814,7 @@ theorem Nobeling.embedding : ClosedEmbedding (Nobeling.ι S) := by
       simp only [Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq]
   · intro a b h
     by_contra hn
-    obtain ⟨C, hC, hh⟩ := exists_clopen_of_totally_separated hn
+    obtain ⟨C, hC, hh⟩ := exists_isClopen_of_totally_separated hn
     apply hh.2 ∘ of_decide_eq_true
     dsimp (config := { unfoldPartialApp := true }) [ι] at h
     rw [← congr_fun h ⟨C, hC⟩]
diff --git a/Mathlib/Topology/Category/Stonean/Basic.lean b/Mathlib/Topology/Category/Stonean/Basic.lean
index 40bdb9669278de..d06ab7e3a8d7a7 100644
--- a/Mathlib/Topology/Category/Stonean/Basic.lean
+++ b/Mathlib/Topology/Category/Stonean/Basic.lean
@@ -194,7 +194,7 @@ lemma epi_iff_surjective {X Y : Stonean} (f : X ⟶ Y) :
   obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_clopen.mem_nhds_iff.mp hUy
   classical
   let g : Y ⟶ mkFinite (ULift (Fin 2)) :=
-    ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
+    ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
   let h : Y ⟶ mkFinite (ULift (Fin 2)) := ⟨fun _ => ⟨1⟩, continuous_const⟩
   have H : h = g := by
     rw [← cancel_epi f]
diff --git a/Mathlib/Topology/Clopen.lean b/Mathlib/Topology/Clopen.lean
index a0fc25ade8dd30..0e2dd4e2570dbc 100644
--- a/Mathlib/Topology/Clopen.lean
+++ b/Mathlib/Topology/Clopen.lean
@@ -110,11 +110,11 @@ theorem IsClopen.preimage {s : Set Y} (h : IsClopen s) {f : X → Y} (hf : Conti
   ⟨h.1.preimage hf, h.2.preimage hf⟩
 #align is_clopen.preimage IsClopen.preimage
 
-theorem ContinuousOn.preimage_clopen_of_clopen {f : X → Y} {s : Set X} {t : Set Y}
+theorem ContinuousOn.preimage_isClopen_of_isClopen {f : X → Y} {s : Set X} {t : Set Y}
     (hf : ContinuousOn f s) (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ f ⁻¹' t) :=
   ⟨ContinuousOn.preimage_open_of_open hf hs.1 ht.1,
-    ContinuousOn.preimage_closed_of_closed hf hs.2 ht.2⟩
-#align continuous_on.preimage_clopen_of_clopen ContinuousOn.preimage_clopen_of_clopen
+    ContinuousOn.preimage_isClosed_of_isClosed hf hs.2 ht.2⟩
+#align continuous_on.preimage_clopen_of_clopen ContinuousOn.preimage_isClopen_of_isClopen
 
 /-- The intersection of a disjoint covering by two open sets of a clopen set will be clopen. -/
 theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s) (cover : s ⊆ a ∪ b)
@@ -150,7 +150,7 @@ protected theorem QuotientMap.isClopen_preimage {f : X → Y} (hf : QuotientMap
   and_congr hf.isOpen_preimage hf.isClosed_preimage
 #align quotient_map.is_clopen_preimage QuotientMap.isClopen_preimage
 
-theorem continuous_boolIndicator_iff_clopen (U : Set X) :
+theorem continuous_boolIndicator_iff_isClopen (U : Set X) :
     Continuous U.boolIndicator ↔ IsClopen U := by
   constructor
   · intro hc
@@ -159,12 +159,12 @@ theorem continuous_boolIndicator_iff_clopen (U : Set X) :
   · refine' fun hU => ⟨fun s _ => _⟩
     rcases U.preimage_boolIndicator s with (h | h | h | h) <;> rw [h]
     exacts [isOpen_univ, hU.1, hU.2.isOpen_compl, isOpen_empty]
-#align continuous_bool_indicator_iff_clopen continuous_boolIndicator_iff_clopen
+#align continuous_bool_indicator_iff_clopen continuous_boolIndicator_iff_isClopen
 
-theorem continuousOn_boolIndicator_iff_clopen (s U : Set X) :
+theorem continuousOn_boolIndicator_iff_isClopen (s U : Set X) :
     ContinuousOn U.boolIndicator s ↔ IsClopen (((↑) : s → X) ⁻¹' U) := by
-  rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_clopen]
+  rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_isClopen]
   rfl
-#align continuous_on_indicator_iff_clopen continuousOn_boolIndicator_iff_clopen
+#align continuous_on_indicator_iff_clopen continuousOn_boolIndicator_iff_isClopen
 
 end Clopen
diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean
index 21a19c11f40ba5..cd287cca63acea 100644
--- a/Mathlib/Topology/Connected/Basic.lean
+++ b/Mathlib/Topology/Connected/Basic.lean
@@ -438,10 +438,10 @@ theorem IsPreconnected.subset_right_of_subset_union (hu : IsOpen u) (hv : IsOpen
 
 -- porting note: moved up
 /-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
-theorem IsPreconnected.subset_clopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t)
+theorem IsPreconnected.subset_isClopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t)
     (hne : (s ∩ t).Nonempty) : s ⊆ t :=
   hs.subset_left_of_subset_union ht.isOpen ht.compl.isOpen disjoint_compl_right (by simp) hne
-#align is_preconnected.subset_clopen IsPreconnected.subset_clopen
+#align is_preconnected.subset_clopen IsPreconnected.subset_isClopen
 
 /-- If a preconnected set `s` intersects an open set `u`, and limit points of `u` inside `s` are
 contained in `u`, then the whole set `s` is contained in `u`. -/
@@ -511,7 +511,7 @@ theorem Sigma.isConnected_iff [∀ i, TopologicalSpace (π i)] {s : Set (Σi, π
   refine' ⟨fun hs => _, _⟩
   · obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty
     have : s ⊆ range (Sigma.mk i) :=
-      hs.isPreconnected.subset_clopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩
+      hs.isPreconnected.subset_isClopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩
     exact ⟨i, Sigma.mk i ⁻¹' s, hs.preimage_of_openMap sigma_mk_injective isOpenMap_sigmaMk this,
       (Set.image_preimage_eq_of_subset this).symm⟩
   · rintro ⟨i, t, ht, rfl⟩
@@ -535,12 +535,12 @@ theorem Sum.isConnected_iff [TopologicalSpace β] {s : Set (Sum α β)} :
   refine' ⟨fun hs => _, _⟩
   · obtain ⟨x | x, hx⟩ := hs.nonempty
     · have h : s ⊆ range Sum.inl :=
-        hs.isPreconnected.subset_clopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
+        hs.isPreconnected.subset_isClopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
       refine' Or.inl ⟨Sum.inl ⁻¹' s, _, _⟩
       · exact hs.preimage_of_openMap Sum.inl_injective isOpenMap_inl h
       · exact (image_preimage_eq_of_subset h).symm
     · have h : s ⊆ range Sum.inr :=
-        hs.isPreconnected.subset_clopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
+        hs.isPreconnected.subset_isClopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
       refine' Or.inr ⟨Sum.inr ⁻¹' s, _, _⟩
       · exact hs.preimage_of_openMap Sum.inr_injective isOpenMap_inr h
       · exact (image_preimage_eq_of_subset h).symm
@@ -1058,13 +1058,13 @@ theorem isConnected_iff_sUnion_disjoint_open {s : Set α} :
     simpa [*, or_imp, forall_and] using h {u, v}
 #align is_connected_iff_sUnion_disjoint_open isConnected_iff_sUnion_disjoint_open
 
--- porting note: `IsPreconnected.subset_clopen` moved up from here
+-- porting note: `IsPreconnected.subset_isClopen` moved up from here
 
 /-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
-theorem disjoint_or_subset_of_clopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) :
+theorem disjoint_or_subset_of_isClopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) :
     Disjoint s t ∨ s ⊆ t :=
-  (disjoint_or_nonempty_inter s t).imp_right <| hs.subset_clopen ht
-#align disjoint_or_subset_of_clopen disjoint_or_subset_of_clopen
+  (disjoint_or_nonempty_inter s t).imp_right <| hs.subset_isClopen ht
+#align disjoint_or_subset_of_clopen disjoint_or_subset_of_isClopen
 
 /-- A set `s` is preconnected if and only if
 for every cover by two closed sets that are disjoint on `s`,
@@ -1115,15 +1115,15 @@ theorem isPreconnected_iff_subset_of_fully_disjoint_closed {s : Set α} (hs : Is
 
 theorem IsClopen.connectedComponent_subset {x} (hs : IsClopen s) (hx : x ∈ s) :
     connectedComponent x ⊆ s :=
-  isPreconnected_connectedComponent.subset_clopen hs ⟨x, mem_connectedComponent, hx⟩
+  isPreconnected_connectedComponent.subset_isClopen hs ⟨x, mem_connectedComponent, hx⟩
 #align is_clopen.connected_component_subset IsClopen.connectedComponent_subset
 
 /-- The connected component of a point is always a subset of the intersection of all its clopen
 neighbourhoods. -/
-theorem connectedComponent_subset_iInter_clopen {x : α} :
+theorem connectedComponent_subset_iInter_isClopen {x : α} :
     connectedComponent x ⊆ ⋂ Z : { Z : Set α // IsClopen Z ∧ x ∈ Z }, Z :=
   subset_iInter fun Z => Z.2.1.connectedComponent_subset Z.2.2
-#align connected_component_subset_Inter_clopen connectedComponent_subset_iInter_clopen
+#align connected_component_subset_Inter_clopen connectedComponent_subset_iInter_isClopen
 
 /-- A clopen set is the union of its connected components. -/
 theorem IsClopen.biUnion_connectedComponent_eq {Z : Set α} (h : IsClopen Z) :
@@ -1315,7 +1315,7 @@ theorem isPreconnected_of_forall_constant {s : Set α}
   rcases this with ⟨u, v, u_op, v_op, hsuv, ⟨x, x_in_s, x_in_u⟩, ⟨y, y_in_s, y_in_v⟩, H⟩
   have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_not_mem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩
   have : ContinuousOn u.boolIndicator s := by
-    apply (continuousOn_boolIndicator_iff_clopen _ _).mpr ⟨_, _⟩
+    apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩
     · exact u_op.preimage continuous_subtype_val
     · rw [preimage_subtype_coe_eq_compl hsuv H]
       exact (v_op.preimage continuous_subtype_val).isClosed_compl
diff --git a/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Mathlib/Topology/Connected/TotallyDisconnected.lean
index cfa0b6a03b7804..252995bd769b35 100644
--- a/Mathlib/Topology/Connected/TotallyDisconnected.lean
+++ b/Mathlib/Topology/Connected/TotallyDisconnected.lean
@@ -90,19 +90,19 @@ instance [∀ i, TopologicalSpace (π i)] [∀ i, TotallyDisconnectedSpace (π i
 -- porting note: reformulated using `Pairwise`
 /-- Let `X` be a topological space, and suppose that for all distinct `x,y ∈ X`, there
   is some clopen set `U` such that `x ∈ U` and `y ∉ U`. Then `X` is totally disconnected. -/
-theorem isTotallyDisconnected_of_clopen_set {X : Type*} [TopologicalSpace X]
+theorem isTotallyDisconnected_of_isClopen_set {X : Type*} [TopologicalSpace X]
     (hX : Pairwise fun x y => ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∉ U) :
     IsTotallyDisconnected (Set.univ : Set X) := by
   rintro S - hS
   unfold Set.Subsingleton
   by_contra' h_contra
   rcases h_contra with ⟨x, hx, y, hy, hxy⟩
-  obtain ⟨U, h_clopen, hxU, hyU⟩ := hX hxy
+  obtain ⟨U, hU, hxU, hyU⟩ := hX hxy
   specialize
-    hS U Uᶜ h_clopen.1 h_clopen.compl.1 (fun a _ => em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩
+    hS U Uᶜ hU.1 hU.compl.1 (fun a _ => em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩
   rw [inter_compl_self, Set.inter_empty] at hS
   exact Set.not_nonempty_empty hS
-#align is_totally_disconnected_of_clopen_set isTotallyDisconnected_of_clopen_set
+#align is_totally_disconnected_of_clopen_set isTotallyDisconnected_of_isClopen_set
 
 /-- A space is totally disconnected iff its connected components are subsingletons. -/
 theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton :
@@ -235,16 +235,16 @@ instance (priority := 100) TotallySeparatedSpace.of_discrete (α : Type*) [Topol
     (compl_union_self _).symm.subset, disjoint_compl_left⟩⟩
 #align totally_separated_space.of_discrete TotallySeparatedSpace.of_discrete
 
-theorem exists_clopen_of_totally_separated {α : Type*} [TopologicalSpace α]
+theorem exists_isClopen_of_totally_separated {α : Type*} [TopologicalSpace α]
     [TotallySeparatedSpace α] {x y : α} (hxy : x ≠ y) :
     ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ := by
   obtain ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ :=
     TotallySeparatedSpace.isTotallySeparated_univ x (Set.mem_univ x) y (Set.mem_univ y) hxy
-  have clopen_U := isClopen_inter_of_disjoint_cover_clopen isClopen_univ f hU hV disj
-  rw [univ_inter _] at clopen_U
+  have hU := isClopen_inter_of_disjoint_cover_clopen isClopen_univ f hU hV disj
+  rw [univ_inter _] at hU
   rw [← Set.subset_compl_iff_disjoint_right, subset_compl_comm] at disj
-  exact ⟨U, clopen_U, Ux, disj Vy⟩
-#align exists_clopen_of_totally_separated exists_clopen_of_totally_separated
+  exact ⟨U, hU, Ux, disj Vy⟩
+#align exists_clopen_of_totally_separated exists_isClopen_of_totally_separated
 
 end TotallySeparated
 
diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean
index 7fafcdfcf30caa..b576ff2a120ac3 100644
--- a/Mathlib/Topology/ContinuousOn.lean
+++ b/Mathlib/Topology/ContinuousOn.lean
@@ -1075,12 +1075,12 @@ theorem ContinuousOn.isOpen_preimage {f : α → β} {s : Set α} {t : Set β} (
   rw [inter_comm, inter_eq_self_of_subset_left hp]
 #align continuous_on.is_open_preimage ContinuousOn.isOpen_preimage
 
-theorem ContinuousOn.preimage_closed_of_closed {f : α → β} {s : Set α} {t : Set β}
+theorem ContinuousOn.preimage_isClosed_of_isClosed {f : α → β} {s : Set α} {t : Set β}
     (hf : ContinuousOn f s) (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ∩ f ⁻¹' t) := by
   rcases continuousOn_iff_isClosed.1 hf t ht with ⟨u, hu⟩
   rw [inter_comm, hu.2]
   apply IsClosed.inter hu.1 hs
-#align continuous_on.preimage_closed_of_closed ContinuousOn.preimage_closed_of_closed
+#align continuous_on.preimage_closed_of_closed ContinuousOn.preimage_isClosed_of_isClosed
 
 theorem ContinuousOn.preimage_interior_subset_interior_preimage {f : α → β} {s : Set α} {t : Set β}
     (hf : ContinuousOn f s) (hs : IsOpen s) : s ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t) :=
diff --git a/Mathlib/Topology/DiscreteQuotient.lean b/Mathlib/Topology/DiscreteQuotient.lean
index 9b3834deb56ffc..15faff9e5518c4 100644
--- a/Mathlib/Topology/DiscreteQuotient.lean
+++ b/Mathlib/Topology/DiscreteQuotient.lean
@@ -82,10 +82,10 @@ lemma toSetoid_injective : Function.Injective (@toSetoid X _)
   | ⟨_, _⟩, ⟨_, _⟩, _ => by congr
 
 /-- Construct a discrete quotient from a clopen set. -/
-def ofClopen {A : Set X} (h : IsClopen A) : DiscreteQuotient X where
+def ofIsClopen {A : Set X} (h : IsClopen A) : DiscreteQuotient X where
   toSetoid := ⟨fun x y => x ∈ A ↔ y ∈ A, fun _ => Iff.rfl, Iff.symm, Iff.trans⟩
   isOpen_setOf_rel x := by by_cases hx : x ∈ A <;> simp [Setoid.Rel, hx, h.1, h.2, ← compl_setOf]
-#align discrete_quotient.of_clopen DiscreteQuotient.ofClopen
+#align discrete_quotient.of_clopen DiscreteQuotient.ofIsClopen
 
 theorem refl : ∀ x, S.Rel x x := S.refl'
 #align discrete_quotient.refl DiscreteQuotient.refl
@@ -362,10 +362,10 @@ end Map
 
 theorem eq_of_forall_proj_eq [T2Space X] [CompactSpace X] [disc : TotallyDisconnectedSpace X]
     {x y : X} (h : ∀ Q : DiscreteQuotient X, Q.proj x = Q.proj y) : x = y := by
-  rw [← mem_singleton_iff, ← connectedComponent_eq_singleton, connectedComponent_eq_iInter_clopen,
+  rw [← mem_singleton_iff, ← connectedComponent_eq_singleton, connectedComponent_eq_iInter_isClopen,
     mem_iInter]
   rintro ⟨U, hU1, hU2⟩
-  exact (Quotient.exact' (h (ofClopen hU1))).mpr hU2
+  exact (Quotient.exact' (h (ofIsClopen hU1))).mpr hU2
 #align discrete_quotient.eq_of_forall_proj_eq DiscreteQuotient.eq_of_forall_proj_eq
 
 theorem fiber_subset_ofLE {A B : DiscreteQuotient X} (h : A ≤ B) (a : A) :
diff --git a/Mathlib/Topology/LocallyConstant/Basic.lean b/Mathlib/Topology/LocallyConstant/Basic.lean
index 9fcb4d461887f5..bac88a372cc4c5 100644
--- a/Mathlib/Topology/LocallyConstant/Basic.lean
+++ b/Mathlib/Topology/LocallyConstant/Basic.lean
@@ -334,7 +334,7 @@ theorem coe_const (y : Y) : (const X y : X → Y) = Function.const X y :=
 #align locally_constant.coe_const LocallyConstant.coe_const
 
 /-- The locally constant function to `Fin 2` associated to a clopen set. -/
-def ofClopen {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x ∈ U)]
+def ofIsClopen {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x ∈ U)]
     (hU : IsClopen U) : LocallyConstant X (Fin 2) where
   toFun x := if x ∈ U then 0 else 1
   isLocallyConstant := by
@@ -348,24 +348,24 @@ def ofClopen {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x 
       convert hU.2
       ext
       simp
-#align locally_constant.of_clopen LocallyConstant.ofClopen
+#align locally_constant.of_clopen LocallyConstant.ofIsClopen
 
 @[simp]
-theorem ofClopen_fiber_zero {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x ∈ U)]
-    (hU : IsClopen U) : ofClopen hU ⁻¹' ({0} : Set (Fin 2)) = U := by
+theorem ofIsClopen_fiber_zero {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x ∈ U)]
+    (hU : IsClopen U) : ofIsClopen hU ⁻¹' ({0} : Set (Fin 2)) = U := by
   ext
-  simp only [ofClopen, mem_singleton_iff, Fin.one_eq_zero_iff, coe_mk, mem_preimage,
+  simp only [ofIsClopen, mem_singleton_iff, Fin.one_eq_zero_iff, coe_mk, mem_preimage,
     ite_eq_left_iff, Nat.succ_succ_ne_one]
   tauto
-#align locally_constant.of_clopen_fiber_zero LocallyConstant.ofClopen_fiber_zero
+#align locally_constant.of_clopen_fiber_zero LocallyConstant.ofIsClopen_fiber_zero
 
 @[simp]
-theorem ofClopen_fiber_one {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x ∈ U)]
-    (hU : IsClopen U) : ofClopen hU ⁻¹' ({1} : Set (Fin 2)) = Uᶜ := by
+theorem ofIsClopen_fiber_one {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x ∈ U)]
+    (hU : IsClopen U) : ofIsClopen hU ⁻¹' ({1} : Set (Fin 2)) = Uᶜ := by
   ext
-  simp only [ofClopen, mem_singleton_iff, coe_mk, Fin.zero_eq_one_iff, mem_preimage,
+  simp only [ofIsClopen, mem_singleton_iff, coe_mk, Fin.zero_eq_one_iff, mem_preimage,
     ite_eq_right_iff, mem_compl_iff, Nat.succ_succ_ne_one]
-#align locally_constant.of_clopen_fiber_one LocallyConstant.ofClopen_fiber_one
+#align locally_constant.of_clopen_fiber_one LocallyConstant.ofIsClopen_fiber_one
 
 theorem locallyConstant_eq_of_fiber_zero_eq {X : Type*} [TopologicalSpace X]
     (f g : LocallyConstant X (Fin 2)) (h : f ⁻¹' ({0} : Set (Fin 2)) = g ⁻¹' {0}) : f = g := by
diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean
index d7fc5c6ea2fcd2..4df33c7c2e5f36 100644
--- a/Mathlib/Topology/Order/Basic.lean
+++ b/Mathlib/Topology/Order/Basic.lean
@@ -256,7 +256,7 @@ theorem ContinuousWithinAt.closure_le [TopologicalSpace β] {f g : β → α} {s
 then the set `{x ∈ s | f x ≤ g x}` is a closed set. -/
 theorem IsClosed.isClosed_le [TopologicalSpace β] {f g : β → α} {s : Set β} (hs : IsClosed s)
     (hf : ContinuousOn f s) (hg : ContinuousOn g s) : IsClosed ({ x ∈ s | f x ≤ g x }) :=
-  (hf.prod hg).preimage_closed_of_closed hs OrderClosedTopology.isClosed_le'
+  (hf.prod hg).preimage_isClosed_of_isClosed hs OrderClosedTopology.isClosed_le'
 #align is_closed.is_closed_le IsClosed.isClosed_le
 
 theorem le_on_closure [TopologicalSpace β] {f g : β → α} {s : Set β} (h : ∀ x ∈ s, f x ≤ g x)
diff --git a/Mathlib/Topology/Order/Priestley.lean b/Mathlib/Topology/Order/Priestley.lean
index b99d53a4cb4d04..c637b6f3c456b1 100644
--- a/Mathlib/Topology/Order/Priestley.lean
+++ b/Mathlib/Topology/Order/Priestley.lean
@@ -47,16 +47,16 @@ section Preorder
 
 variable [Preorder α] [PriestleySpace α] {x y : α}
 
-theorem exists_clopen_upper_of_not_le :
+theorem exists_isClopen_upper_of_not_le :
     ¬x ≤ y → ∃ U : Set α, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U :=
   PriestleySpace.priestley
-#align exists_clopen_upper_of_not_le exists_clopen_upper_of_not_le
+#align exists_clopen_upper_of_not_le exists_isClopen_upper_of_not_le
 
-theorem exists_clopen_lower_of_not_le (h : ¬x ≤ y) :
+theorem exists_isClopen_lower_of_not_le (h : ¬x ≤ y) :
     ∃ U : Set α, IsClopen U ∧ IsLowerSet U ∧ x ∉ U ∧ y ∈ U :=
-  let ⟨U, hU, hU', hx, hy⟩ := exists_clopen_upper_of_not_le h
+  let ⟨U, hU, hU', hx, hy⟩ := exists_isClopen_upper_of_not_le h
   ⟨Uᶜ, hU.compl, hU'.compl, Classical.not_not.2 hx, hy⟩
-#align exists_clopen_lower_of_not_le exists_clopen_lower_of_not_le
+#align exists_clopen_lower_of_not_le exists_isClopen_lower_of_not_le
 
 end Preorder
 
@@ -64,18 +64,18 @@ section PartialOrder
 
 variable [PartialOrder α] [PriestleySpace α] {x y : α}
 
-theorem exists_clopen_upper_or_lower_of_ne (h : x ≠ y) :
+theorem exists_isClopen_upper_or_lower_of_ne (h : x ≠ y) :
     ∃ U : Set α, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U := by
   obtain h | h := h.not_le_or_not_le
-  · exact (exists_clopen_upper_of_not_le h).imp fun _ ↦ And.imp_right <| And.imp_left Or.inl
-  · obtain ⟨U, hU, hU', hy, hx⟩ := exists_clopen_lower_of_not_le h
+  · exact (exists_isClopen_upper_of_not_le h).imp fun _ ↦ And.imp_right <| And.imp_left Or.inl
+  · obtain ⟨U, hU, hU', hy, hx⟩ := exists_isClopen_lower_of_not_le h
     exact ⟨U, hU, Or.inr hU', hx, hy⟩
-#align exists_clopen_upper_or_lower_of_ne exists_clopen_upper_or_lower_of_ne
+#align exists_clopen_upper_or_lower_of_ne exists_isClopen_upper_or_lower_of_ne
 
 -- See note [lower instance priority]
 instance (priority := 100) PriestleySpace.toT2Space : T2Space α :=
   ⟨fun _ _ h ↦
-    let ⟨U, hU, _, hx, hy⟩ := exists_clopen_upper_or_lower_of_ne h
+    let ⟨U, hU, _, hx, hy⟩ := exists_isClopen_upper_or_lower_of_ne h
     ⟨U, Uᶜ, hU.isOpen, hU.compl.isOpen, hx, hy, disjoint_compl_right⟩⟩
 #align priestley_space.to_t2_space PriestleySpace.toT2Space
 
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index 3a66aaea273888..ac6839a632d61e 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -75,7 +75,7 @@ This file defines the predicate `SeparatedNhds`, and common separation axioms
 If the space is also compact:
 
 * `normalOfCompactT2`: A compact T₂ space is a `NormalSpace`.
-* `connectedComponent_eq_iInter_clopen`: The connected component of a point
+* `connectedComponent_eq_iInter_isClopen`: The connected component of a point
   is the intersection of all its clopen neighbourhoods.
 * `compact_t2_tot_disc_iff_tot_sep`: Being a `TotallyDisconnectedSpace`
   is equivalent to being a `TotallySeparatedSpace`.
@@ -2045,9 +2045,9 @@ end CompletelyNormal
 
 /-- In a compact T₂ space, the connected component of a point equals the intersection of all
 its clopen neighbourhoods. -/
-theorem connectedComponent_eq_iInter_clopen [T2Space X] [CompactSpace X] (x : X) :
+theorem connectedComponent_eq_iInter_isClopen [T2Space X] [CompactSpace X] (x : X) :
     connectedComponent x = ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s := by
-  apply Subset.antisymm connectedComponent_subset_iInter_clopen
+  apply Subset.antisymm connectedComponent_subset_iInter_isClopen
   -- Reduce to showing that the clopen intersection is connected.
   refine' IsPreconnected.subset_connectedComponent _ (mem_iInter.2 fun s => s.2.2)
   -- We do this by showing that any disjoint cover by two closed sets implies
@@ -2097,7 +2097,7 @@ theorem connectedComponent_eq_iInter_clopen [T2Space X] [CompactSpace X] (x : X)
       · refine Subset.trans ?_ (inter_subset_right s v)
         exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
           ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩
-#align connected_component_eq_Inter_clopen connectedComponent_eq_iInter_clopen
+#align connected_component_eq_Inter_clopen connectedComponent_eq_iInter_isClopen
 
 section Profinite
 
@@ -2121,7 +2121,7 @@ theorem compact_t2_tot_disc_iff_tot_sep : TotallyDisconnectedSpace X ↔ Totally
   intro hyp
   suffices x ∈ connectedComponent y by
     simpa [totallyDisconnectedSpace_iff_connectedComponent_singleton.1 h y, mem_singleton_iff]
-  rw [connectedComponent_eq_iInter_clopen, mem_iInter]
+  rw [connectedComponent_eq_iInter_isClopen, mem_iInter]
   rintro ⟨w : Set X, hw : IsClopen w, hy : y ∈ w⟩
   by_contra hx
   exact hyp wᶜ w hw.2.isOpen_compl hw.1 hx hy (@isCompl_compl _ w _).symm.codisjoint.top_le
@@ -2138,7 +2138,7 @@ theorem nhds_basis_clopen (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∈ s
     constructor
     · have hx : connectedComponent x = {x} :=
         totallyDisconnectedSpace_iff_connectedComponent_singleton.mp ‹_› x
-      rw [connectedComponent_eq_iInter_clopen] at hx
+      rw [connectedComponent_eq_iInter_isClopen] at hx
       intro hU
       let N := { s // IsClopen s ∧ x ∈ s }
       suffices : ∃ s : N, s.val ⊆ U
@@ -2231,7 +2231,7 @@ instance ConnectedComponents.t2 [T2Space X] [CompactSpace X] : T2Space (Connecte
   rw [ConnectedComponents.coe_ne_coe] at ne
   have h := connectedComponent_disjoint ne
   -- write ↑b as the intersection of all clopen subsets containing it
-  rw [connectedComponent_eq_iInter_clopen b, disjoint_iff_inter_eq_empty] at h
+  rw [connectedComponent_eq_iInter_isClopen b, disjoint_iff_inter_eq_empty] at h
   -- Now we show that this can be reduced to some clopen containing `↑b` being disjoint to `↑a`
   obtain ⟨U, V, hU, ha, hb, rfl⟩ : ∃ (U : Set X) (V : Set (ConnectedComponents X)),
       IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ (↑) ⁻¹' V = U := by
diff --git a/Mathlib/Topology/Sets/Closeds.lean b/Mathlib/Topology/Sets/Closeds.lean
index 7c8b0af4ec1627..df686d420867fa 100644
--- a/Mathlib/Topology/Sets/Closeds.lean
+++ b/Mathlib/Topology/Sets/Closeds.lean
@@ -275,7 +275,7 @@ theorem Opens.isCoatom_iff [T1Space α] {s : Opens α} :
 /-- The type of clopen sets of a topological space. -/
 structure Clopens (α : Type*) [TopologicalSpace α] where
   carrier : Set α
-  clopen' : IsClopen carrier
+  isClopen' : IsClopen carrier
 #align topological_space.clopens TopologicalSpace.Clopens
 
 namespace Clopens
@@ -284,9 +284,9 @@ instance : SetLike (Clopens α) α where
   coe s := s.carrier
   coe_injective' s t h := by cases s; cases t; congr
 
-theorem clopen (s : Clopens α) : IsClopen (s : Set α) :=
-  s.clopen'
-#align topological_space.clopens.clopen TopologicalSpace.Clopens.clopen
+theorem isClopen (s : Clopens α) : IsClopen (s : Set α) :=
+  s.isClopen'
+#align topological_space.clopens.clopen TopologicalSpace.Clopens.isClopen
 
 /-- See Note [custom simps projection]. -/
 def Simps.coe (s : Clopens α) : Set α := s
@@ -296,7 +296,7 @@ initialize_simps_projections Clopens (carrier → coe)
 /-- Reinterpret a clopen as an open. -/
 @[simps]
 def toOpens (s : Clopens α) : Opens α :=
-  ⟨s, s.clopen.isOpen⟩
+  ⟨s, s.isClopen.isOpen⟩
 #align topological_space.clopens.to_opens TopologicalSpace.Clopens.toOpens
 
 @[ext]
@@ -309,12 +309,12 @@ theorem coe_mk (s : Set α) (h) : (mk s h : Set α) = s :=
   rfl
 #align topological_space.clopens.coe_mk TopologicalSpace.Clopens.coe_mk
 
-instance : Sup (Clopens α) := ⟨fun s t => ⟨s ∪ t, s.clopen.union t.clopen⟩⟩
-instance : Inf (Clopens α) := ⟨fun s t => ⟨s ∩ t, s.clopen.inter t.clopen⟩⟩
+instance : Sup (Clopens α) := ⟨fun s t => ⟨s ∪ t, s.isClopen.union t.isClopen⟩⟩
+instance : Inf (Clopens α) := ⟨fun s t => ⟨s ∩ t, s.isClopen.inter t.isClopen⟩⟩
 instance : Top (Clopens α) := ⟨⟨⊤, isClopen_univ⟩⟩
 instance : Bot (Clopens α) := ⟨⟨⊥, isClopen_empty⟩⟩
-instance : SDiff (Clopens α) := ⟨fun s t => ⟨s \ t, s.clopen.diff t.clopen⟩⟩
-instance : HasCompl (Clopens α) := ⟨fun s => ⟨sᶜ, s.clopen.compl⟩⟩
+instance : SDiff (Clopens α) := ⟨fun s t => ⟨s \ t, s.isClopen.diff t.isClopen⟩⟩
+instance : HasCompl (Clopens α) := ⟨fun s => ⟨sᶜ, s.isClopen.compl⟩⟩
 
 instance : BooleanAlgebra (Clopens α) :=
   SetLike.coe_injective.booleanAlgebra _ (fun _ _ => rfl) (fun _ _ => rfl) rfl rfl (fun _ => rfl)
diff --git a/Mathlib/Topology/Sets/Order.lean b/Mathlib/Topology/Sets/Order.lean
index 80335006ee12ce..cfb557047b3330 100644
--- a/Mathlib/Topology/Sets/Order.lean
+++ b/Mathlib/Topology/Sets/Order.lean
@@ -45,9 +45,9 @@ theorem upper (s : ClopenUpperSet α) : IsUpperSet (s : Set α) :=
   s.upper'
 #align clopen_upper_set.upper ClopenUpperSet.upper
 
-theorem clopen (s : ClopenUpperSet α) : IsClopen (s : Set α) :=
-  s.clopen'
-#align clopen_upper_set.clopen ClopenUpperSet.clopen
+theorem isClopen (s : ClopenUpperSet α) : IsClopen (s : Set α) :=
+  s.isClopen'
+#align clopen_upper_set.clopen ClopenUpperSet.isClopen
 
 /-- Reinterpret an upper clopen as an upper set. -/
 @[simps]
diff --git a/Mathlib/Topology/StoneCech.lean b/Mathlib/Topology/StoneCech.lean
index 9392c6eed2f5be..02bef1354b2c40 100644
--- a/Mathlib/Topology/StoneCech.lean
+++ b/Mathlib/Topology/StoneCech.lean
@@ -96,7 +96,7 @@ instance : TotallyDisconnectedSpace (Ultrafilter α) := by
   intro B hB
   rw [← Ultrafilter.coe_le_coe]
   intro s hs
-  rw [connectedComponent_eq_iInter_clopen, Set.mem_iInter] at hB
+  rw [connectedComponent_eq_iInter_isClopen, Set.mem_iInter] at hB
   let Z := { F : Ultrafilter α | s ∈ F }
   have hZ : IsClopen Z := ⟨ultrafilter_isOpen_basic s, ultrafilter_isClosed_basic s⟩
   exact hB ⟨Z, hZ, hs⟩
diff --git a/scripts/nolints.json b/scripts/nolints.json
index 35ea86ba099313..e5357638ae9db6 100644
--- a/scripts/nolints.json
+++ b/scripts/nolints.json
@@ -1903,7 +1903,7 @@
  ["docBlame", "ToAdditive.additiveTestUnsafe.visit"],
  ["docBlame", "TopCat.GlueData.f_open"],
  ["docBlame", "TopologicalSpace.Clopens.carrier"],
- ["docBlame", "TopologicalSpace.Clopens.clopen'"],
+ ["docBlame", "TopologicalSpace.Clopens.isClopen'"],
  ["docBlame", "TopologicalSpace.Closeds.carrier"],
  ["docBlame", "TopologicalSpace.Closeds.closed'"],
  ["docBlame", "TopologicalSpace.CompactOpens.isOpen'"],