feat(Mathlib/Tactic/Positivity/Basic): positivity extension for ℕ+(PNat) (#13229)

The positivity extention to prove the positivity of `ℕ+`(`PNat`):
```lean
example (n : ℕ+) : 0 < (↑n : ℕ) := by positivity
```

Author: Komyyy

Mathlib/Tactic/Positivity/Basic.lean

@@ -10,6 +10,7 @@ import Mathlib.Data.NNRat.Defs
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.Data.Nat.Factorial.Basic
 import Mathlib.Data.Rat.Order
+import Mathlib.Data.PNat.Defs
 import Mathlib.Tactic.Positivity.Core
 import Qq
 
@@ -404,6 +405,15 @@ def evalNatSucc : PositivityExt where eval {u α} _zα _pα e := do
     pure (.positive q(Nat.succ_pos $a))
   | _, _, _ => throwError "not Nat.succ"
 
+/-- Extension for `PNat.val`. -/
+@[positivity PNat.val _]
+def evalPNatVal : PositivityExt where eval {u α} _zα _pα e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(PNat.val $a) =>
+    assertInstancesCommute
+    pure (.positive q(PNat.pos $a))
+  | _, _, _ => throwError "not PNat.val"
+
 /-- Extension for `Nat.factorial`. -/
 @[positivity Nat.factorial _]
 def evalFactorial : PositivityExt where eval {u α} _ _ e := do

scripts/noshake.json

@@ -227,7 +227,8 @@
   ["Mathlib.Algebra.GroupPower.Order",
    "Mathlib.Algebra.Order.Group.PosPart",
    "Mathlib.Data.Int.CharZero",
-   "Mathlib.Data.Nat.Factorial.Basic"],
+   "Mathlib.Data.Nat.Factorial.Basic",
+   "Mathlib.Data.PNat.Defs"],
   "Mathlib.Tactic.NormNum.Ineq":
   ["Mathlib.Algebra.Order.Field.Defs", "Mathlib.Algebra.Order.Monoid.WithTop"],
   "Mathlib.Tactic.NormNum.BigOperators": ["Mathlib.Data.List.FinRange"],

test/positivity.lean

@@ -282,6 +282,7 @@ example : 0 ≤ max (-3 : ℤ) 5 := by positivity
 --   [OrderedSMul α β] {a : α} (ha : 0 < a) {b : β} (hb : 0 < b) : 0 ≤ a • b := by positivity
 
 example (n : ℕ) : 0 < n.succ := by positivity
+example (n : ℕ+) : 0 < (↑n : ℕ) := by positivity
 example (n : ℕ) : 0 < n ! := by positivity
 example (n k : ℕ) : 0 < (n+1).ascFactorial k := by positivity