feat: add a positivity extension for Real.toNNReal (#31956)

Author: urkud

Mathlib/Data/NNReal/Defs.lean

@@ -908,6 +908,9 @@ theorem cast_natAbs_eq_nnabs_cast (n : ℤ) : (n.natAbs : ℝ≥0) = nnabs n :=
   ext
   rw [NNReal.coe_natCast, Nat.cast_natAbs, Real.coe_nnabs, Int.cast_abs]
 
+@[simp]
+theorem nnabs_pos {x : ℝ} : 0 < x.nnabs ↔ x ≠ 0 := by simp [← NNReal.coe_pos]
+
 /-- Every real number nonnegative or nonpositive, phrased using `ℝ≥0`. -/
 lemma nnreal_dichotomy (r : ℝ) : ∃ x : ℝ≥0, r = x ∨ r = -x := by
   obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by simpa using le_total ..
@@ -995,4 +998,28 @@ meta def evalNNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do
     | _ => pure (.nonnegative q(NNReal.coe_nonneg $a))
   | _, _, _ => throwError "not NNReal.toReal"
 
+/-- Extension for the `positivity` tactic: `Real.toNNReal. -/
+@[positivity Real.toNNReal _]
+meta def evalRealToNNReal : PositivityExt where eval {u α} _zα _pα e := do
+  match u, α, e with
+  | 0, ~q(ℝ≥0), ~q(Real.toNNReal $a) =>
+    assertInstancesCommute
+    match (← core q(inferInstance) q(inferInstance) a) with
+    | .positive pa => pure (.positive q(toNNReal_pos.mpr $pa))
+    | _ => failure
+  | _, _, _ => throwError "not Real.toNNReal"
+
+private alias ⟨_, nnabs_pos_of_pos⟩ := Real.nnabs_pos
+
+/-- Extension for the `positivity` tactic: `Real.nnabs. -/
+@[positivity Real.nnabs _]
+meta def evalRealNNAbs : PositivityExt where eval {u α} _zα _pα e := do
+  match u, α, e with
+  | 0, ~q(ℝ≥0), ~q(Real.nnabs $a) =>
+    assertInstancesCommute
+    match (← core q(inferInstance) q(inferInstance) a).toNonzero with
+    | some pa => pure (.positive q(nnabs_pos_of_pos $pa))
+    | _ => failure
+  | _, _, _ => throwError "not Real.nnabs"
+
 end Mathlib.Meta.Positivity

MathlibTest/positivity.lean

@@ -252,6 +252,19 @@ example (a b : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a.lcm b := by positivity
 example (a : ℕ) (ha : a ≠ 0) : 0 < a.sqrt := by positivity
 example (a : ℕ) (ha : a ≠ 0) : 0 < a.totient := by positivity
 
+section NNReal
+
+example (a : ℝ) (ha : 0 < a) : 0 < a.toNNReal := by positivity
+example (a : ℝ) : 0 ≤ a.toNNReal := by positivity
+example (a : ℝ) : 0 ≤ a.nnabs := by positivity
+example (a : ℝ) (ha : 0 < a) : 0 < a.nnabs := by positivity
+example (a : ℝ) (ha : a ≠ 0) : 0 < a.nnabs := by positivity
+example (a : ℝ≥0) (ha : 0 < a) : 0 < (a : ℝ) := by positivity
+example (a : ℝ≥0) (ha : a ≠ 0) : 0 < (a : ℝ) := by positivity
+example (a : ℝ≥0) : 0 ≤ (a : ℝ) := by positivity
+
+end NNReal
+
 section ENNReal
 
 variable {a b : ℝ≥0∞}