chore(Tactic/Linarith): put linarith declarations into Mathlib.Tactic namespace (#25955)

The `Name.isMetaProgramming` function is used to exclude lemmas from library search tactics. Thus, it is important that lemmas that are only meant for use in a tactic implementation have a name flagged by `Name.isMetaProgramming`. So, this PR renames everying in `Mathlib/Tactic/Linarith` to the namespace `Mathlib.Tactic.Linarith` (which previously was just `Linarith`)

Author: JovanGerb

Mathlib/Tactic/Linarith/Datatypes.lean

@@ -16,12 +16,12 @@ We split them into their own file.
 This file also contains a few convenient auxiliary functions.
 -/
 
-open Lean Elab Tactic Meta Qq Mathlib
+open Lean Elab Tactic Meta Qq
 
 initialize registerTraceClass `linarith
 initialize registerTraceClass `linarith.detail
 
-namespace Linarith
+namespace Mathlib.Tactic.Linarith
 
 /-- A shorthand for getting the types of a list of proofs terms, to trace. -/
 def linarithGetProofsMessage (l : List Expr) : MetaM MessageData := do
@@ -305,4 +305,4 @@ def mkSingleCompZeroOf (c : Nat) (h : Expr) : MetaM (Ineq × Expr) := do
     let e' ← mkAppM iq.toConstMulName #[h, ex]
     return (iq, e')
 
-end Linarith
+end Mathlib.Tactic.Linarith

Mathlib/Tactic/Linarith/Frontend.lean

@@ -131,10 +131,10 @@ linarith, nlinarith, lra, nra, Fourier-Motzkin, linear arithmetic, linear progra
 -/
 
 open Lean Elab Parser Tactic Meta
-open Batteries Mathlib
+open Batteries
 
 
-namespace Linarith
+namespace Mathlib.Tactic.Linarith
 
 /-! ### Config objects
 
@@ -487,3 +487,5 @@ elab_rules : tactic
 --   category   := doc_category.tactic,
 --   decl_names := [`tactic.interactive.nlinarith],
 --   tags       := ["arithmetic", "decision procedure", "finishing"] }
+
+end Mathlib.Tactic

Mathlib/Tactic/Linarith/Lemmas.lean

@@ -19,7 +19,7 @@ Those in the `Linarith` namespace should stay here.
 Those outside the `Linarith` namespace may be deleted as they are ported to mathlib4.
 -/
 
-namespace Linarith
+namespace Mathlib.Tactic.Linarith
 
 universe u
 theorem lt_irrefl {α : Type u} [Preorder α] {a : α} : ¬a < a := _root_.lt_irrefl a
@@ -90,7 +90,6 @@ theorem sub_neg_of_lt [IsOrderedRing α] {a b : α} : a < b → a - b < 0 :=
 
 end Ring
 
-open Mathlib in
 /-- Finds the name of a multiplicative lemma corresponding to an inequality strength. -/
 def _root_.Mathlib.Ineq.toConstMulName : Ineq → Lean.Name
   | .lt => ``mul_neg
@@ -112,14 +111,14 @@ lemma zero_mul_eq {α} {R : α → α → Prop} [Semiring α] {a b : α} (h : a
     a * b = 0 := by
   simp [h]
 
-end Linarith
+end Mathlib.Tactic.Linarith
 
 section
-open Function
--- These lemmas can be removed when their originals are ported.
 
+@[deprecated GT.gt.lt (since := "2025-06-16")]
 theorem lt_zero_of_zero_gt {α : Type*} [Zero α] [LT α] {a : α} (h : 0 > a) : a < 0 := h
 
+@[deprecated GE.ge.le (since := "2025-06-16")]
 theorem le_zero_of_zero_ge {α : Type*} [Zero α] [LE α] {a : α} (h : 0 ≥ a) : a ≤ 0 := h
 
 end

Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean

@@ -55,7 +55,7 @@ instance : SDiff (TreeSet α cmp) := ⟨TreeSet.sdiff⟩
 
 end Std.TreeSet
 
-namespace Linarith
+namespace Mathlib.Tactic.Linarith
 
 /-!
 ### Datatypes
@@ -361,4 +361,4 @@ def CertificateOracle.fourierMotzkin : CertificateOracle where
     | (Except.ok _) => failure
     | (Except.error contr) => return contr.src.flatten
 
-end Linarith
+end Mathlib.Tactic.Linarith

Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean

@@ -14,8 +14,7 @@ The algorithm's entry point is the function `Linarith.SimplexAlgorithm.findPosit
 See the file `PositiveVector.lean` for details of how the procedure works.
 -/
 
-namespace Linarith.SimplexAlgorithm
-open Mathlib
+namespace Mathlib.Tactic.Linarith.SimplexAlgorithm
 
 /-- Preprocess the goal to pass it to `Linarith.SimplexAlgorithm.findPositiveVector`. -/
 def preprocess (matType : ℕ → ℕ → Type) [UsableInSimplexAlgorithm matType] (hyps : List Comp)
@@ -56,4 +55,4 @@ def CertificateOracle.simplexAlgorithmDense : CertificateOracle where
     let vec ← findPositiveVector A strictIndexes
     return postprocess vec
 
-end Linarith
+end Mathlib.Tactic.Linarith

Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean

@@ -11,7 +11,7 @@ import Std.Data.HashMap.Basic
 # Datatypes for the Simplex Algorithm implementation
 -/
 
-namespace Linarith.SimplexAlgorithm
+namespace Mathlib.Tactic.Linarith.SimplexAlgorithm
 
 /--
 Specification for matrix types over ℚ which can be used in the Gauss Elimination and the Simplex
@@ -126,4 +126,4 @@ structure Tableau (matType : Nat → Nat → Type) [UsableInSimplexAlgorithm mat
   /-- Matrix of coefficients the basic variables expressed through the free ones. -/
   mat : matType basic.size free.size
 
-end Linarith.SimplexAlgorithm
+end Mathlib.Tactic.Linarith.SimplexAlgorithm

Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Gauss.lean

@@ -12,7 +12,7 @@ The first step of `Linarith.SimplexAlgorithm.findPositiveVector` is finding init
 solution which is done by standard Gaussian Elimination algorithm implemented in this file.
 -/
 
-namespace Linarith.SimplexAlgorithm.Gauss
+namespace Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss
 
 /-- The monad for the Gaussian Elimination algorithm. -/
 abbrev GaussM (n m : Nat) (matType : Nat → Nat → Type) := StateT (matType n m) Lean.CoreM
@@ -78,4 +78,4 @@ ones.
 def getTableau (A : matType n m) : Lean.CoreM (Tableau matType) := do
   return (← getTableauImp.run A).fst
 
-end Linarith.SimplexAlgorithm.Gauss
+end Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss

Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/PositiveVector.lean

@@ -33,7 +33,7 @@ The function `findPositiveVector` solves this problem.
 
 -/
 
-namespace Linarith.SimplexAlgorithm
+namespace Mathlib.Tactic.Linarith.SimplexAlgorithm
 
 variable {matType : Nat → Nat → Type} [UsableInSimplexAlgorithm matType]
 
@@ -99,6 +99,4 @@ def findPositiveVector {n m : Nat} {matType : Nat → Nat → Type} [UsableInSim
   else
     throwError "Simplex Algorithm failed"
 
-end SimplexAlgorithm
-
-end Linarith
+end Mathlib.Tactic.Linarith.SimplexAlgorithm

Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/SimplexAlgorithm.lean

@@ -12,7 +12,7 @@ To obtain required vector in `Linarith.SimplexAlgorithm.findPositiveVector` we r
 Algorithm. We use Bland's rule for pivoting, which guarantees that the algorithm terminates.
 -/
 
-namespace Linarith.SimplexAlgorithm
+namespace Mathlib.Tactic.Linarith.SimplexAlgorithm
 
 /-- An exception in the `SimplexAlgorithmM` monad. -/
 inductive SimplexAlgorithmException
@@ -120,4 +120,4 @@ def runSimplexAlgorithm : SimplexAlgorithmM matType Unit := do
     let ⟨exitIdx, enterIdx⟩ ← choosePivots
     doPivotOperation exitIdx enterIdx
 
-end Linarith.SimplexAlgorithm
+end Mathlib.Tactic.Linarith.SimplexAlgorithm

Mathlib/Tactic/Linarith/Parsing.lean

@@ -27,7 +27,6 @@ This is ultimately converted into a `Linexp` in the obvious way.
 `linearFormsAndMaxVar` is the main entry point into this file. Everything else is contained.
 -/
 
-open Mathlib.Ineq Batteries
 open Std (TreeMap)
 
 namespace Std.TreeMap
@@ -78,7 +77,7 @@ local instance {α β : Type*} {c : α → α → Ordering} [Add β] [Zero β] [
     Add (TreeMap α β c) where
   add := fun f g => (f.mergeWith (fun _ b b' => b + b') g).filter (fun _ b => b ≠ 0)
 
-namespace Linarith
+namespace Mathlib.Tactic.Linarith
 
 /-- A local abbreviation for `TreeMap` so we don't need to write `Ord.compare` each time. -/
 abbrev Map (α β) [Ord α] := TreeMap α β Ord.compare
@@ -268,4 +267,4 @@ def linearFormsAndMaxVar (red : TransparencyMode) (pfs : List Expr) :
   trace[linarith.detail] "monomial map: {map.toList.map fun ⟨k,v⟩ => (k.toList, v)}"
   return (l, map.size - 1)
 
-end Linarith
+end Mathlib.Tactic.Linarith