restore

Mathlib/Data/ENNReal/Basic.lean

@@ -685,6 +685,33 @@ end OrdConnected
 
 end Set
 
+namespace Mathlib.Meta.Positivity
+
+open Lean Meta Qq
+
+/-- Extension for the `positivity` tactic: `ENNReal.toReal`. -/
+@[positivity ENNReal.toReal _]
+def evalENNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do
+  match u, α, e with
+  | 0, ~q(ℝ), ~q(ENNReal.toReal $a) =>
+    assertInstancesCommute
+    pure (.nonnegative q(ENNReal.toReal_nonneg))
+  | _, _, _ => throwError "not ENNReal.toReal"
+
+/-- Extension for the `positivity` tactic: `ENNReal.ofNNReal`. -/
+@[positivity ENNReal.ofNNReal _]
+def evalENNRealOfNNReal : PositivityExt where eval {u α} _zα _pα e := do
+  match u, α, e with
+  | 0, ~q(ℝ≥0∞), ~q(ENNReal.ofNNReal $a) =>
+    let ra ← core q(inferInstance) q(inferInstance) a
+    assertInstancesCommute
+    match ra with
+    | .positive pa => pure <| .positive q(ENNReal.coe_pos.mpr $pa)
+    | _ => pure .none
+  | _, _, _ => throwError "not ENNReal.ofNNReal"
+
+end Mathlib.Meta.Positivity
+
 @[deprecated (since := "2023-12-23")] protected alias
 ENNReal.le_inv_smul_iff_of_pos := le_inv_smul_iff_of_pos
 @[deprecated (since := "2023-12-23")] protected alias