[Merged by Bors] - feat: make the dupNamespace linter catch any duplicate namespace(s)

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
 

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)

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`. -/

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")]

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
 

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 : γ → α}

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
 

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. -/

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