diff --git a/Mathlib/Analysis/InnerProductSpace/OfNorm.lean b/Mathlib/Analysis/InnerProductSpace/OfNorm.lean
index 2616c07526d0b..48732656917c7 100644
--- a/Mathlib/Analysis/InnerProductSpace/OfNorm.lean
+++ b/Mathlib/Analysis/InnerProductSpace/OfNorm.lean
@@ -269,7 +269,7 @@ private theorem real_prop (r : ℝ) : innerProp' E (r : 𝕜) := by
   intro x y
   revert r
   rw [← Function.funext_iff]
-  refine Rat.denseEmbedding_coe_real.dense.equalizer ?_ ?_ (funext fun X => ?_)
+  refine Rat.isDenseEmbedding_coe_real.dense.equalizer ?_ ?_ (funext fun X => ?_)
   · exact (continuous_ofReal.smul continuous_const).inner_ continuous_const
   · exact (continuous_conj.comp continuous_ofReal).mul continuous_const
   · simp only [Function.comp_apply, RCLike.ofReal_ratCast, rat_prop _ _]
diff --git a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
index d2aa0a504c720..29f9a7d7b2d9b 100644
--- a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
+++ b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
@@ -23,7 +23,7 @@ by a sequence of simple functions.
   measurable and `Memℒp` (for `p < ∞`), then the simple functions
   `SimpleFunc.approxOn f hf s 0 h₀ n` may be considered as elements of `Lp E p μ`, and they tend
   in Lᵖ to `f`.
-* `Lp.simpleFunc.denseEmbedding`: the embedding `coeToLp` of the `Lp` simple functions into
+* `Lp.simpleFunc.isDenseEmbedding`: the embedding `coeToLp` of the `Lp` simple functions into
   `Lp` is dense.
 * `Lp.simpleFunc.induction`, `Lp.induction`, `Memℒp.induction`, `Integrable.induction`: to prove
   a predicate for all elements of one of these classes of functions, it suffices to check that it
@@ -685,10 +685,10 @@ protected theorem uniformEmbedding : UniformEmbedding ((↑) : Lp.simpleFunc E p
 protected theorem uniformInducing : UniformInducing ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
   simpleFunc.uniformEmbedding.toUniformInducing
 
-protected theorem denseEmbedding (hp_ne_top : p ≠ ∞) :
-    DenseEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) := by
+lemma isDenseEmbedding (hp_ne_top : p ≠ ∞) :
+    IsDenseEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) := by
   borelize E
-  apply simpleFunc.uniformEmbedding.denseEmbedding
+  apply simpleFunc.uniformEmbedding.isDenseEmbedding
   intro f
   rw [mem_closure_iff_seq_limit]
   have hfi' : Memℒp f p μ := Lp.memℒp f
@@ -703,9 +703,12 @@ protected theorem denseEmbedding (hp_ne_top : p ≠ ∞) :
   convert SimpleFunc.tendsto_approxOn_range_Lp hp_ne_top (Lp.stronglyMeasurable f).measurable hfi'
   rw [toLp_coeFn f (Lp.memℒp f)]
 
+@[deprecated (since := "2024-09-30")]
+alias denseEmbedding := isDenseEmbedding
+
 protected theorem isDenseInducing (hp_ne_top : p ≠ ∞) :
     IsDenseInducing ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
-  (simpleFunc.denseEmbedding hp_ne_top).toIsDenseInducing
+  (simpleFunc.isDenseEmbedding hp_ne_top).toIsDenseInducing
 
 protected theorem denseRange (hp_ne_top : p ≠ ∞) :
     DenseRange ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
diff --git a/Mathlib/NumberTheory/Liouville/Residual.lean b/Mathlib/NumberTheory/Liouville/Residual.lean
index 4d72a848d850a..38feb5335e927 100644
--- a/Mathlib/NumberTheory/Liouville/Residual.lean
+++ b/Mathlib/NumberTheory/Liouville/Residual.lean
@@ -53,7 +53,7 @@ theorem setOf_liouville_eq_irrational_inter_iInter_iUnion :
 theorem eventually_residual_liouville : ∀ᶠ x in residual ℝ, Liouville x := by
   rw [Filter.Eventually, setOf_liouville_eq_irrational_inter_iInter_iUnion]
   refine eventually_residual_irrational.and ?_
