feat: make the dupNamespace linter catch any duplicate namespace(s) (leanprover-community#39793)

Before this PR, the `dupNamespace` linter would only flag a namespace as duplicate if it was repeated in two consecutive positions: `Foo.Foo.bar` would be linted, but neither `Foo.Bar.Foo.Bar.baz` nor `Foo.Bar.Foo.Baz.baz` would be (even though they are very likely unintentional).

Strengthen the linter check, to error if any namespace component is duplicated.
This has few false positives (which we manually annotate), but catches many pre-existing
cases where the duplication was clearly unintentional and undesirable.

Most of the mathlib adaptation was done in leanprover-community#39794.

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

Author: 2 people

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
 

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

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

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

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
 

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] :

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,13 +491,15 @@ 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
 @[deprecated (since := "2026-03-06")]
 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")]

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
 

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

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