diff --git a/Mathlib/Algebra/Polynomial/Bivariate.lean b/Mathlib/Algebra/Polynomial/Bivariate.lean
index c2064ba46b87fb..19e5486a598d95 100644
--- a/Mathlib/Algebra/Polynomial/Bivariate.lean
+++ b/Mathlib/Algebra/Polynomial/Bivariate.lean
@@ -353,6 +353,7 @@ lemma pderiv_zero_equivMvPolynomial {R : Type*} [CommRing R] (p : R[X][Y]) :
     simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]
     simp [map_nsmul]
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2025-12-09")]
 alias Polynomial.Bivariate.pderiv_zero_equivMvPolynomial := pderiv_zero_equivMvPolynomial
 
@@ -367,6 +368,7 @@ lemma pderiv_one_equivMvPolynomial (p : R[X][Y]) :
     simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]
     simp [derivative_pow]
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2025-12-09")]
 alias Polynomial.Bivariate.pderiv_one_equivMvPolynomial := pderiv_one_equivMvPolynomial
 
diff --git a/Mathlib/Analysis/Distribution/Support.lean b/Mathlib/Analysis/Distribution/Support.lean
index aea1884470473b..1598e7ae0ae86b 100644
--- a/Mathlib/Analysis/Distribution/Support.lean
+++ b/Mathlib/Analysis/Distribution/Support.lean
@@ -189,7 +189,7 @@ theorem smulLeftCLM (hf : IsVanishingOn f s) {g : E → ℂ} (hg : g.HasTemperat
   rw [SchwartzMap.smulLeftCLM_apply hg]
   exact (tsupport_smul_subset_right g u).trans hu
 
-@[deprecated (since := "2026-06-27")] alias Distribution.IsVanishingOn.smulLeftCLM :=
+@[deprecated (since := "2026-07-01")] alias _root_.Distribution.IsVanishingOn.smulLeftCLM :=
   Distribution.TemperedDistribution.IsVanishingOn.smulLeftCLM
 
 open LineDeriv
@@ -225,7 +225,7 @@ theorem dsupport_smulLeftCLM_subset {g : E → ℂ} (hg : g.HasTemperateGrowth)
     dsupport (smulLeftCLM F g f) ⊆ dsupport f := by
   gcongr; fun_prop
 
-@[deprecated (since := "2026-06-27")] alias Distribution.dsupport_smulLeftCLM_subset :=
+@[deprecated (since := "2026-07-01")] alias _root_.Distribution.dsupport_smulLeftCLM_subset :=
   Distribution.TemperedDistribution.dsupport_smulLeftCLM_subset
 
 open LineDeriv
diff --git a/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean b/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
index a2b446dbaae0ef..97df41135bc48e 100644
--- a/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
+++ b/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
@@ -140,6 +140,7 @@ theorem directSum_isInternal_of_pairwise_commute [DecidableEq (n → 𝕜)]
   · rw [iSup_iInf_eq_top_of_commute hT hC, top_orthogonal_eq_bot]
   · exact orthogonalFamily_iInf_eigenspaces hT
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-05-24")]
 alias LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute :=
   directSum_isInternal_of_pairwise_commute
diff --git a/Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean b/Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean
index c8a557f1e6ca79..52352ccc4076a4 100644
--- a/Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean
+++ b/Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean
@@ -131,23 +131,27 @@ def iso₂Mk {α β : a ⟶ b} (el : α.l ≅ β.l) (er : β.r ≅ α.r)
 
 namespace Bicategory
 
+set_option linter.dupNamespace false in
 /-- The associator in the bicategory `Adj B`. -/
 @[simps!]
 def associator (α : a ⟶ b) (β : b ⟶ c) (γ : c ⟶ d) : (α ≫ β) ≫ γ ≅ α ≫ β ≫ γ :=
   iso₂Mk (α_ _ _ _) (α_ _ _ _) (conjugateEquiv_associator_hom _ _ _)
 
+set_option linter.dupNamespace false in
 /-- The left unitor in the bicategory `Adj B`. -/
 @[simps!]
 def leftUnitor (α : a ⟶ b) : 𝟙 a ≫ α ≅ α :=
   iso₂Mk (λ_ _) (ρ_ _).symm
     (by simpa using conjugateEquiv_id_comp_right_apply α.adj α.adj (𝟙 _))
 
+set_option linter.dupNamespace false in
 /-- The right unitor in the bicategory `Adj B`. -/
 @[simps!]
 def rightUnitor (α : a ⟶ b) : α ≫ 𝟙 b ≅ α :=
   iso₂Mk (ρ_ _) (λ_ _).symm
     (by simpa using conjugateEquiv_comp_id_right_apply α.adj α.adj (𝟙 _))
 
+set_option linter.dupNamespace false in
 /-- The left whiskering in the bicategory `Adj B`. -/
 @[simps]
 def whiskerLeft (α : a ⟶ b) {β β' : b ⟶ c} (y : β ⟶ β') : α ≫ β ⟶ α ≫ β' where
@@ -156,6 +160,7 @@ def whiskerLeft (α : a ⟶ b) {β β' : b ⟶ c} (y : β ⟶ β') : α ≫ β 
   conjugateEquiv_τl := by
     simp [conjugateEquiv_whiskerLeft, Hom₂.conjugateEquiv_τl]
 
+set_option linter.dupNamespace false in
 /-- The right whiskering in the bicategory `Adj B`. -/
 @[simps]
 def whiskerRight {α α' : a ⟶ b} (x : α ⟶ α') (β : b ⟶ c) : α ≫ β ⟶ α' ≫ β where
diff --git a/Mathlib/CategoryTheory/Groupoid/VertexGroup.lean b/Mathlib/CategoryTheory/Groupoid/VertexGroup.lean
index 289facce1b9efe..df6fd2c21367e8 100644
--- a/Mathlib/CategoryTheory/Groupoid/VertexGroup.lean
+++ b/Mathlib/CategoryTheory/Groupoid/VertexGroup.lean
@@ -83,9 +83,11 @@ def _root_.CategoryTheory.Functor.mapVertexGroup {D : Type v} [Groupoid D] (φ :
   map_one' := φ.map_id c
   map_mul' := φ.map_comp
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-05-24")]
 alias CategoryTheory.Functor.mapVertexGroup := CategoryTheory.Functor.mapVertexGroup
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-05-24")]
 alias CategoryTheory.Functor.mapVertexGroup_apply := CategoryTheory.Functor.mapVertexGroup_apply
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
index ad855e72608a3d..d1cc9b3eb0f9bc 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
@@ -204,8 +204,7 @@ def pushout.desc' {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h
     { l : pushout f g ⟶ W // pushout.inl _ _ ≫ l = h ∧ pushout.inr _ _ ≫ l = k } :=
   ⟨pushout.desc h k w, pushout.inl_desc _ _ _, pushout.inr_desc _ _ _⟩
 
-@[deprecated (since := "2026-06-25")]
-alias CategoryTheory.Limits.pullback.desc' := pushout.desc'
+@[deprecated (since := "2026-06-25")] alias pullback.desc' := pushout.desc'
 
 @[reassoc]
 theorem pullback.condition {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] :
diff --git a/Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean b/Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean
index ce1187d910572b..bce43342532765 100644
--- a/Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean
+++ b/Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean
@@ -392,6 +392,7 @@ namespace SubobjectRepresentableBy
 given `h : SubobjectRepresentableBy Ω`. -/
 def Ω₀ : Subobject Ω := h.homEquiv (𝟙 Ω)
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.Ω₀ := Ω₀
 @[deprecated (since := "2026-03-06")]
@@ -403,6 +404,7 @@ lemma homEquiv_eq {X : C} (f : X ⟶ Ω) :
     h.homEquiv f = (Subobject.pullback f).obj h.Ω₀ := by
   simpa using! h.homEquiv_comp f (𝟙 _)
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.homEquiv_eq := homEquiv_eq
 @[deprecated (since := "2026-03-06")]
@@ -414,6 +416,7 @@ lemma pullback_homEquiv_symm_obj_Ω₀ {X : C} (x : Subobject X) :
     (Subobject.pullback (h.homEquiv.symm x)).obj h.Ω₀ = x := by
   rw [← homEquiv_eq, Equiv.apply_symm_apply]
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀ :=
   pullback_homEquiv_symm_obj_Ω₀
@@ -428,6 +431,7 @@ variable {U X : C} (m : U ⟶ X) [Mono m]
 /-- `h.χ m` is the characteristic map of monomorphism `m` given by the bijection `h.homEquiv`. -/
 def χ : X ⟶ Ω := h.homEquiv.symm (Subobject.mk m)
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.χ := χ
 @[deprecated (since := "2026-03-06")]
@@ -440,6 +444,7 @@ noncomputable def iso : MonoOver.mk m ≅
   (Subobject.representativeIso (.mk m)).symm ≪≫ Subobject.representative.mapIso
     (eqToIso (h.pullback_homEquiv_symm_obj_Ω₀ (.mk m)).symm)
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.iso := iso
 @[deprecated (since := "2026-03-06")]
@@ -459,6 +464,7 @@ alias _root_.CategoryTheory.Classifier.SubobjectRepresentableBy.iso := iso
 noncomputable def π : U ⟶ Subobject.underlying.obj h.Ω₀ :=
   (h.iso m).hom.hom.left ≫ Subobject.pullbackπ (h.χ m) h.Ω₀
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.π := π
 @[deprecated (since := "2026-03-06")]
@@ -473,6 +479,7 @@ lemma iso_inv_left_π :
   convert! Category.id_comp _ using 2
   exact (MonoOver.forget _ ⋙ Over.forget _).congr_map (h.iso m).inv_hom_id
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π := iso_inv_left_π
 @[deprecated (since := "2026-03-06")]
@@ -484,6 +491,7 @@ lemma iso_inv_hom_left_comp :
       ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow :=
   MonoOver.w (h.iso m).inv
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp :=
   iso_inv_hom_left_comp
@@ -491,6 +499,7 @@ alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_
 alias _root_.CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp :=
   iso_inv_hom_left_comp
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2025-12-18")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_comp :=
   iso_inv_hom_left_comp
@@ -503,6 +512,7 @@ lemma isPullback {U X : C} (m : U ⟶ X) [Mono m] :
     (Iso.refl _) (Iso.refl _)
   all_goals simp [MonoOver.forget]
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.isPullback := isPullback
 @[deprecated (since := "2026-03-06")]
@@ -515,6 +525,7 @@ lemma uniq {χ' : X ⟶ Ω} {π : U ⟶ h.Ω₀}
   simp only [χ, Equiv.apply_symm_apply, homEquiv_eq]
   simpa using! Subobject.pullback_obj_mk sq.flip
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.uniq := uniq
 @[deprecated (since := "2026-03-06")]
@@ -532,6 +543,7 @@ noncomputable def isTerminalΩ₀ : IsTerminal (h.Ω₀ : C) :=
     rw [← cancel_mono h.Ω₀.arrow, h.uniq this,
       ← (h.isPullback (𝟙 X)).w, Category.id_comp])
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.isTerminalΩ₀ := isTerminalΩ₀
 @[deprecated (since := "2026-03-06")]
@@ -540,6 +552,7 @@ alias _root_.CategoryTheory.Classifier.SubobjectRepresentableBy.isTerminalΩ₀
 /-- The unique map to the terminal object. -/
 noncomputable def χ₀ (U : C) : U ⟶ h.Ω₀ := h.isTerminalΩ₀.from U
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.χ₀ := χ₀
 @[deprecated (since := "2026-03-06")]
@@ -548,6 +561,7 @@ alias _root_.CategoryTheory.Classifier.SubobjectRepresentableBy.χ₀ := χ₀
 include h in
 lemma hasTerminal : HasTerminal C := h.isTerminalΩ₀.hasTerminal
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.hasTerminal := hasTerminal
 @[deprecated (since := "2026-03-06")]
@@ -559,6 +573,7 @@ variable [HasTerminal C]
 noncomputable def isoΩ₀ : (h.Ω₀ : C) ≅ ⊤_ C :=
   h.isTerminalΩ₀.conePointUniqueUpToIso (limit.isLimit _)
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.isoΩ₀ := isoΩ₀
 @[deprecated (since := "2026-03-06")]
@@ -582,6 +597,7 @@ noncomputable def classifier : Subobject.Classifier C where
         (by simp) (h.isTerminalΩ₀.hom_ext _ _) (by simp) (by simp)
     exact h.uniq this
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-06")]
 alias _root.CategoryTheory.Classifier.SubobjectRepresentableBy.classifier := classifier
 @[deprecated (since := "2026-03-06")]
diff --git a/Mathlib/Data/Set/FiniteExhaustion.lean b/Mathlib/Data/Set/FiniteExhaustion.lean
index 1d9bd2db3e8194..10b3a9449870e0 100644
--- a/Mathlib/Data/Set/FiniteExhaustion.lean
+++ b/Mathlib/Data/Set/FiniteExhaustion.lean
@@ -80,6 +80,7 @@ lemma _root_.Set.nonempty_finiteExhaustion_iff {s : Set α} :
   rw [← K.iUnion_eq]
   exact countable_iUnion <| fun i ↦ (K.finite i).countable
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-05-24")]
 alias Set.nonempty_finiteExhaustion_iff := Set.nonempty_finiteExhaustion_iff
 
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
index 389c63c3be81ce..77f7642f8e1a13 100644
--- a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
+++ b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
@@ -317,6 +317,7 @@ theorem mdifferentiable [ContMDiffVectorBundle 1 F Z I]
     e.MDifferentiable (I.prod 𝓘(𝕜, F)) (I.prod 𝓘(𝕜, F)) :=
   ⟨e.contMDiffOn.mdifferentiableOn one_ne_zero, e.contMDiffOn_symm.mdifferentiableOn one_ne_zero⟩
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-05-24")] alias Bundle.Trivialization.mdifferentiable := mdifferentiable
 
 end
diff --git a/Mathlib/GroupTheory/Submonoid/Inverses.lean b/Mathlib/GroupTheory/Submonoid/Inverses.lean
index 847d5ddb31f104..d4efa62017f0eb 100644
--- a/Mathlib/GroupTheory/Submonoid/Inverses.lean
+++ b/Mathlib/GroupTheory/Submonoid/Inverses.lean
@@ -56,6 +56,7 @@ theorem _root_.IsUnit.submonoid.coe_inv [Monoid M] (x : IsUnit.submonoid M) :
 
 @[deprecated (since := "2026-05-24")]
 alias _root_.AddSubmonoid.IsUnit.Submonoid.coe_neg := IsAddUnit.addSubmonoid.coe_neg
+set_option linter.dupNamespace false in
 @[to_additive existing, deprecated (since := "2026-05-24")]
 alias IsUnit.Submonoid.coe_inv := IsUnit.submonoid.coe_inv
 
diff --git a/Mathlib/LinearAlgebra/FreeModule/Basic.lean b/Mathlib/LinearAlgebra/FreeModule/Basic.lean
index 4e9d8b89e6b7bf..37d796cf745408 100644
--- a/Mathlib/LinearAlgebra/FreeModule/Basic.lean
+++ b/Mathlib/LinearAlgebra/FreeModule/Basic.lean
@@ -149,6 +149,7 @@ lemma iff_of_equiv {R R' M M'} [Semiring R] [AddCommMonoid M] [Module R M]
 instance shrink [Small.{w} M] : Module.Free R (Shrink.{w} M) :=
   Module.Free.of_equiv (Shrink.linearEquiv R M).symm
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-04-18")] alias Module.free_shrink := shrink
 
 variable (R M N)
diff --git a/Mathlib/Logic/Equiv/Set.lean b/Mathlib/Logic/Equiv/Set.lean
index c1a73bf4892d9d..b430f0e1e4d1cf 100644
--- a/Mathlib/Logic/Equiv/Set.lean
+++ b/Mathlib/Logic/Equiv/Set.lean
@@ -249,6 +249,7 @@ protected def singleton {α} (a : α) : ({a} : Set α) ≃ PUnit.{u} :=
 lemma _root_.Equiv.strictMono_setCongr {α : Type*} [Preorder α] {S T : Set α} (h : S = T) :
     StrictMono (setCongr h) := fun _ _ ↦ id
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-05-24")] alias Equiv.strictMono_setCongr := Equiv.strictMono_setCongr
 
 /-- If `a ∉ s`, then `insert a s` is equivalent to `s ⊕ PUnit`. -/
diff --git a/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean b/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
index ff7e2f7603593e..32dfaa31d15c60 100644
--- a/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
+++ b/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
@@ -175,58 +175,71 @@ theorem adicAbv_natCast_le_one (n : ℕ) : adicAbv K v n ≤ 1 :=
 theorem adicAbv_intCast_le_one (n : ℤ) : adicAbv K v n ≤ 1 :=
   (isNonarchimedean_adicAbv K v).apply_intCast_le_one
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm := one_lt_absNorm
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm := one_lt_absNorm
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal := one_lt_absNorm_nnreal
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal :=
   one_lt_absNorm_nnreal
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero := absNorm_ne_zero
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero := absNorm_ne_zero
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv := adicAbv
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv := adicAbv
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def := adicAbv_def
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def := adicAbv_def
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv :=
   isNonarchimedean_adicAbv
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv :=
   isNonarchimedean_adicAbv
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.instRankOneAdicCompletion := instRankOneAdicCompletion
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.instRankOneAdicCompletion := instRankOneAdicCompletion
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.instNormedFieldValuedAdicCompletion := instNormedFieldValuedAdicCompletion
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.instNormedFieldValuedAdicCompletion := instNormedFieldValuedAdicCompletion
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.rankOne_hom'_def := rankOne_hom'_def
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.rankOne_hom'_def := rankOne_hom'_def
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.toNNReal_valued_eq_adicAbv := toNNReal_valued_eq_adicAbv
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.toNNReal_valued_eq_adicAbv := toNNReal_valued_eq_adicAbv
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max := adicAbv_add_le_max
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max := adicAbv_add_le_max
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one := adicAbv_natCast_le_one
 @[deprecated (since := "2026-03-11")]
 alias _root_.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one :=
   adicAbv_natCast_le_one
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-03-11")]
 alias NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one := adicAbv_intCast_le_one
 @[deprecated (since := "2026-03-11")]
diff --git a/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean b/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
index d5ffa594968644..5f6e2279bcd393 100644
--- a/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
@@ -309,6 +309,7 @@ open scoped Classical in
 protected noncomputable instance fintype [NumberField K] :
     Fintype (InfinitePlace K) := Set.fintypeRange _
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-05-24")]
 alias NumberField.InfinitePlace.fintype := InfinitePlace.fintype
 
diff --git a/Mathlib/Order/Filter/Germ/Basic.lean b/Mathlib/Order/Filter/Germ/Basic.lean
index dd0aa8723d3e62..8e4bdba81b88d5 100644
--- a/Mathlib/Order/Filter/Germ/Basic.lean
+++ b/Mathlib/Order/Filter/Germ/Basic.lean
@@ -256,6 +256,7 @@ theorem _root_.Filter.Tendsto.congr_germ {f g : β → γ} {l : Filter α} {l' :
     (h : f =ᶠ[l'] g) {φ : α → β} (hφ : Tendsto φ l l') : (f ∘ φ : Germ l γ) = g ∘ φ :=
   EventuallyEq.germ_eq (h.comp_tendsto hφ)
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-05-24")] alias Filter.Tendsto.congr_germ := Filter.Tendsto.congr_germ
 
 lemma isConstant_comp_tendsto {lc : Filter γ} {g : γ → α}
diff --git a/Mathlib/RingTheory/Etale/Basic.lean b/Mathlib/RingTheory/Etale/Basic.lean
index 1277c23b518a03..c941952589073a 100644
--- a/Mathlib/RingTheory/Etale/Basic.lean
+++ b/Mathlib/RingTheory/Etale/Basic.lean
@@ -130,6 +130,7 @@ lemma _root_.Algebra.FormallySmooth.iff_restrictScalars [FormallyEtale R A] :
     Algebra.FormallySmooth R B ↔ Algebra.FormallySmooth A B :=
   ⟨fun _ ↦ .of_restrictScalars R _ _, fun _ ↦ .comp _ A _⟩
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2025-12-09")]
 alias Algebra.FormallyEtale.of_restrictScalars := of_restrictScalars
 
@@ -142,6 +143,7 @@ lemma iff_of_surjective
   rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, ← FormallySmooth.iff_of_surjective h,
     and_iff_right (FormallyUnramified.of_surjective (Algebra.ofId R S) h)]
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2025-12-09")]
 alias Algebra.FormallyEtale.iff_of_surjective := iff_of_surjective
 
diff --git a/Mathlib/RingTheory/Finiteness/Basic.lean b/Mathlib/RingTheory/Finiteness/Basic.lean
index 4ea58f2b32969a..7cb4b5fed17525 100644
--- a/Mathlib/RingTheory/Finiteness/Basic.lean
+++ b/Mathlib/RingTheory/Finiteness/Basic.lean
@@ -324,6 +324,7 @@ universe u in
 instance shrink [Module.Finite R M] [Small.{u} M] : Module.Finite R (Shrink.{u} M) :=
   Module.Finite.equiv (Shrink.linearEquiv R M).symm
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-04-18")] alias Module.finite_shrink := shrink
 
 /-- A submodule is finite as a module iff it is finitely generated. -/
diff --git a/Mathlib/RingTheory/TensorProduct/Maps.lean b/Mathlib/RingTheory/TensorProduct/Maps.lean
index 10c1e8486bc3c8..bc903ffb8e07dd 100644
--- a/Mathlib/RingTheory/TensorProduct/Maps.lean
+++ b/Mathlib/RingTheory/TensorProduct/Maps.lean
@@ -426,6 +426,7 @@ attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 lemma commRight_symm_tmul (s : S) (a : A) :
     (commRight R S A).symm (a ⊗ₜ[R] s) = s ⊗ₜ a := rfl
 
+set_option linter.dupNamespace false in
 @[deprecated (since := "2026-05-24")]
 alias Algebra.TensorProduct.commRight_symm_tmul := commRight_symm_tmul
 
diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean
index 1b1bd995958ab8..b46f67dd8ccc4a 100644
--- a/Mathlib/Tactic/Linter/Lint.lean
+++ b/Mathlib/Tactic/Linter/Lint.lean
@@ -11,7 +11,6 @@ module
 public import Batteries.Tactic.Lint -- shake: keep
 public import Lean.Linter.Deprecated
 public import Mathlib.Tactic.DeclarationNames
-public import Batteries.Tactic.Lint.Basic
 
 /-!
 # Linters for Mathlib
@@ -63,21 +62,19 @@ namespace Mathlib.Linter
 /-!
 ### `dupNamespace` linter
 
-The `dupNamespace` linter produces a warning when a declaration contains the same namespace
-at least twice consecutively.
+The `dupNamespace` linter produces a warning when a component of a declaration name is repeated
+several times. The repetition does not have to be consecutive. Examples: `Nat.Nat.foo`,
+`One.two.two`, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo`, `Nat.Prime.Nat.bar`
 
-For instance, `Nat.Nat.foo` and `One.two.two` trigger a warning, while `Nat.One.Nat` does not.
+The linter also warns about auto-generated declarations (such as, those generated by `to_additive`).
 -/
 
 /--
-The `dupNamespace` linter is set on by default.  Lean emits a warning on any declaration that
-contains the same namespace at least twice consecutively.
+The `dupNamespace` linter produces a warning when a component of a declaration name is repeated
+several times. The repetition does not have to be consecutive. Examples: `Nat.Nat.foo`,
+`One.two.two`, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo`, `Nat.Prime.Nat.bar`
 
-For instance, `Nat.Nat.foo` and `One.two.two` trigger a warning, while `Nat.One.Nat` does not.
-
-*Note.*
-This linter will not detect duplication in namespaces of autogenerated declarations
-(other than the one whose `declId` is present in the source declaration).
+The linter also warns about auto-generated declarations (such as, those generated by `to_additive`).
 -/
 public register_option linter.dupNamespace : Bool := {
   defValue := true
@@ -96,12 +93,23 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do
       aliases ← getAliasSyntax exp
     for id in (← getNamesFrom (stx.getPos?.getD default)) ++ aliases do
       let declName := id.getId
+      -- We intentionally *do* lint deprecated declarations:
+      -- this is important since people can forget to add a `_root_` when adding deprecations.
       if declName.hasMacroScopes || isPrivateName declName then continue
       let nm := declName.components
-      let some (dup, _) := nm.zip (nm.tailD []) |>.find? fun (x, y) ↦ x == y
-        | continue
-      Linter.logLint linter.dupNamespace id
-        m!"The namespace '{dup}' is duplicated in the declaration '{declName}'"
+      -- Collect distinct components which appear more than once.
+      let duplicated := List.eraseDups <| nm.filter (fun comp ↦ nm.count comp > 1)
+      match duplicated with
+      | [] => continue
+      | [ns] =>
+        Linter.logLint linter.dupNamespace id
+          m!"The namespace `{ns}` is duplicated in the declaration \
+          `{.ofConstName (fullNames := true) declName}`."
+      | dup =>
+        let ns := MessageData.andList (duplicated.map (m!"`{·}`"))
+        Linter.logLint linter.dupNamespace id
+          m!"The namespaces {ns} are duplicated in the declaration \
+          `{.ofConstName (fullNames := true) declName}`."
 
 initialize addLinter dupNamespace
 
diff --git a/MathlibTest/Linter/DupNamespace.lean b/MathlibTest/Linter/DupNamespace.lean
index b5013fb0c8d7c5..56e0180ba9b60d 100644
--- a/MathlibTest/Linter/DupNamespace.lean
+++ b/MathlibTest/Linter/DupNamespace.lean
@@ -2,7 +2,7 @@ import Batteries.Tactic.Alias
 import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.ToAdditive
 /--
-warning: The namespace 'add' is duplicated in the declaration 'add.add'
+warning: The namespace `add` is duplicated in the declaration `add.add`.
 
 Note: This linter can be disabled with `set_option linter.dupNamespace false`
 -/
@@ -12,7 +12,7 @@ def add.add := True
 namespace Foo
 
 /--
-warning: The namespace 'Foo' is duplicated in the declaration 'Foo.Foo.foo'
+warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo.foo`.
 
 Note: This linter can be disabled with `set_option linter.dupNamespace false`
 -/
@@ -21,7 +21,7 @@ def Foo.foo := True
 
 set_option linter.translateRedundant false in
 /--
-warning: The namespace 'add' is duplicated in the declaration 'Foo.add.add'
+warning: The namespace `add` is duplicated in the declaration `Foo.add.add`.
 
 Note: This linter can be disabled with `set_option linter.dupNamespace false`
 -/
@@ -37,7 +37,7 @@ run_cmd Lean.Elab.Command.liftTermElabM do
 namespace Nat
 
 /--
-warning: The namespace 'Nat' is duplicated in the declaration 'Foo.Nat.Nat.Nats'
+warning: The namespace `Nat` is duplicated in the declaration `Foo.Nat.Nat.Nats`.
 
 Note: This linter can be disabled with `set_option linter.dupNamespace false`
 -/
@@ -50,11 +50,11 @@ end Foo
 namespace add
 
 /--
-warning: The namespace 'add' is duplicated in the declaration 'add.add'
+warning: The namespace `add` is duplicated in the declaration `add.add`.
 
 Note: This linter can be disabled with `set_option linter.dupNamespace false`
 ---
-warning: The namespace 'add' is duplicated in the declaration 'add.add'
+warning: The namespace `add` is duplicated in the declaration `add.add`.
 
 Note: This linter can be disabled with `set_option linter.dupNamespace false`
 -/
@@ -62,3 +62,111 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false`
 export Nat (add add_comm add)
 
 end add
+
+/--
+warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+lemma Foo.Foo : True := trivial
+
+/--
+warning: The namespace `Foo` is duplicated in the declaration `Bar.Foo.Foo`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+lemma Bar.Foo.Foo : True := trivial
+
+/--
+warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo.Bar`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+lemma Foo.Foo.Bar : True := trivial
+
+/--
+warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo.Bar.Baz.hoge`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+lemma Foo.Foo.Bar.Baz.hoge : True := trivial
+
+#guard_msgs in
+lemma Foo.Foos.Bar.Baz : True := trivial
+
+/--
+warning: The namespace `Foo` is duplicated in the declaration `Foo.Bar.Foo.baz`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+lemma Foo.Bar.Foo.baz : True := trivial
+
+/--
+warning: The namespaces `Foo` and `Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+lemma Foo.Bar.Foo.Bar.baz : True := trivial
+
+/--
+warning: The namespaces `Foo` and `Baz` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Baz.baz`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+lemma Foo.Bar.Baz.Hoge.Foo.Baz.baz : True := trivial
+
+/--
+warning: The namespaces `Foo` and `Bar` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.baz`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+lemma Foo.Bar.Baz.Hoge.Foo.Bar.baz : True := trivial
+
+/--
+warning: The namespaces `Foo`, `Bar`, and `Baz` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.Baz.az`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+lemma Foo.Bar.Baz.Hoge.Foo.Bar.Baz.az : True := trivial
+
+-- The linter detects the final name and not just what's written in the syntax.
+namespace Foo.Bar
+/--
+warning: The namespaces `Foo` and `Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz'`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+def Foo.Bar.baz' := 42
+end Foo.Bar
+
+-- We detect additional generated names.
+/--
+warning: The namespace `AddSubgroup` is duplicated in the declaration `AddSubgroup.AddSubgroup.foo`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+@[to_additive AddSubgroup.AddSubgroup.foo]
+def Subgroup.AddSubgroup.foo := 42
+-- (`AddSubgroup` is duplicated but only after translation)
+
+-- The linter works on deprecated decls: this is important
+-- since people can forget to add a `_root_` when adding deprecations.
+/--
+warning: The namespace `Foo` is duplicated in the declaration `Foo.Bar.Foo.baz'`.
+
+Note: This linter can be disabled with `set_option linter.dupNamespace false`
+-/
+#guard_msgs in
+@[deprecated "" (since := "")]
+def Foo.Bar.Foo.baz' := 42