-  refine residual_of_dense_Gδ ?_ (Rat.denseEmbedding_coe_real.dense.mono ?_)
+  refine residual_of_dense_Gδ ?_ (Rat.isDenseEmbedding_coe_real.dense.mono ?_)
   · exact .iInter fun n => IsOpen.isGδ <|
           isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => isOpen_ball
   · rintro _ ⟨r, rfl⟩
diff --git a/Mathlib/Topology/Algebra/UniformField.lean b/Mathlib/Topology/Algebra/UniformField.lean
index 59733a4968e23..27cc2841c5eb2 100644
--- a/Mathlib/Topology/Algebra/UniformField.lean
+++ b/Mathlib/Topology/Algebra/UniformField.lean
@@ -111,7 +111,7 @@ theorem coe_inv (x : K) : (x : hat K)⁻¹ = ((x⁻¹ : K) : hat K) := by
   · conv_lhs => dsimp [Inv.inv]
     rw [if_neg]
     · exact hatInv_extends h
-    · exact fun H => h (denseEmbedding_coe.inj H)
+    · exact fun H => h (isDenseEmbedding_coe.inj H)
 
 variable [UniformAddGroup K]
 
diff --git a/Mathlib/Topology/Compactification/OnePoint.lean b/Mathlib/Topology/Compactification/OnePoint.lean
index cb7d3c40f534c..ffe89b1a9a2a8 100644
--- a/Mathlib/Topology/Compactification/OnePoint.lean
+++ b/Mathlib/Topology/Compactification/OnePoint.lean
@@ -426,9 +426,12 @@ theorem denseRange_coe [NoncompactSpace X] : DenseRange ((↑) : X → OnePoint
   rw [DenseRange, ← compl_infty]
   exact dense_compl_singleton _
 
-theorem denseEmbedding_coe [NoncompactSpace X] : DenseEmbedding ((↑) : X → OnePoint X) :=
+theorem isDenseEmbedding_coe [NoncompactSpace X] : IsDenseEmbedding ((↑) : X → OnePoint X) :=
   { openEmbedding_coe with dense := denseRange_coe }
 
+@[deprecated (since := "2024-09-30")]
+alias denseEmbedding_coe := isDenseEmbedding_coe
+
 @[simp, norm_cast]
 theorem specializes_coe {x y : X} : (x : OnePoint X) ⤳ y ↔ x ⤳ y :=
   openEmbedding_coe.toInducing.specializes_iff
@@ -507,7 +510,7 @@ example [WeaklyLocallyCompactSpace X] [T2Space X] : T4Space (OnePoint X) := infe
 
 /-- If `X` is not a compact space, then `OnePoint X` is a connected space. -/
 instance [PreconnectedSpace X] [NoncompactSpace X] : ConnectedSpace (OnePoint X) where
-  toPreconnectedSpace := denseEmbedding_coe.toIsDenseInducing.preconnectedSpace
+  toPreconnectedSpace := isDenseEmbedding_coe.toIsDenseInducing.preconnectedSpace
   toNonempty := inferInstance
 
 /-- If `X` is an infinite type with discrete topology (e.g., `ℕ`), then the identity map from
diff --git a/Mathlib/Topology/DenseEmbedding.lean b/Mathlib/Topology/DenseEmbedding.lean
index 78c6173ce6866..84bfa9ec96c78 100644
--- a/Mathlib/Topology/DenseEmbedding.lean
+++ b/Mathlib/Topology/DenseEmbedding.lean
@@ -11,9 +11,9 @@ import Mathlib.Topology.Bases
 
 This file defines three properties of functions:
 
-* `DenseRange f`      means `f` has dense image;
-* `IsDenseInducing i` means `i` is also `Inducing`, namely it induces the topology on its codomain;
-* `DenseEmbedding e`  means `e` is further an `Embedding`, namely it is injective and `Inducing`.
+* `DenseRange f`       means `f` has dense image;
+* `IsDenseInducing i`  means `i` is also `Inducing`, namely it induces the topology on its codomain;
+* `IsDenseEmbedding e` means `e` is further an `Embedding`, namely it is injective and `Inducing`.
 
 The main theorem `continuous_extend` gives a criterion for a function
 `f : X → Z` to a T₃ space Z to extend along a dense embedding
@@ -202,37 +202,40 @@ theorem mk' (i : α → β) (c : Continuous i) (dense : ∀ x, x ∈ closure (ra
 end IsDenseInducing
 
 /-- A dense embedding is an embedding with dense image. -/
-structure DenseEmbedding [TopologicalSpace α] [TopologicalSpace β] (e : α → β) extends
+structure IsDenseEmbedding [TopologicalSpace α] [TopologicalSpace β] (e : α → β) extends
   IsDenseInducing e : Prop where
   /-- A dense embedding is injective. -/
   inj : Function.Injective e
 
-theorem DenseEmbedding.mk' [TopologicalSpace α] [TopologicalSpace β] (e : α → β) (c : Continuous e)
+lemma IsDenseEmbedding.mk' [TopologicalSpace α] [TopologicalSpace β] (e : α → β) (c : Continuous e)
     (dense : DenseRange e) (inj : Function.Injective e)
-    (H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (e a), ∀ b, e b ∈ t → b ∈ s) : DenseEmbedding e :=
+    (H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (e a), ∀ b, e b ∈ t → b ∈ s) : IsDenseEmbedding e :=
   { IsDenseInducing.mk' e c dense H with inj }
 
-namespace DenseEmbedding
+@[deprecated (since := "2024-09-30")]
+alias DenseEmbedding.mk' := IsDenseEmbedding.mk'
+
+namespace IsDenseEmbedding
 
 open TopologicalSpace
 
 variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ]
 variable {e : α → β}
 
-theorem inj_iff (de : DenseEmbedding e) {x y} : e x = e y ↔ x = y :=
+theorem inj_iff (de : IsDenseEmbedding e) {x y} : e x = e y ↔ x = y :=
   de.inj.eq_iff
 
-theorem to_embedding (de : DenseEmbedding e) : Embedding e :=
+theorem to_embedding (de : IsDenseEmbedding e) : Embedding e :=
   { induced := de.induced
     inj := de.inj }
 
-/-- If the domain of a `DenseEmbedding` is a separable space, then so is its codomain. -/
-protected theorem separableSpace [SeparableSpace α] (de : DenseEmbedding e) : SeparableSpace β :=
+/-- If the domain of a `IsDenseEmbedding` is a separable space, then so is its codomain. -/
+protected theorem separableSpace [SeparableSpace α] (de : IsDenseEmbedding e) : SeparableSpace β :=
   de.toIsDenseInducing.separableSpace
 
 /-- The product of two dense embeddings is a dense embedding. -/
-protected theorem prod {e₁ : α → β} {e₂ : γ → δ} (de₁ : DenseEmbedding e₁)
-    (de₂ : DenseEmbedding e₂) : DenseEmbedding fun p : α × γ => (e₁ p.1, e₂ p.2) :=
+protected theorem prod {e₁ : α → β} {e₂ : γ → δ} (de₁ : IsDenseEmbedding e₁)
+    (de₂ : IsDenseEmbedding e₂) : IsDenseEmbedding fun p : α × γ => (e₁ p.1, e₂ p.2) :=
   { de₁.toIsDenseInducing.prod de₂.toIsDenseInducing with
     inj := de₁.inj.prodMap de₂.inj }
 
@@ -242,8 +245,8 @@ def subtypeEmb {α : Type*} (p : α → Prop) (e : α → β) (x : { x // p x })
     { x // x ∈ closure (e '' { x | p x }) } :=
   ⟨e x, subset_closure <| mem_image_of_mem e x.prop⟩
 
-protected theorem subtype (de : DenseEmbedding e) (p : α → Prop) :
-    DenseEmbedding (subtypeEmb p e) :=
+protected theorem subtype (de : IsDenseEmbedding e) (p : α → Prop) :
+    IsDenseEmbedding (subtypeEmb p e) :=
   { dense :=
       dense_iff_closure_eq.2 <| by
         ext ⟨x, hx⟩
@@ -255,18 +258,24 @@ protected theorem subtype (de : DenseEmbedding e) (p : α → Prop) :
         simp [subtypeEmb, nhds_subtype_eq_comap, de.toInducing.nhds_eq_comap, comap_comap,
           Function.comp_def] }
 
-theorem dense_image (de : DenseEmbedding e) {s : Set α} : Dense (e '' s) ↔ Dense s :=
+theorem dense_image (de : IsDenseEmbedding e) {s : Set α} : Dense (e '' s) ↔ Dense s :=
   de.toIsDenseInducing.dense_image
 
-end DenseEmbedding
-
-theorem denseEmbedding_id {α : Type*} [TopologicalSpace α] : DenseEmbedding (id : α → α) :=
+protected lemma id {α : Type*} [TopologicalSpace α] : IsDenseEmbedding (id : α → α) :=
   { embedding_id with dense := denseRange_id }
 
-theorem Dense.denseEmbedding_val [TopologicalSpace α] {s : Set α} (hs : Dense s) :
-    DenseEmbedding ((↑) : s → α) :=
+end IsDenseEmbedding
+
+@[deprecated (since := "2024-09-30")]
+alias denseEmbedding_id := IsDenseEmbedding.id
+
+theorem Dense.isDenseEmbedding_val [TopologicalSpace α] {s : Set α} (hs : Dense s) :
+    IsDenseEmbedding ((↑) : s → α) :=
   { embedding_subtype_val with dense := hs.denseRange_val }
 
+@[deprecated (since := "2024-09-30")]
+alias Dense.denseEmbedding_val := Dense.isDenseEmbedding_val
+
 theorem isClosed_property [TopologicalSpace β] {e : α → β} {p : β → Prop} (he : DenseRange e)
     (hp : IsClosed { x | p x }) (h : ∀ a, p (e a)) : ∀ b, p b :=
   have : univ ⊆ { b | p b } :=
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
index bc14d3525fda0..228d23d3112d8 100644
--- a/Mathlib/Topology/Homeomorph.lean
+++ b/Mathlib/Topology/Homeomorph.lean
@@ -308,9 +308,12 @@ protected theorem t2Space [T2Space X] (h : X ≃ₜ Y) : T2Space Y :=
 protected theorem t3Space [T3Space X] (h : X ≃ₜ Y) : T3Space Y :=
   h.symm.embedding.t3Space
 
-protected theorem denseEmbedding (h : X ≃ₜ Y) : DenseEmbedding h :=
+theorem isDenseEmbedding (h : X ≃ₜ Y) : IsDenseEmbedding h :=
   { h.embedding with dense := h.surjective.denseRange }
 
+@[deprecated (since := "2024-09-30")]
+alias denseEmbedding := isDenseEmbedding
+
 @[simp]
 theorem isOpen_preimage (h : X ≃ₜ Y) {s : Set Y} : IsOpen (h ⁻¹' s) ↔ IsOpen s :=
   h.quotientMap.isOpen_preimage
@@ -901,7 +904,10 @@ protected lemma quotientMap : QuotientMap f := (hf.homeomorph f).quotientMap
 protected lemma embedding : Embedding f := (hf.homeomorph f).embedding
 protected lemma openEmbedding : OpenEmbedding f := (hf.homeomorph f).openEmbedding
 protected lemma closedEmbedding : ClosedEmbedding f := (hf.homeomorph f).closedEmbedding
-protected lemma denseEmbedding : DenseEmbedding f := (hf.homeomorph f).denseEmbedding
+lemma isDenseEmbedding : IsDenseEmbedding f := (hf.homeomorph f).isDenseEmbedding
+
+@[deprecated (since := "2024-09-30")]
+alias denseEmbedding := isDenseEmbedding
 
 end IsHomeomorph
 
diff --git a/Mathlib/Topology/Instances/Complex.lean b/Mathlib/Topology/Instances/Complex.lean
index 8cfe0e613fcb3..6b8e3c0862a14 100644
--- a/Mathlib/Topology/Instances/Complex.lean
+++ b/Mathlib/Topology/Instances/Complex.lean
@@ -39,7 +39,7 @@ theorem Complex.subfield_eq_of_closed {K : Subfield ℂ} (hc : IsClosed (K : Set
     simp only [Function.comp_apply, ofReal_ratCast, SetLike.mem_coe, SubfieldClass.ratCast_mem]
   nth_rw 1 [range_comp]
   refine subset_trans ?_ (image_closure_subset_closure_image continuous_ofReal)
-  rw [DenseRange.closure_range Rat.denseEmbedding_coe_real.dense]
+  rw [DenseRange.closure_range Rat.isDenseEmbedding_coe_real.dense]
   simp only [image_univ]
   rfl
 
@@ -106,7 +106,7 @@ theorem Complex.uniformContinuous_ringHom_eq_id_or_conj (K : Subfield ℂ) {ψ :
         simp only [id, Set.image_id']
         rfl ⟩
     convert DenseRange.comp (Function.Surjective.denseRange _)
-        (DenseEmbedding.subtype denseEmbedding_id (K : Set ℂ)).dense (by continuity : Continuous j)
+      (IsDenseEmbedding.id.subtype (K : Set ℂ)).dense (by continuity : Continuous j)
     rintro ⟨y, hy⟩
     use
       ⟨y, by
diff --git a/Mathlib/Topology/Instances/Rat.lean b/Mathlib/Topology/Instances/Rat.lean
index 1fd5e8eaa6966..22cc2d6c6f682 100644
--- a/Mathlib/Topology/Instances/Rat.lean
+++ b/Mathlib/Topology/Instances/Rat.lean
@@ -33,11 +33,14 @@ theorem uniformContinuous_coe_real : UniformContinuous ((↑) : ℚ → ℝ) :=
 theorem uniformEmbedding_coe_real : UniformEmbedding ((↑) : ℚ → ℝ) :=
   uniformEmbedding_comap Rat.cast_injective
 
-theorem denseEmbedding_coe_real : DenseEmbedding ((↑) : ℚ → ℝ) :=
-  uniformEmbedding_coe_real.denseEmbedding Rat.denseRange_cast
+theorem isDenseEmbedding_coe_real : IsDenseEmbedding ((↑) : ℚ → ℝ) :=
+  uniformEmbedding_coe_real.isDenseEmbedding Rat.denseRange_cast
+
+@[deprecated (since := "2024-09-30")]
+alias denseEmbedding_coe_real := isDenseEmbedding_coe_real
 
 theorem embedding_coe_real : Embedding ((↑) : ℚ → ℝ) :=
-  denseEmbedding_coe_real.to_embedding
+  isDenseEmbedding_coe_real.to_embedding
 
 theorem continuous_coe_real : Continuous ((↑) : ℚ → ℝ) :=
   uniformContinuous_coe_real.continuous
diff --git a/Mathlib/Topology/Instances/RatLemmas.lean b/Mathlib/Topology/Instances/RatLemmas.lean
index 16c498e04a27f..69619e025121f 100644
--- a/Mathlib/Topology/Instances/RatLemmas.lean
+++ b/Mathlib/Topology/Instances/RatLemmas.lean
@@ -39,7 +39,7 @@ namespace Rat
 variable {p q : ℚ} {s t : Set ℚ}
 
 theorem interior_compact_eq_empty (hs : IsCompact s) : interior s = ∅ :=
-  denseEmbedding_coe_real.toIsDenseInducing.interior_compact_eq_empty dense_irrational hs
+  isDenseEmbedding_coe_real.toIsDenseInducing.interior_compact_eq_empty dense_irrational hs
 
 theorem dense_compl_compact (hs : IsCompact s) : Dense sᶜ :=
   interior_eq_empty_iff_dense_compl.1 (interior_compact_eq_empty hs)
diff --git a/Mathlib/Topology/Instances/RealVectorSpace.lean b/Mathlib/Topology/Instances/RealVectorSpace.lean
index a7eaa801c1d9f..5d4327d792021 100644
--- a/Mathlib/Topology/Instances/RealVectorSpace.lean
+++ b/Mathlib/Topology/Instances/RealVectorSpace.lean
@@ -23,7 +23,7 @@ theorem map_real_smul {G} [FunLike G E F] [AddMonoidHomClass G E F] (f : G) (hf
     (c : ℝ) (x : E) :
     f (c • x) = c • f x :=
   suffices (fun c : ℝ => f (c • x)) = fun c : ℝ => c • f x from congr_fun this c
-  Rat.denseEmbedding_coe_real.dense.equalizer (hf.comp <| continuous_id.smul continuous_const)
+  Rat.isDenseEmbedding_coe_real.dense.equalizer (hf.comp <| continuous_id.smul continuous_const)
     (continuous_id.smul continuous_const) (funext fun r => map_ratCast_smul f ℝ ℝ r x)
 
 namespace AddMonoidHom
diff --git a/Mathlib/Topology/StoneCech.lean b/Mathlib/Topology/StoneCech.lean
index 240f69c279ec2..3beed85e1b698 100644
--- a/Mathlib/Topology/StoneCech.lean
+++ b/Mathlib/Topology/StoneCech.lean
@@ -154,10 +154,13 @@ theorem isDenseInducing_pure : @IsDenseInducing _ _ ⊥ _ (pure : α → Ultrafi
 
 -- The following refined version will never be used
 /-- `pure : α → Ultrafilter α` defines a dense embedding of `α` in `Ultrafilter α`. -/
-theorem denseEmbedding_pure : @DenseEmbedding _ _ ⊥ _ (pure : α → Ultrafilter α) :=
+theorem isDenseEmbedding_pure : @IsDenseEmbedding _ _ ⊥ _ (pure : α → Ultrafilter α) :=
   letI : TopologicalSpace α := ⊥
   { isDenseInducing_pure with inj := ultrafilter_pure_injective }
 
+@[deprecated (since := "2024-09-30")]
+alias denseEmbedding_pure := isDenseEmbedding_pure
+
 end Embedding
 
 section Extension
diff --git a/Mathlib/Topology/UniformSpace/CompareReals.lean b/Mathlib/Topology/UniformSpace/CompareReals.lean
index 709fc27902447..7a90e73b4afcc 100644
--- a/Mathlib/Topology/UniformSpace/CompareReals.lean
+++ b/Mathlib/Topology/UniformSpace/CompareReals.lean
@@ -73,7 +73,7 @@ def rationalCauSeqPkg : @AbstractCompletion ℚ <| (@AbsoluteValue.abs ℚ _).un
     (uniformInducing := by
       rw [Rat.uniformSpace_eq]
       exact Rat.uniformEmbedding_coe_real.toUniformInducing)
-    (dense := Rat.denseEmbedding_coe_real.dense)
+    (dense := Rat.isDenseEmbedding_coe_real.dense)
 
 namespace CompareReals
 
diff --git a/Mathlib/Topology/UniformSpace/Completion.lean b/Mathlib/Topology/UniformSpace/Completion.lean
index b038f0744d751..0f386364453d4 100644
--- a/Mathlib/Topology/UniformSpace/Completion.lean
+++ b/Mathlib/Topology/UniformSpace/Completion.lean
@@ -183,12 +183,15 @@ theorem denseRange_pureCauchy : DenseRange (pureCauchy : α → CauchyFilter α)
 theorem isDenseInducing_pureCauchy : IsDenseInducing (pureCauchy : α → CauchyFilter α) :=
   uniformInducing_pureCauchy.isDenseInducing denseRange_pureCauchy
 
-theorem denseEmbedding_pureCauchy : DenseEmbedding (pureCauchy : α → CauchyFilter α) :=
-  uniformEmbedding_pureCauchy.denseEmbedding denseRange_pureCauchy
+theorem isDenseEmbedding_pureCauchy : IsDenseEmbedding (pureCauchy : α → CauchyFilter α) :=
+  uniformEmbedding_pureCauchy.isDenseEmbedding denseRange_pureCauchy
+
+@[deprecated (since := "2024-09-30")]
+alias denseEmbedding_pureCauchy := isDenseEmbedding_pureCauchy
 
 theorem nonempty_cauchyFilter_iff : Nonempty (CauchyFilter α) ↔ Nonempty α := by
   constructor <;> rintro ⟨c⟩
-  · have := eq_univ_iff_forall.1 denseEmbedding_pureCauchy.toIsDenseInducing.closure_range c
+  · have := eq_univ_iff_forall.1 isDenseEmbedding_pureCauchy.toIsDenseInducing.closure_range c
     obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial
     exact ⟨a⟩
   · exact ⟨pureCauchy c⟩
@@ -377,9 +380,12 @@ open TopologicalSpace
 instance separableSpace_completion [SeparableSpace α] : SeparableSpace (Completion α) :=
   Completion.isDenseInducing_coe.separableSpace
 
-theorem denseEmbedding_coe [T0Space α] : DenseEmbedding ((↑) : α → Completion α) :=
+theorem isDenseEmbedding_coe [T0Space α] : IsDenseEmbedding ((↑) : α → Completion α) :=
   { isDenseInducing_coe with inj := separated_pureCauchy_injective }
 
+@[deprecated (since := "2024-09-30")]
+alias denseEmbedding_coe := isDenseEmbedding_coe
+
 theorem denseRange_coe₂ :
     DenseRange fun x : α × β => ((x.1 : Completion α), (x.2 : Completion β)) :=
   denseRange_coe.prod_map denseRange_coe
diff --git a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean
index 9029d071993e6..048ea735a5df4 100644
--- a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean
+++ b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean
@@ -219,10 +219,13 @@ protected theorem UniformEmbedding.embedding {f : α → β} (h : UniformEmbeddi
   { toInducing := h.toUniformInducing.inducing
     inj := h.inj }
 
-theorem UniformEmbedding.denseEmbedding {f : α → β} (h : UniformEmbedding f) (hd : DenseRange f) :
-    DenseEmbedding f :=
+theorem UniformEmbedding.isDenseEmbedding {f : α → β} (h : UniformEmbedding f) (hd : DenseRange f) :
+    IsDenseEmbedding f :=
   { h.embedding with dense := hd }
 
+@[deprecated (since := "2024-09-30")]
+alias UniformEmbedding.denseEmbedding := UniformEmbedding.isDenseEmbedding
+
 theorem closedEmbedding_of_spaced_out {α} [TopologicalSpace α] [DiscreteTopology α]
     [T0Space β] {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
     (hf : Pairwise fun x y => (f x, f y) ∉ s) : ClosedEmbedding f := by
@@ -246,9 +249,9 @@ theorem closure_image_mem_nhds_of_uniformInducing {s : Set (α × α)} {e : α 
   exact ⟨e x, hxV, mem_image_of_mem e hxU⟩
 
 theorem uniformEmbedding_subtypeEmb (p : α → Prop) {e : α → β} (ue : UniformEmbedding e)
-    (de : DenseEmbedding e) : UniformEmbedding (DenseEmbedding.subtypeEmb p e) :=
+    (de : IsDenseEmbedding e) : UniformEmbedding (IsDenseEmbedding.subtypeEmb p e) :=
   { comap_uniformity := by
-      simp [comap_comap, Function.comp_def, DenseEmbedding.subtypeEmb, uniformity_subtype,
+      simp [comap_comap, Function.comp_def, IsDenseEmbedding.subtypeEmb, uniformity_subtype,
         ue.comap_uniformity.symm]
     inj := (de.subtype p).inj }
 
@@ -434,14 +437,15 @@ theorem uniform_extend_subtype [CompleteSpace γ] {p : α → Prop} {e : α →
     {s : Set α} (hf : UniformContinuous fun x : Subtype p => f x.val) (he : UniformEmbedding e)
     (hd : ∀ x : β, x ∈ closure (range e)) (hb : closure (e '' s) ∈ 𝓝 b) (hs : IsClosed s)
     (hp : ∀ x ∈ s, p x) : ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c) := by
-  have de : DenseEmbedding e := he.denseEmbedding hd
-  have de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e) := de.subtype p
-  have ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e) := uniformEmbedding_subtypeEmb _ he de
+  have de : IsDenseEmbedding e := he.isDenseEmbedding hd
+  have de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e) := de.subtype p
+  have ue' : UniformEmbedding (IsDenseEmbedding.subtypeEmb p e) :=
+    uniformEmbedding_subtypeEmb _ he de
   have : b ∈ closure (e '' { x | p x }) :=
     (closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb)
   let ⟨c, hc⟩ := uniformly_extend_exists ue'.toUniformInducing de'.dense hf ⟨b, this⟩
   replace hc : Tendsto (f ∘ Subtype.val (p := p)) (((𝓝 b).comap e).comap Subtype.val) (𝓝 c) := by
-    simpa only [nhds_subtype_eq_comap, comap_comap, DenseEmbedding.subtypeEmb_coe] using hc
+    simpa only [nhds_subtype_eq_comap, comap_comap, IsDenseEmbedding.subtypeEmb_coe] using hc
   refine ⟨c, (tendsto_comap'_iff ?_).1 hc⟩
   rw [Subtype.range_coe_subtype]
   exact ⟨_, hb, by rwa [← de.toInducing.closure_eq_preimage_closure_image, hs.closure_eq]⟩
diff --git a/scripts/no_lints_prime_decls.txt b/scripts/no_lints_prime_decls.txt
index e8be7c1b7ded7..d66cd78fe7c09 100644
--- a/scripts/no_lints_prime_decls.txt
+++ b/scripts/no_lints_prime_decls.txt
@@ -998,7 +998,7 @@ decide_True'
 DedekindDomain.ProdAdicCompletions.algebra'
 DedekindDomain.ProdAdicCompletions.algebraMap_apply'
 DedekindDomain.ProdAdicCompletions.IsFiniteAdele.algebraMap'
-DenseEmbedding.mk'
+IsDenseEmbedding.mk'
 Dense.exists_ge'
 Dense.exists_le'
 IsDenseInducing.extend_eq_at'