From 66e1af5211fca99ea4977cc3a805aeef47e84726 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 24 May 2026 23:27:38 +0200 Subject: [PATCH 01/27] feat: check for larger overlap windows in the dupNamespace linter --- Mathlib/Tactic/Linter/Lint.lean | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 1b1bd995958ab8..5ae3c78fac1c0e 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -88,6 +88,20 @@ namespace DupNamespaceLinter open Lean Parser Elab Command Meta Linter +def hasDuplicates (items : List Name) : Bool := Id.run do + return !items.Nodup + +#guard hasDuplicates [`Foo, `Foo] == true +#guard hasDuplicates [`Bar, `Foo, `Foo] == true +#guard hasDuplicates [`Foo, `Foo, `Bar] == true +#guard hasDuplicates [`Foo, `Foo, `Bar, `Baz, `hoge] == true +#guard hasDuplicates [`Foo, `Foos, `Bar, `Baz] == false +#guard hasDuplicates [`Foo, `Bar, `Foo, `baz] == true +#guard hasDuplicates [`Foo, `Bar, `Foo, `Bar, `baz] == true +#guard hasDuplicates [`Foo, `Bar, `Baz, `Hoge, `Foo, `Baz, `baz] == true -- `Foo duplicate +#guard hasDuplicates [`Foo, `Bar, `Baz, `Hoge, `Foo, `Bar, `baz] == true -- `Foo, `Bar duplicate +#guard hasDuplicates [`Foo, `Bar, `Baz, `Hoge, `Foo, `Bar, `Baz, `baz] == true -- `Foo, `Bar duplicate + @[inherit_doc linter.dupNamespace] def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do if getLinterValue linter.dupNamespace (← getLinterOptions) then @@ -98,10 +112,13 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do let declName := id.getId 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}'" + if !nm.Nodup then + -- There are duplicate naming components: find the longest substring of duplicate + -- component(s). + let duplicated := nm.filter (fun comp ↦ nm.count comp > 1) + let (s, verb) := if duplicated.length > 1 then ("s", "are") else ("", "is") + Linter.logLint linter.dupNamespace id + m!"The namespace component{s} `{duplicated}` {verb} duplicated in the declaration `{declName}`" initialize addLinter dupNamespace From 3b807aad3ab6990dde625112f8a49d1f2b8d6c7e Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 25 May 2026 13:02:42 +0200 Subject: [PATCH 02/27] chore: better error messages; update tests to include backticks --- Mathlib/Tactic/Linter/Lint.lean | 10 ++++++---- MathlibTest/Lint.lean | 12 ++++++------ 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 5ae3c78fac1c0e..022b60e6e26265 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -12,6 +12,7 @@ public import Batteries.Tactic.Lint -- shake: keep public import Lean.Linter.Deprecated public import Mathlib.Tactic.DeclarationNames public import Batteries.Tactic.Lint.Basic +public meta import Batteries.Data.List.Basic /-! # Linters for Mathlib @@ -115,10 +116,11 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do if !nm.Nodup then -- There are duplicate naming components: find the longest substring of duplicate -- component(s). - let duplicated := nm.filter (fun comp ↦ nm.count comp > 1) - let (s, verb) := if duplicated.length > 1 then ("s", "are") else ("", "is") - Linter.logLint linter.dupNamespace id - m!"The namespace component{s} `{duplicated}` {verb} duplicated in the declaration `{declName}`" + let duplicated := List.pwFilter (· ≠ ·) <| nm.filter (fun comp ↦ nm.count comp > 1) + let msg := if let [ns] := duplicated then + m!"The namespace `{ns}` is duplicated in the declaration `{declName}`" + else m!"The namespaces `{duplicated}` are duplicated in the declaration `{declName}`" + Linter.logLint linter.dupNamespace id msg initialize addLinter dupNamespace diff --git a/MathlibTest/Lint.lean b/MathlibTest/Lint.lean index 391ebca8357334..4aef7f50c4099b 100644 --- a/MathlibTest/Lint.lean +++ b/MathlibTest/Lint.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` -/ From 46afed19c8c30c2eeb5e89c59e7c05964086abdb Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 25 May 2026 13:09:04 +0200 Subject: [PATCH 03/27] End-to-end-test for the new cases, including some by Snir --- Mathlib/Tactic/Linter/Lint.lean | 14 ----- MathlibTest/Lint.lean | 108 ++++++++++++++++++++++++++++++++ 2 files changed, 108 insertions(+), 14 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 022b60e6e26265..121f117161360e 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -89,20 +89,6 @@ namespace DupNamespaceLinter open Lean Parser Elab Command Meta Linter -def hasDuplicates (items : List Name) : Bool := Id.run do - return !items.Nodup - -#guard hasDuplicates [`Foo, `Foo] == true -#guard hasDuplicates [`Bar, `Foo, `Foo] == true -#guard hasDuplicates [`Foo, `Foo, `Bar] == true -#guard hasDuplicates [`Foo, `Foo, `Bar, `Baz, `hoge] == true -#guard hasDuplicates [`Foo, `Foos, `Bar, `Baz] == false -#guard hasDuplicates [`Foo, `Bar, `Foo, `baz] == true -#guard hasDuplicates [`Foo, `Bar, `Foo, `Bar, `baz] == true -#guard hasDuplicates [`Foo, `Bar, `Baz, `Hoge, `Foo, `Baz, `baz] == true -- `Foo duplicate -#guard hasDuplicates [`Foo, `Bar, `Baz, `Hoge, `Foo, `Bar, `baz] == true -- `Foo, `Bar duplicate -#guard hasDuplicates [`Foo, `Bar, `Baz, `Hoge, `Foo, `Bar, `Baz, `baz] == true -- `Foo, `Bar duplicate - @[inherit_doc linter.dupNamespace] def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do if getLinterValue linter.dupNamespace (← getLinterOptions) then diff --git a/MathlibTest/Lint.lean b/MathlibTest/Lint.lean index 4aef7f50c4099b..54f661c6cacea6 100644 --- a/MathlibTest/Lint.lean +++ b/MathlibTest/Lint.lean @@ -72,3 +72,111 @@ Note: This linter can be disabled with `set_option linter.style.nameCheck false` #guard_msgs in set_option linter.style.nameCheck true in theorem double__underscore : True := trivial + +/-- +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, 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, 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, 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, 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, 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 From 7b9915407c5cda0b207c898a23a0e5593e9a6a0e Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 25 May 2026 23:13:15 +0200 Subject: [PATCH 04/27] Review comments: - update documentation (including an outdated comment about auto-generated names; there is now a test which verifies this is false), - print multiple namespaces more nicely, - inline duplicate checking: List.Nodup is currently quadratic; let's avoid an additional pass over the full list. It is slightly less readable, but perhaps the performance difference is worth it... --- Mathlib/Tactic/Linter/Lint.lean | 37 ++++++++++++++++++--------------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 121f117161360e..7c783aa4f05a80 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -64,21 +64,21 @@ 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 declaration name's component is repeated +several times. This includes consecutive repetitions (such as, `Nat.Nat.foo` and `One.two.two`), +but is not limited to them: for example, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo` and +`Nat.Prime.Nat.bar` would all trigger a warning. -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 declaration name's component is repeated +several times. This includes consecutive repetitions (such as, `Nat.Nat.foo` and `One.two.two`), +but is not limited to them: for example, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo` and +`Nat.Prime.Nat.bar` would all trigger a warning. -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 @@ -99,14 +99,17 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do let declName := id.getId if declName.hasMacroScopes || isPrivateName declName then continue let nm := declName.components - if !nm.Nodup then - -- There are duplicate naming components: find the longest substring of duplicate - -- component(s). - let duplicated := List.pwFilter (· ≠ ·) <| nm.filter (fun comp ↦ nm.count comp > 1) - let msg := if let [ns] := duplicated then + -- Collect distinct components which appear more than once. + let duplicated := List.pwFilter (· ≠ ·) <| 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 `{declName}`" - else m!"The namespaces `{duplicated}` are duplicated in the declaration `{declName}`" - Linter.logLint linter.dupNamespace id msg + | dup => + let ns := MessageData.joinSep (duplicated.map (m!"{·}")) ", " + Linter.logLint linter.dupNamespace id + m!"The namespaces `{ns}` are duplicated in the declaration `{declName}`" initialize addLinter dupNamespace From dcd8d372d0e0047e7c9d46467b13dc79d9784551 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 25 May 2026 23:17:27 +0200 Subject: [PATCH 05/27] Re-bless test --- MathlibTest/Lint.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/MathlibTest/Lint.lean b/MathlibTest/Lint.lean index 54f661c6cacea6..511d5843e083d5 100644 --- a/MathlibTest/Lint.lean +++ b/MathlibTest/Lint.lean @@ -117,7 +117,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Foo.baz : True := trivial /-- -warning: The namespaces `[Foo, Bar]` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz` +warning: The namespaces `Foo, Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz` Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ @@ -125,7 +125,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Foo.Bar.baz : True := trivial /-- -warning: The namespaces `[Foo, Baz]` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Baz.baz` +warning: The namespaces `Foo, 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` -/ @@ -133,7 +133,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Baz.Hoge.Foo.Baz.baz : True := trivial /-- -warning: The namespaces `[Foo, Bar]` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.baz` +warning: The namespaces `Foo, 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` -/ @@ -141,7 +141,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Baz.Hoge.Foo.Bar.baz : True := trivial /-- -warning: The namespaces `[Foo, Bar, Baz]` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.Baz.az` +warning: The namespaces `Foo, Bar, 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` -/ @@ -151,7 +151,7 @@ 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, Bar]` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz'` +warning: The namespaces `Foo, Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz'` Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ From f062e83c308b0a8c28de143cefdadf38cdb5212f Mon Sep 17 00:00:00 2001 From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> Date: Thu, 28 May 2026 00:08:51 +0300 Subject: [PATCH 06/27] `set_option linter.dupNamespace false in` (#7) --- Mathlib/Algebra/Polynomial/Bivariate.lean | 2 ++ .../InnerProductSpace/JointEigenspace.lean | 1 + .../Bicategory/Adjunction/Adj.lean | 5 +++++ Mathlib/CategoryTheory/Groupoid/VertexGroup.lean | 2 ++ .../Subobject/Classifier/Defs.lean | 16 ++++++++++++++++ Mathlib/Data/Set/FiniteExhaustion.lean | 1 + .../Manifold/VectorBundle/MDifferentiable.lean | 1 + Mathlib/GroupTheory/Submonoid/Inverses.lean | 1 + Mathlib/LinearAlgebra/FreeModule/Basic.lean | 1 + Mathlib/Logic/Equiv/Set.lean | 1 + .../NumberField/Completion/FinitePlace.lean | 13 +++++++++++++ .../NumberField/InfinitePlace/Basic.lean | 1 + Mathlib/Order/Filter/Germ/Basic.lean | 1 + Mathlib/RingTheory/Etale/Basic.lean | 2 ++ Mathlib/RingTheory/Finiteness/Basic.lean | 1 + Mathlib/RingTheory/TensorProduct/Maps.lean | 1 + 16 files changed, 50 insertions(+) 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/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/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 4b00a7caea82ec..aef528c4b1d882 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 ac9b4aab75ccf4..d1e23023b7699c 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean @@ -322,6 +322,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 138daff2d913d2..f25113c7ec1660 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 a9df5a2c6bf8e4..e0e2777fdc4914 100644 --- a/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean +++ b/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean @@ -174,58 +174,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 8a5ba37de10e61..a27f77ba5c668f 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 7390a26c100c7e..e8a114e5d09fbe 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 e31cbc726bf1ad..de26be52b0949f 100644 --- a/Mathlib/RingTheory/Etale/Basic.lean +++ b/Mathlib/RingTheory/Etale/Basic.lean @@ -128,6 +128,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 @@ -140,6 +141,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 1044b0ae92511e..3e436d96da60f9 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 d1b56d3faa6a5e..6eb626e169cce2 100644 --- a/Mathlib/RingTheory/TensorProduct/Maps.lean +++ b/Mathlib/RingTheory/TensorProduct/Maps.lean @@ -413,6 +413,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 From 5aab66008d4d9fe847000a2e4269afdb6dec390f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 29 May 2026 19:39:43 +0200 Subject: [PATCH 07/27] Update Mathlib/Tactic/Linter/Lint.lean Co-authored-by: Jon Eugster --- Mathlib/Tactic/Linter/Lint.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 7c783aa4f05a80..74842525194d57 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -65,9 +65,8 @@ namespace Mathlib.Linter ### `dupNamespace` linter The `dupNamespace` linter produces a warning when a declaration name's component is repeated -several times. This includes consecutive repetitions (such as, `Nat.Nat.foo` and `One.two.two`), -but is not limited to them: for example, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo` and -`Nat.Prime.Nat.bar` would all trigger a warning. +several times. The repetition does not have to be consequitive. Examples: `Nat.Nat.foo`, +`One.two.two`, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo`, `Nat.Prime.Nat.bar` The linter also warns about auto-generated declarations (such as, those generated by `to_additive`). -/ From 9703215bcfbe0f443d864d83a52d9e5efb5a54ab Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 29 May 2026 19:42:12 +0200 Subject: [PATCH 08/27] Second comment; mirror change --- Mathlib/Tactic/Linter/Lint.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 74842525194d57..d8d148a0329f18 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -64,7 +64,7 @@ namespace Mathlib.Linter /-! ### `dupNamespace` linter -The `dupNamespace` linter produces a warning when a declaration name's component is repeated +The `dupNamespace` linter produces a warning when a component of a declaration name is repeated several times. The repetition does not have to be consequitive. Examples: `Nat.Nat.foo`, `One.two.two`, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo`, `Nat.Prime.Nat.bar` @@ -72,10 +72,9 @@ The linter also warns about auto-generated declarations (such as, those generate -/ /-- -The `dupNamespace` linter produces a warning when a declaration name's component is repeated -several times. This includes consecutive repetitions (such as, `Nat.Nat.foo` and `One.two.two`), -but is not limited to them: for example, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo` and -`Nat.Prime.Nat.bar` would all trigger a warning. +The `dupNamespace` linter produces a warning when a component of a declaration name is repeated +several times. The repetition does not have to be consequitive. Examples: `Nat.Nat.foo`, +`One.two.two`, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo`, `Nat.Prime.Nat.bar` The linter also warns about auto-generated declarations (such as, those generated by `to_additive`). -/ From 2e431f844d23b456ce0149dad0410430dbe2f101 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 29 May 2026 21:24:46 +0200 Subject: [PATCH 09/27] perf: asymptotically faster algorithm for duplicate components HashSet insertion is amortized O(1), so the new algorithm is amortized O(n) in the number of components. If this makes a difference? Let's see! --- Mathlib/Tactic/Linter/Lint.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index d8d148a0329f18..7794dc8de6f04f 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -98,7 +98,9 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do if declName.hasMacroScopes || isPrivateName declName then continue let nm := declName.components -- Collect distinct components which appear more than once. - let duplicated := List.pwFilter (· ≠ ·) <| nm.filter (fun comp ↦ nm.count comp > 1) + let (_, duplicated) : Std.HashSet Name × (Std.HashSet Name) := + nm.foldl (init := (∅, ∅)) fun (unique, dup) x ↦ + if x ∈ unique then (unique, dup.insert x) else (unique.insert x, dup) match duplicated with | [] => continue | [ns] => From 3bfec322225335e9a3c610f69121cae94dcb472d Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 30 May 2026 12:36:13 +0200 Subject: [PATCH 10/27] Fix --- Mathlib/Tactic/Linter/Lint.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 7794dc8de6f04f..0040cfb6126d1d 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -101,6 +101,7 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do let (_, duplicated) : Std.HashSet Name × (Std.HashSet Name) := nm.foldl (init := (∅, ∅)) fun (unique, dup) x ↦ if x ∈ unique then (unique, dup.insert x) else (unique.insert x, dup) + let duplicated := duplicated.toList match duplicated with | [] => continue | [ns] => From e4e55b8c08432f52d8821c2d9ae11bab83749ca5 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 2 Jun 2026 10:35:39 +0200 Subject: [PATCH 11/27] Test update: I think this is undesirable! --- MathlibTest/Lint.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/MathlibTest/Lint.lean b/MathlibTest/Lint.lean index 511d5843e083d5..7fddc1446931d6 100644 --- a/MathlibTest/Lint.lean +++ b/MathlibTest/Lint.lean @@ -117,7 +117,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Foo.baz : True := trivial /-- -warning: The namespaces `Foo, Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz` +warning: The namespaces `Bar, Foo` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz` Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ @@ -133,7 +133,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Baz.Hoge.Foo.Baz.baz : True := trivial /-- -warning: The namespaces `Foo, Bar` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.baz` +warning: The namespaces `Bar, Foo` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.baz` Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ @@ -141,7 +141,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Baz.Hoge.Foo.Bar.baz : True := trivial /-- -warning: The namespaces `Foo, Bar, Baz` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.Baz.az` +warning: The namespaces `Bar, Foo, 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` -/ @@ -151,7 +151,7 @@ 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, Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz'` +warning: The namespaces `Bar, Foo` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz'` Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ From 12165f745799a3f8a240401451f18b1ea40cdb6d Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 4 Jun 2026 10:28:16 +0200 Subject: [PATCH 12/27] fix(AlgebraicGeometry/Modules/Tilde): remove duplicate namespace The Scheme.Modules namespace was duplicated in the declaration. --- Mathlib/AlgebraicGeometry/Modules/Tilde.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean index a260233440f8f1..e981f97002609a 100644 --- a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean +++ b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean @@ -121,12 +121,12 @@ lemma isSMulRegular_of_le_basicOpen {f : R} (hle : U ≤ PrimeSpectrum.basicOpen set_option backward.isDefEq.respectTransparency false in @[simp] -lemma Scheme.Modules.restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S) +lemma restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S) [IsOpenImmersion (Spec.map f)] {U : (Spec S).Opens} (r : R) (x : Γ(M.restrict (Spec.map f), U)) : dsimp% (M.restrictAppIso (Spec.map f) U).hom (f r • x) = r • (M.restrictAppIso (Spec.map f) U).hom x := by - rw [Scheme.Modules.smul_Spec_def, Scheme.Modules.smul_Spec_def] + rw [smul_Spec_def, smul_Spec_def] simp_rw [smul_restrictAppIso_hom_apply, ← ConcreteCategory.comp_apply, Category.assoc] have : f ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.map U.leTop.op ≫ (Hom.appIso (Spec.map f) U).inv = @@ -134,6 +134,10 @@ lemma Scheme.Modules.restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S simp [Iso.cancel_iso_inv_left, Hom.app_eq_appLE] rfl rw [this] +set_option linter.dupNamespace false in + +@[deprecated (since := "2026-06-04")] +alias Scheme.Modules.restrictAppIso_smul_Spec := restrictAppIso_smul_Spec end Scheme.Modules From 641b6746fa40855362c015aa23937465068b4e23 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 4 Jun 2026 12:03:37 +0200 Subject: [PATCH 13/27] Revert to old code, let's re-bench --- Mathlib/Tactic/Linter/Lint.lean | 5 +---- MathlibTest/Lint.lean | 8 ++++---- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 0040cfb6126d1d..d8d148a0329f18 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -98,10 +98,7 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do if declName.hasMacroScopes || isPrivateName declName then continue let nm := declName.components -- Collect distinct components which appear more than once. - let (_, duplicated) : Std.HashSet Name × (Std.HashSet Name) := - nm.foldl (init := (∅, ∅)) fun (unique, dup) x ↦ - if x ∈ unique then (unique, dup.insert x) else (unique.insert x, dup) - let duplicated := duplicated.toList + let duplicated := List.pwFilter (· ≠ ·) <| nm.filter (fun comp ↦ nm.count comp > 1) match duplicated with | [] => continue | [ns] => diff --git a/MathlibTest/Lint.lean b/MathlibTest/Lint.lean index 7fddc1446931d6..511d5843e083d5 100644 --- a/MathlibTest/Lint.lean +++ b/MathlibTest/Lint.lean @@ -117,7 +117,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Foo.baz : True := trivial /-- -warning: The namespaces `Bar, Foo` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz` +warning: The namespaces `Foo, Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz` Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ @@ -133,7 +133,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Baz.Hoge.Foo.Baz.baz : True := trivial /-- -warning: The namespaces `Bar, Foo` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.baz` +warning: The namespaces `Foo, 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` -/ @@ -141,7 +141,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Baz.Hoge.Foo.Bar.baz : True := trivial /-- -warning: The namespaces `Bar, Foo, Baz` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.Baz.az` +warning: The namespaces `Foo, Bar, 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` -/ @@ -151,7 +151,7 @@ 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 `Bar, Foo` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz'` +warning: The namespaces `Foo, Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz'` Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ From 10fa137fae66eaedc121cc633cbd4ce719f56daa Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 8 Jun 2026 12:15:02 +0200 Subject: [PATCH 14/27] Fix --- Mathlib/AlgebraicGeometry/Modules/Tilde.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean index 6d1ecaf9f321ab..92eacec3e0c9e2 100644 --- a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean +++ b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean @@ -134,10 +134,6 @@ lemma restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S) simp [Iso.cancel_iso_inv_left, Hom.app_eq_appLE] rfl rw [this] -set_option linter.dupNamespace false in - -@[deprecated (since := "2026-06-04")] -alias Scheme.Modules.restrictAppIso_smul_Spec := restrictAppIso_smul_Spec set_option linter.dupNamespace false in @[deprecated (since := "2026-06-04")] From c1fbc3357d8a655e44fd1d4045367e26a343ff76 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 9 Jun 2026 10:52:00 +0200 Subject: [PATCH 15/27] Silence --- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean index ad9e9fe8731b55..c89b366ae7285f 100644 --- a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean +++ b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean @@ -453,6 +453,7 @@ instance : Monoid.FG (𝓞 K)ˣ := by theorem finrank_modTorsion : finrank ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) = rank K := by rw [← LinearEquiv.finrank_eq (logEmbeddingEquiv K).symm, unitLattice_rank] +set_option linter.dupNamespace false in @[deprecated (since := "2026-06-05")] alias NumberField.Units.rank_modTorsion := finrank_modTorsion From c329e58a4de658d33cec2dad7b1a34df576e64cb Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 10:55:17 +0200 Subject: [PATCH 16/27] Update Mathlib/Tactic/Linter/Lint.lean Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com> --- Mathlib/Tactic/Linter/Lint.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index d8d148a0329f18..8eed121385b3b3 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -103,11 +103,11 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do | [] => continue | [ns] => Linter.logLint linter.dupNamespace id - m!"The namespace `{ns}` is duplicated in the declaration `{declName}`" + m!"The namespace `{ns}` is duplicated in the declaration `{.ofConstName declName}`." | dup => - let ns := MessageData.joinSep (duplicated.map (m!"{·}")) ", " + let ns := MessageData.andList (duplicated.map (m!"`{·}`")) Linter.logLint linter.dupNamespace id - m!"The namespaces `{ns}` are duplicated in the declaration `{declName}`" + m!"The namespaces {ns} are duplicated in the declaration `{.ofConstName declName}`." initialize addLinter dupNamespace From 03b6026e3e34e286c1e54d10cbac118a8e9e6740 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 10:56:58 +0200 Subject: [PATCH 17/27] Update Mathlib/Tactic/Linter/Lint.lean Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com> --- Mathlib/Tactic/Linter/Lint.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 8eed121385b3b3..2043d5b7938cdc 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -95,7 +95,10 @@ 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 - if declName.hasMacroScopes || isPrivateName declName then continue + if + declName.hasMacroScopes || isPrivateName declName || Linter.isDeprecated (← getEnv) declName + then + continue let nm := declName.components -- Collect distinct components which appear more than once. let duplicated := List.pwFilter (· ≠ ·) <| nm.filter (fun comp ↦ nm.count comp > 1) From 37fa205180c2ba5554dbee780a6df4c9ee985950 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 11:02:23 +0200 Subject: [PATCH 18/27] chore: remove now-superfluous disabling of linter on deprecated declarations --- Mathlib/Algebra/Polynomial/Bivariate.lean | 2 -- Mathlib/AlgebraicGeometry/Modules/Tilde.lean | 1 - .../InnerProductSpace/JointEigenspace.lean | 1 - Mathlib/CategoryTheory/Groupoid/VertexGroup.lean | 2 -- .../Subobject/Classifier/Defs.lean | 16 ---------------- Mathlib/Data/Set/FiniteExhaustion.lean | 1 - .../Manifold/VectorBundle/MDifferentiable.lean | 1 - Mathlib/GroupTheory/Submonoid/Inverses.lean | 1 - Mathlib/LinearAlgebra/FreeModule/Basic.lean | 1 - Mathlib/Logic/Equiv/Set.lean | 1 - .../NumberField/Completion/FinitePlace.lean | 13 ------------- .../NumberField/InfinitePlace/Basic.lean | 1 - Mathlib/Order/Filter/Germ/Basic.lean | 1 - Mathlib/RingTheory/Etale/Basic.lean | 2 -- Mathlib/RingTheory/Finiteness/Basic.lean | 1 - Mathlib/RingTheory/TensorProduct/Maps.lean | 1 - Mathlib/Tactic/Linter/Lint.lean | 5 ++--- 17 files changed, 2 insertions(+), 49 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Bivariate.lean b/Mathlib/Algebra/Polynomial/Bivariate.lean index 19e5486a598d95..c2064ba46b87fb 100644 --- a/Mathlib/Algebra/Polynomial/Bivariate.lean +++ b/Mathlib/Algebra/Polynomial/Bivariate.lean @@ -353,7 +353,6 @@ 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 @@ -368,7 +367,6 @@ 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/AlgebraicGeometry/Modules/Tilde.lean b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean index 92eacec3e0c9e2..4a6ceba9acec82 100644 --- a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean +++ b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean @@ -135,7 +135,6 @@ lemma restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S) rfl rw [this] -set_option linter.dupNamespace false in @[deprecated (since := "2026-06-04")] alias Scheme.Modules.restrictAppIso_smul_Spec := restrictAppIso_smul_Spec diff --git a/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean b/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean index 97df41135bc48e..a2b446dbaae0ef 100644 --- a/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean +++ b/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean @@ -140,7 +140,6 @@ 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/Groupoid/VertexGroup.lean b/Mathlib/CategoryTheory/Groupoid/VertexGroup.lean index df6fd2c21367e8..289facce1b9efe 100644 --- a/Mathlib/CategoryTheory/Groupoid/VertexGroup.lean +++ b/Mathlib/CategoryTheory/Groupoid/VertexGroup.lean @@ -83,11 +83,9 @@ 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/Subobject/Classifier/Defs.lean b/Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean index bce43342532765..ce1187d910572b 100644 --- a/Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean +++ b/Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean @@ -392,7 +392,6 @@ 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")] @@ -404,7 +403,6 @@ 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")] @@ -416,7 +414,6 @@ 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_Ω₀ @@ -431,7 +428,6 @@ 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")] @@ -444,7 +440,6 @@ 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")] @@ -464,7 +459,6 @@ 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")] @@ -479,7 +473,6 @@ 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")] @@ -491,7 +484,6 @@ 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 @@ -499,7 +491,6 @@ 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 @@ -512,7 +503,6 @@ 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")] @@ -525,7 +515,6 @@ 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")] @@ -543,7 +532,6 @@ 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")] @@ -552,7 +540,6 @@ 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")] @@ -561,7 +548,6 @@ 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")] @@ -573,7 +559,6 @@ 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")] @@ -597,7 +582,6 @@ 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 10b3a9449870e0..1d9bd2db3e8194 100644 --- a/Mathlib/Data/Set/FiniteExhaustion.lean +++ b/Mathlib/Data/Set/FiniteExhaustion.lean @@ -80,7 +80,6 @@ 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 d1e23023b7699c..ac9b4aab75ccf4 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean @@ -322,7 +322,6 @@ 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 d4efa62017f0eb..847d5ddb31f104 100644 --- a/Mathlib/GroupTheory/Submonoid/Inverses.lean +++ b/Mathlib/GroupTheory/Submonoid/Inverses.lean @@ -56,7 +56,6 @@ 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 37d796cf745408..4e9d8b89e6b7bf 100644 --- a/Mathlib/LinearAlgebra/FreeModule/Basic.lean +++ b/Mathlib/LinearAlgebra/FreeModule/Basic.lean @@ -149,7 +149,6 @@ 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 b430f0e1e4d1cf..c1a73bf4892d9d 100644 --- a/Mathlib/Logic/Equiv/Set.lean +++ b/Mathlib/Logic/Equiv/Set.lean @@ -249,7 +249,6 @@ 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 32dfaa31d15c60..ff7e2f7603593e 100644 --- a/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean +++ b/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean @@ -175,71 +175,58 @@ 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 5f6e2279bcd393..d5ffa594968644 100644 --- a/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean @@ -309,7 +309,6 @@ 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 e8a114e5d09fbe..7390a26c100c7e 100644 --- a/Mathlib/Order/Filter/Germ/Basic.lean +++ b/Mathlib/Order/Filter/Germ/Basic.lean @@ -256,7 +256,6 @@ 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 c941952589073a..1277c23b518a03 100644 --- a/Mathlib/RingTheory/Etale/Basic.lean +++ b/Mathlib/RingTheory/Etale/Basic.lean @@ -130,7 +130,6 @@ 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 @@ -143,7 +142,6 @@ 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 3e436d96da60f9..1044b0ae92511e 100644 --- a/Mathlib/RingTheory/Finiteness/Basic.lean +++ b/Mathlib/RingTheory/Finiteness/Basic.lean @@ -324,7 +324,6 @@ 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 6eb626e169cce2..d1b56d3faa6a5e 100644 --- a/Mathlib/RingTheory/TensorProduct/Maps.lean +++ b/Mathlib/RingTheory/TensorProduct/Maps.lean @@ -413,7 +413,6 @@ 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 2043d5b7938cdc..d099b72e0b3c88 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -95,9 +95,8 @@ 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 - if - declName.hasMacroScopes || isPrivateName declName || Linter.isDeprecated (← getEnv) declName - then + if declName.hasMacroScopes || isPrivateName declName + || Linter.isDeprecated (← getEnv) declName then continue let nm := declName.components -- Collect distinct components which appear more than once. From 793f6dd14ef4802ce68a2c9a491ca4118881c66f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 11:06:46 +0200 Subject: [PATCH 19/27] chore: some test updates --- MathlibTest/Lint.lean | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/MathlibTest/Lint.lean b/MathlibTest/Lint.lean index 511d5843e083d5..8c1f5e3b833b61 100644 --- a/MathlibTest/Lint.lean +++ b/MathlibTest/Lint.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` -/ @@ -74,7 +74,7 @@ set_option linter.style.nameCheck true in theorem double__underscore : True := trivial /-- -warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo` +warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo`. Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ @@ -82,7 +82,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Foo : True := trivial /-- -warning: The namespace `Foo` is duplicated in the declaration `Bar.Foo.Foo` +warning: The namespace `Foo` is duplicated in the declaration `Bar.Foo.Foo`. Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ @@ -90,7 +90,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Bar.Foo.Foo : True := trivial /-- -warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo.Bar` +warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo.Bar`. Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ @@ -98,7 +98,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Foo.Bar : True := trivial /-- -warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo.Bar.Baz.hoge` +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` -/ @@ -109,7 +109,7 @@ lemma Foo.Foo.Bar.Baz.hoge : True := trivial lemma Foo.Foos.Bar.Baz : True := trivial /-- -warning: The namespace `Foo` is duplicated in the declaration `Foo.Bar.Foo.baz` +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` -/ @@ -117,7 +117,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Foo.baz : True := trivial /-- -warning: The namespaces `Foo, Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz` +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` -/ @@ -125,7 +125,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Foo.Bar.baz : True := trivial /-- -warning: The namespaces `Foo, Baz` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Baz.baz` +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` -/ @@ -133,7 +133,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Baz.Hoge.Foo.Baz.baz : True := trivial /-- -warning: The namespaces `Foo, Bar` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.baz` +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` -/ @@ -141,7 +141,7 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false` lemma Foo.Bar.Baz.Hoge.Foo.Bar.baz : True := trivial /-- -warning: The namespaces `Foo, Bar, Baz` are duplicated in the declaration `Foo.Bar.Baz.Hoge.Foo.Bar.Baz.az` +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` -/ @@ -151,7 +151,7 @@ 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, Bar` are duplicated in the declaration `Foo.Bar.Foo.Bar.baz'` +warning: The namespaces `Foo` and `Bar` are duplicated in the declaration `Foo.Bar.baz'`. Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ @@ -161,7 +161,7 @@ end Foo.Bar -- We detect additional generated names. /-- -warning: The namespace `AddSubgroup` is duplicated in the declaration `AddSubgroup.AddSubgroup.foo` +warning: The namespace `AddSubgroup` is duplicated in the declaration `AddSubgroup.AddSubgroup.foo`. Note: This linter can be disabled with `set_option linter.dupNamespace false` -/ @@ -173,7 +173,7 @@ def Subgroup.AddSubgroup.foo := 42 -- 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'` +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` -/ From 9fcf2a8cc5d8b9a36637b5dcb115d6274b0518f1 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 11:08:12 +0200 Subject: [PATCH 20/27] ahem, do lint deprecated declarations --- Mathlib/Tactic/Linter/Lint.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index d099b72e0b3c88..da95d1f55a22d1 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -95,9 +95,9 @@ 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 - if declName.hasMacroScopes || isPrivateName declName - || Linter.isDeprecated (← getEnv) declName then - continue + -- 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 -- Collect distinct components which appear more than once. let duplicated := List.pwFilter (· ≠ ·) <| nm.filter (fun comp ↦ nm.count comp > 1) @@ -105,7 +105,7 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do | [] => continue | [ns] => Linter.logLint linter.dupNamespace id - m!"The namespace `{ns}` is duplicated in the declaration `{.ofConstName declName}`." + m!"The namespace `{ns}` is duplicated in the declaration `{declName}`." -- .ofConstName | dup => let ns := MessageData.andList (duplicated.map (m!"`{·}`")) Linter.logLint linter.dupNamespace id From 200288b32902e6ab764614dd7ecbf43f48340353 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 11:08:50 +0200 Subject: [PATCH 21/27] Revert "chore: remove now-superfluous disabling of linter on deprecated declarations" This reverts commit 37fa205180c2ba5554dbee780a6df4c9ee985950. --- Mathlib/Algebra/Polynomial/Bivariate.lean | 2 ++ Mathlib/AlgebraicGeometry/Modules/Tilde.lean | 1 + .../InnerProductSpace/JointEigenspace.lean | 1 + Mathlib/CategoryTheory/Groupoid/VertexGroup.lean | 2 ++ .../Subobject/Classifier/Defs.lean | 16 ++++++++++++++++ Mathlib/Data/Set/FiniteExhaustion.lean | 1 + .../Manifold/VectorBundle/MDifferentiable.lean | 1 + Mathlib/GroupTheory/Submonoid/Inverses.lean | 1 + Mathlib/LinearAlgebra/FreeModule/Basic.lean | 1 + Mathlib/Logic/Equiv/Set.lean | 1 + .../NumberField/Completion/FinitePlace.lean | 13 +++++++++++++ .../NumberField/InfinitePlace/Basic.lean | 1 + Mathlib/Order/Filter/Germ/Basic.lean | 1 + Mathlib/RingTheory/Etale/Basic.lean | 2 ++ Mathlib/RingTheory/Finiteness/Basic.lean | 1 + Mathlib/RingTheory/TensorProduct/Maps.lean | 1 + 16 files changed, 46 insertions(+) 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/AlgebraicGeometry/Modules/Tilde.lean b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean index 4a6ceba9acec82..92eacec3e0c9e2 100644 --- a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean +++ b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean @@ -135,6 +135,7 @@ lemma restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S) rfl rw [this] +set_option linter.dupNamespace false in @[deprecated (since := "2026-06-04")] alias Scheme.Modules.restrictAppIso_smul_Spec := restrictAppIso_smul_Spec 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/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/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 ac9b4aab75ccf4..d1e23023b7699c 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean @@ -322,6 +322,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 7390a26c100c7e..e8a114e5d09fbe 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 1044b0ae92511e..3e436d96da60f9 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 d1b56d3faa6a5e..6eb626e169cce2 100644 --- a/Mathlib/RingTheory/TensorProduct/Maps.lean +++ b/Mathlib/RingTheory/TensorProduct/Maps.lean @@ -413,6 +413,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 From 90e3e935b45f70a585f4edfb27105dac1bd27c72 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 11:10:17 +0200 Subject: [PATCH 22/27] Don't use ofConstantName --- Mathlib/Tactic/Linter/Lint.lean | 8 ++++++-- MathlibTest/Lint.lean | 2 +- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index da95d1f55a22d1..c4f3d3aff3f909 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -104,12 +104,16 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do match duplicated with | [] => continue | [ns] => + -- Note: using `.ofConstName declName` would print only the visible name, whereas we prefer + -- the full path. Linter.logLint linter.dupNamespace id - m!"The namespace `{ns}` is duplicated in the declaration `{declName}`." -- .ofConstName + m!"The namespace `{ns}` is duplicated in the declaration `{declName}`." | dup => let ns := MessageData.andList (duplicated.map (m!"`{·}`")) + -- Note: using `.ofConstName declName` would print only the visible name, whereas we prefer + -- the full path. Linter.logLint linter.dupNamespace id - m!"The namespaces {ns} are duplicated in the declaration `{.ofConstName declName}`." + m!"The namespaces {ns} are duplicated in the declaration `{declName}`." initialize addLinter dupNamespace diff --git a/MathlibTest/Lint.lean b/MathlibTest/Lint.lean index 8c1f5e3b833b61..08bb5843e25c64 100644 --- a/MathlibTest/Lint.lean +++ b/MathlibTest/Lint.lean @@ -151,7 +151,7 @@ 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.baz'`. +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` -/ From 29bcf0ed392cfbaaf08f6b76ff800acdf3ba5b4f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 16:00:02 +0200 Subject: [PATCH 23/27] Add hovers --- Mathlib/Tactic/Linter/Lint.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index c4f3d3aff3f909..df587734ee9662 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -104,16 +104,14 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do match duplicated with | [] => continue | [ns] => - -- Note: using `.ofConstName declName` would print only the visible name, whereas we prefer - -- the full path. Linter.logLint linter.dupNamespace id - m!"The namespace `{ns}` is duplicated in the declaration `{declName}`." + m!"The namespace `{ns}` is duplicated in the declaration \ + `{.ofConstName (fullNames := true) declName}`." | dup => let ns := MessageData.andList (duplicated.map (m!"`{·}`")) - -- Note: using `.ofConstName declName` would print only the visible name, whereas we prefer - -- the full path. Linter.logLint linter.dupNamespace id - m!"The namespaces {ns} are duplicated in the declaration `{declName}`." + m!"The namespaces {ns} are duplicated in the declaration \ + `{.ofConstName (fullNames := true) declName}`." initialize addLinter dupNamespace From 9ec108431b917fee306e6cef91c40ebe190653fa Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 16:01:40 +0200 Subject: [PATCH 24/27] eraseDups --- Mathlib/Tactic/Linter/Lint.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index df587734ee9662..d1b7649aede9d0 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -11,8 +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 -public meta import Batteries.Data.List.Basic /-! # Linters for Mathlib @@ -100,7 +98,7 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do if declName.hasMacroScopes || isPrivateName declName then continue let nm := declName.components -- Collect distinct components which appear more than once. - let duplicated := List.pwFilter (· ≠ ·) <| nm.filter (fun comp ↦ nm.count comp > 1) + let duplicated := List.eraseDups <| nm.filter (fun comp ↦ nm.count comp > 1) match duplicated with | [] => continue | [ns] => From 72444dd52e5bb4f163f754c3dae10ee680342d99 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 17 Jun 2026 16:35:45 +0200 Subject: [PATCH 25/27] Apply suggestions from code review Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com> --- Mathlib/Tactic/Linter/Lint.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index d1b7649aede9d0..b46f67dd8ccc4a 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -63,7 +63,7 @@ namespace Mathlib.Linter ### `dupNamespace` linter The `dupNamespace` linter produces a warning when a component of a declaration name is repeated -several times. The repetition does not have to be consequitive. Examples: `Nat.Nat.foo`, +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` The linter also warns about auto-generated declarations (such as, those generated by `to_additive`). @@ -71,7 +71,7 @@ The linter also warns about auto-generated declarations (such as, those generate /-- The `dupNamespace` linter produces a warning when a component of a declaration name is repeated -several times. The repetition does not have to be consequitive. Examples: `Nat.Nat.foo`, +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` The linter also warns about auto-generated declarations (such as, those generated by `to_additive`). From 5f76901ca2e2b43f316c1374955890eaff319dcc Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 2 Jul 2026 00:50:43 +0200 Subject: [PATCH 26/27] chore(Analysis/Distribution/Support): fix deprecations The PR added deprecated aliases, but in a wrong namespace: this meant the original declarations did not actually get deprecated (and had in fact duplicated namespaces in their name). Fix the deprecation. As these landed just 24 hours ago, we don't deprecate the deprecations. Also update the deprecation date to when the PR was actually merged. --- Mathlib/Analysis/Distribution/Support.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 From 2e7d27597d27cd04a609c2539d4688d6e411569f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 2 Jul 2026 00:52:26 +0200 Subject: [PATCH 27/27] chore(CategoryTheory/Limits/Shapes/Pullback/HasPullback): fix deprecation The deprecation accidentally duplicated declaration namespaces, meaning it was never effective. This is confirmed by the declarations diff on the PR back then. Fix it. --- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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] :