chore: remove unnecessary Mathlib.Meta.Positivity namespacing (#10343)

Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -594,13 +594,13 @@ lemma integral_rpow_mul_exp_neg_mul_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
   rw [← ofReal_cpow (le_of_lt ht), IsROrC.ofReal_mul]
   rfl
 
-open Lean.Meta Qq in
+open Lean.Meta Qq Mathlib.Meta.Positivity in
 /-- The `positivity` extension which identifies expressions of the form `Gamma a`. -/
 @[positivity Gamma (_ : ℝ)]
 def _root_.Mathlib.Meta.Positivity.evalGamma :
-    Mathlib.Meta.Positivity.PositivityExt where eval {_ _α} zα pα (e : Q(ℝ)) := do
+    PositivityExt where eval {_ _α} zα pα (e : Q(ℝ)) := do
   let ~q(Gamma $a) := e | throwError "failed to match on Gamma application"
-  match ← Mathlib.Meta.Positivity.core zα pα a with
+  match ← core zα pα a with
   | .positive (pa : Q(0 < $a)) =>
     pure (.positive (q(Gamma_pos_of_pos $pa) : Q(0 < $e)))
   | .nonnegative (pa : Q(0 ≤ $a)) =>

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -351,7 +351,7 @@ open Lean Meta Qq
 /-- Extension for the `positivity` tactic: exponentiation by a real number is positive (namely 1)
 when the exponent is zero. The other cases are done in `evalRpow`. -/
 @[positivity (_ : ℝ) ^ (0 : ℝ), Pow.pow (_ : ℝ) (0 : ℝ), Real.rpow (_ : ℝ) (0 : ℝ)]
-def evalRpowZero : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ e := do
+def evalRpowZero : PositivityExt where eval {_ _} _ _ e := do
   let .app (.app (f : Q(ℝ → ℝ → ℝ)) (a : Q(ℝ))) (_ : Q(ℝ)) ← withReducible (whnf e)
     | throwError "not Real.rpow"
   guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(Real.rpow)
@@ -360,7 +360,7 @@ def evalRpowZero : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ e
 /-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when
 the base is nonnegative and positive when the base is positive. -/
 @[positivity (_ : ℝ) ^ (_ : ℝ), Pow.pow (_ : ℝ) (_ : ℝ), Real.rpow (_ : ℝ) (_ : ℝ)]
-def evalRpow : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} zα pα e := do
+def evalRpow : PositivityExt where eval {_ _} zα pα e := do
   let .app (.app (f : Q(ℝ → ℝ → ℝ)) (a : Q(ℝ))) (b : Q(ℝ)) ← withReducible (whnf e)
     | throwError "not Real.rpow"
   guard <| ← withDefault <| withNewMCtxDepth <| isDefEq f q(Real.rpow)

Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

@@ -182,7 +182,7 @@ open Lean.Meta Qq
 
 /-- Extension for the `positivity` tactic: `π` is always positive. -/
 @[positivity Real.pi]
-def evalRealPi : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ _ := do
+def evalRealPi : PositivityExt where eval {_ _} _ _ _ := do
   pure (.positive (q(Real.pi_pos) : Lean.Expr))
 
 end Mathlib.Meta.Positivity

Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -267,24 +267,24 @@ theorem add_div_le_sum_sq_div_card (hst : s ⊆ t) (f : ι → 𝕜) (d : 𝕜)
 
 end SzemerediRegularity
 
-namespace Tactic
+namespace Mathlib.Meta.Positivity
 
 open Lean.Meta Qq
 
 /-- Extension for the `positivity` tactic: `SzemerediRegularity.initialBound` is always positive. -/
 @[positivity SzemerediRegularity.initialBound _ _]
-def evalInitialBound : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ e := do
+def evalInitialBound : PositivityExt where eval {_ _} _ _ e := do
   let (.app (.app _ (ε : Q(ℝ))) (l : Q(ℕ))) ← whnfR e | throwError "not initialBound"
   pure (.positive (q(SzemerediRegularity.initialBound_pos $ε $l) : Lean.Expr))
 
 example (ε : ℝ) (l : ℕ) : 0 < SzemerediRegularity.initialBound ε l := by positivity
 
 /-- Extension for the `positivity` tactic: `SzemerediRegularity.bound` is always positive. -/
 @[positivity SzemerediRegularity.bound _ _]
-def evalBound : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ e := do
+def evalBound : PositivityExt where eval {_ _} _ _ e := do
   let (.app (.app _ (ε : Q(ℝ))) (l : Q(ℕ))) ← whnfR e | throwError "not bound"
   pure (.positive (q(SzemerediRegularity.bound_pos $ε $l) : Lean.Expr))
 
 example (ε : ℝ) (l : ℕ) : 0 < SzemerediRegularity.bound ε l := by positivity
 
-end Tactic
+end Mathlib.Meta.Positivity