Commit 2026-02-13 16:28 7c1ce076

View on Github →

chore: add missing namespaces (#34631) I noticed that there is a global definition called slice, which causes ambiguity with Finset.slice. This PR improved the namespacedness of some tactic files. Really, we should have a linter against definitions in the root namespace in the Mathlib.Tactic and Mathlib.Meta folders.

Estimated changes

Modified Mathlib/Tactic/CategoryTheory/CategoryStar.lean

Modified Mathlib/Tactic/CategoryTheory/Elementwise.lean

added def Mathlib.Tactic.Elementwise.elementwiseExpr

added def Mathlib.Tactic.Elementwise.elementwiseThms

added theorem Mathlib.Tactic.Elementwise.forall_congr_forget_Type

added theorem Mathlib.Tactic.Elementwise.forget_hom_Type

added theorem Mathlib.Tactic.Elementwise.hom_elementwise

deleted def Tactic.Elementwise.elementwiseExpr

deleted def Tactic.Elementwise.elementwiseThms

deleted theorem Tactic.Elementwise.forall_congr_forget_Type

deleted theorem Tactic.Elementwise.forget_hom_Type

deleted theorem Tactic.Elementwise.hom_elementwise

Modified Mathlib/Tactic/CategoryTheory/Slice.lean

added def Mathlib.Tactic.Slice.evalSlice

deleted def evalSlice

Modified Mathlib/Tactic/CategoryTheory/ToApp.lean

deleted def CategoryTheory.catAppSimp

deleted def CategoryTheory.toAppExpr

deleted def CategoryTheory.toCatExpr

deleted def CategoryTheory.toNatTransExpr

deleted theorem CategoryTheory.toNatTrans_congr

added def Mathlib.Tactic.CategoryTheory.ToApp.catAppSimp

added def Mathlib.Tactic.CategoryTheory.ToApp.toAppExpr

added def Mathlib.Tactic.CategoryTheory.ToApp.toCatExpr

added def Mathlib.Tactic.CategoryTheory.ToApp.toNatTransExpr

added theorem Mathlib.Tactic.CategoryTheory.ToApp.toNatTrans_congr