feat(Tactic/Positivity): make positivity work for types that are not partial orders

Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

@@ -412,12 +412,13 @@ open Lean Meta Mathlib Meta Positivity Qq in
 For performance reasons, we only attempt to apply this when `abv` is a variable.
 If it is an explicit function, e.g. `|_|` or `‖_‖`, another extension should apply. -/
 @[positivity _]
-meta def Mathlib.Meta.Positivity.evalAbv : PositivityExt where eval {_ _α} _zα _pα e := do
+meta def Mathlib.Meta.Positivity.evalAbv : PositivityExt where eval {_ _α} _zα pα? e := do
+  let some pα := pα? | pure .none
   let (.app f a) ← whnfR e | throwError "not abv ·"
   if !f.getAppFn.isFVar then
     throwError "abv: function is not a variable"
   let pa' ← mkAppM ``abv_nonneg #[f, a]
-  pure (.nonnegative pa')
+  pure (.nonnegative (leα := q(($pα).toLE)) pa')
 
 lemma abv_eq_zero {x} : abv x = 0 ↔ x = 0 := abv_eq_zero'
 

Mathlib/Algebra/Order/Algebra.lean

@@ -89,7 +89,7 @@ open Lean Meta Qq Function
 @[positivity algebraMap _ _ _]
 meta def evalAlgebraMap : PositivityExt where eval {u β} _zβ _pβ e := do
   let ~q(@algebraMap $α _ $instα $instβ $instαβ $a) := e | throwError "not `algebraMap`"
-  let pα ← synthInstanceQ q(PartialOrder $α)
+  let pα ← try? <| synthInstanceQ q(PartialOrder $α)
   match ← core q(inferInstance) pα a with
   | .positive pa =>
     let _instαSemiring ← synthInstanceQ q(Semiring $α)

Mathlib/Algebra/Order/BigOperators/Expect.lean

@@ -183,7 +183,8 @@ open scoped BigOperators
 attribute [local instance] monadLiftOptionMetaM in
 /-- Positivity extension for `Finset.expect`. -/
 @[positivity Finset.expect _ _]
-meta def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do
+meta def evalFinsetExpect : PositivityExt where eval {u α} zα pα? e := do
+  let some pα := pα? | pure .none
   match e with
   | ~q(@Finset.expect $ι _ $instα $instmod $s $f) =>
     let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -287,7 +287,8 @@ example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.pro
 because `compareHyp` can't look for assumptions behind binders.
 -/
 @[positivity Finset.prod _ _]
-meta def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
+meta def evalFinsetProd : PositivityExt where eval {u α} zα pα? e := do
+  let some pα := pα? | pure .none
   match e with
   | ~q(@Finset.prod $ι _ $instα $s $f) =>
     let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque

Mathlib/Algebra/Order/Field/Basic.lean

@@ -728,47 +728,82 @@ lemma zpow_zero_pos {α : Type*} [Semifield α] [PartialOrder α] [IsStrictOrder
 
 /-- The `positivity` extension which identifies expressions of the form `a / b`,
 such that `positivity` successfully recognises both `a` and `b`. -/
-@[positivity _ / _] meta def evalDiv : PositivityExt where eval {u α} zα pα e := do
+@[positivity _ / _] meta def evalDiv : PositivityExt where eval {u α} zα pα? e := do
   let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
     | throwError "not /"
   let _e_eq : $e =Q $f $a $b := ⟨⟩
+  trace[Tactic.positivity.zeroness] "evalDiv: {a} divided by {b}"
+  let _a ← synthInstanceQ q(Semifield $α)
+  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HDiv.hDiv)
+  let some _ := pα? |
+    match ← core zα pα? a, ← core zα pα? b with
+    | .nonzero pa, .nonzero pb =>
+      let _a ← synthInstanceQ q(GroupWithZero $α)
+      assumeInstancesCommute
+      pure (.nonzero q(div_ne_zero $pa $pb))
+    | _, _ => pure .none
   let _a ← synthInstanceQ q(GroupWithZero $α)
-  let _a ← synthInstanceQ q(PartialOrder $α)
+  let pα' ← synthInstanceQ q(PartialOrder $α)
   let _a ← synthInstanceQ q(PosMulReflectLT $α)
   assumeInstancesCommute
-  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HDiv.hDiv)
-  let ra ← core zα pα a; let rb ← core zα pα b
+  let ra ← core zα pα? a; let rb ← core zα pα? b
   match ra, rb with
-  | .positive pa, .positive pb => pure (.positive q(div_pos $pa $pb))
-  | .positive pa, .nonnegative pb => pure (.nonnegative q(div_nonneg_of_pos_of_nonneg $pa $pb))
-  | .nonnegative pa, .positive pb => pure (.nonnegative q(div_nonneg_of_nonneg_of_pos $pa $pb))
-  | .nonnegative pa, .nonnegative pb => pure (.nonnegative q(div_nonneg $pa $pb))
-  | .positive pa, .nonzero pb => pure (.nonzero q(div_ne_zero_of_pos_of_ne_zero $pa $pb))
-  | .nonzero pa, .positive pb => pure (.nonzero q(div_ne_zero_of_ne_zero_of_pos $pa $pb))
+  | .positive (ltα := ltα) pa, .positive pb =>
+    haveI' : $ltα =Q ($pα').toLT := ⟨⟩
+    assumeInstancesCommute
+    pure (.positive q(div_pos $pa $pb))
+  | .positive pa, .nonnegative pb =>
+    assumeInstancesCommute
+    pure (.nonnegative q(div_nonneg_of_pos_of_nonneg $pa $pb))
+  | .nonnegative pa, .positive pb =>
+    assumeInstancesCommute
+    pure (.nonnegative q(div_nonneg_of_nonneg_of_pos $pa $pb))
+  | .nonnegative (leα := leα) pa, .nonnegative pb =>
+    haveI' : $leα =Q ($pα').toLE := ⟨⟩
+    assumeInstancesCommute
+    pure (.nonnegative q(div_nonneg $pa $pb))
+  | .positive pa, .nonzero pb =>
+    assumeInstancesCommute
+    pure (.nonzero q(div_ne_zero_of_pos_of_ne_zero $pa $pb))
+  | .nonzero pa, .positive pb =>
+    assumeInstancesCommute
+    pure (.nonzero q(div_ne_zero_of_ne_zero_of_pos $pa $pb))
   | .nonzero pa, .nonzero pb => pure (.nonzero q(div_ne_zero $pa $pb))
   | _, _ => pure .none
 
 /-- The `positivity` extension which identifies expressions of the form `a⁻¹`,
 such that `positivity` successfully recognises `a`. -/
 @[positivity _⁻¹]
-meta def evalInv : PositivityExt where eval {u α} zα pα e := do
+meta def evalInv : PositivityExt where eval {u α} zα pα? e := do
   let .app (f : Q($α → $α)) (a : Q($α)) ← withReducible (whnf e) | throwError "not ⁻¹"
   let _e_eq : $e =Q $f $a := ⟨⟩
+  let _a ← synthInstanceQ q(Semifield $α)
+  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(Inv.inv)
+  let some _ := pα? |
+    match ← core zα pα? a with
+    | .nonzero pa =>
+      let _a ← synthInstanceQ q(GroupWithZero $α)
+      assumeInstancesCommute
+      pure (.nonzero q(inv_ne_zero $pa))
+    | _ => pure .none
   let _a ← synthInstanceQ q(GroupWithZero $α)
   let _a ← synthInstanceQ q(PartialOrder $α)
   let _a ← synthInstanceQ q(PosMulReflectLT $α)
   assumeInstancesCommute
-  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(Inv.inv)
-  let ra ← core zα pα a
+  let ra ← core zα pα? a
   match ra with
-  | .positive pa => pure (.positive q(inv_pos_of_pos $pa))
-  | .nonnegative pa => pure (.nonnegative q(inv_nonneg_of_nonneg $pa))
+  | .positive pa =>
+    assumeInstancesCommute
+    pure (.positive q(inv_pos_of_pos $pa))
+  | .nonnegative pa =>
+    assumeInstancesCommute
+    pure (.nonnegative q(inv_nonneg_of_nonneg $pa))
   | .nonzero pa => pure (.nonzero q(inv_ne_zero $pa))
   | .none => pure .none
 
 /-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℤ)`. -/
 @[positivity _ ^ (0 : ℤ), Pow.pow _ (0 : ℤ)]
-meta def evalPowZeroInt : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalPowZeroInt : PositivityExt where eval {u α} _zα _pα? e := do
   let .app (.app _ (a : Q($α))) _ ← withReducible (whnf e) | throwError "not ^"
   let _a ← synthInstanceQ q(Semifield $α)
   let _a ← synthInstanceQ q(LinearOrder $α)

Mathlib/Algebra/Order/Field/Power.lean

@@ -123,8 +123,16 @@ open Lean Meta Qq
 /-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℤ)`,
 such that `positivity` successfully recognises both `a` and `b`. -/
 @[positivity _ ^ (_ : ℤ), Pow.pow _ (_ : ℤ)]
-meta def evalZPow : PositivityExt where eval {u α} zα pα e := do
+meta def evalZPow : PositivityExt where eval {u α} zα pα? e := do
   let .app (.app _ (a : Q($α))) (b : Q(ℤ)) ← withReducible (whnf e) | throwError "not ^"
+  let some pα := pα? |
+    match ← core zα pα? a with
+    | .nonzero pa =>
+      let _a ← synthInstanceQ q(GroupWithZero $α)
+      assumeInstancesCommute
+      haveI' : $e =Q $a ^ $b := ⟨⟩
+      pure (.nonzero q(zpow_ne_zero $b $pa))
+    | _ => pure .none
   let result ← catchNone do
     let _a ← synthInstanceQ q(Field $α)
     let _a ← synthInstanceQ q(LinearOrder $α)
@@ -148,7 +156,7 @@ meta def evalZPow : PositivityExt where eval {u α} zα pα e := do
       pure (.nonnegative q(Even.zpow_nonneg (Even.add_self _) $a))
     | _ => throwError "not a ^ n where n is a literal or a negated literal"
   orElse result do
-    let ra ← core zα pα a
+    let ra ← core zα pα? a
     let ofNonneg (pa : Q(0 ≤ $a))
         (_oα : Q(Semifield $α)) (_oα : Q(LinearOrder $α)) (_oα : Q(IsStrictOrderedRing $α)) :
         MetaM (Strictness zα pα e) := do
@@ -174,6 +182,7 @@ meta def evalZPow : PositivityExt where eval {u α} zα pα e := do
         let sα ← synthInstanceQ q(Semifield $α)
         let oα ← synthInstanceQ q(LinearOrder $α)
         let iα ← synthInstanceQ q(IsStrictOrderedRing $α)
+        assumeInstancesCommute
         orElse (← catchNone (ofNonneg q(le_of_lt $pa) sα oα iα))
           (ofNonzero q(ne_of_gt $pa) q(inferInstance))
     | .nonnegative pa =>

Mathlib/Algebra/Order/Floor/Extended.lean

@@ -223,11 +223,11 @@ alias ⟨_, natCeil_pos⟩ := ENat.ceil_pos
 
 /-- Extension for the `positivity` tactic: `ENat.ceil` is positive if its input is. -/
 @[positivity ⌈_⌉ₑ]
-meta def evalENatCeil : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalENatCeil : PositivityExt where eval {u α} _zα _pα? e := do
   match u, α, e with
   | 0, ~q(ℕ∞), ~q(ENat.ceil $r) =>
     assertInstancesCommute
-    match ← core q(inferInstance) q(inferInstance) r with
+    match ← core q(inferInstance) (some q(inferInstance)) r with
     | .positive pr =>
       assertInstancesCommute
       pure (.positive q(natCeil_pos $pr))

Mathlib/Algebra/Order/Floor/Ring.lean

@@ -50,10 +50,10 @@ theorem int_floor_nonneg_of_pos [Ring α] [LinearOrder α] [FloorRing α] {a : 
 
 /-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is. -/
 @[positivity ⌊_⌋]
-meta def evalIntFloor : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalIntFloor : PositivityExt where eval {u α} _zα _pα? e := do
   match u, α, e with
   | 0, ~q(ℤ), ~q(@Int.floor $α' $ir $io $j $a) =>
-    match ← core q(inferInstance) q(inferInstance) a with
+    match ← core q(inferInstance) (some q(inferInstance)) a with
     | .positive pa =>
         assertInstancesCommute
         pure (.nonnegative q(int_floor_nonneg_of_pos (α := $α') $pa))
@@ -69,13 +69,13 @@ theorem nat_ceil_pos [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α}
 
 /-- Extension for the `positivity` tactic: `Nat.ceil` is positive if its input is. -/
 @[positivity ⌈_⌉₊]
-meta def evalNatCeil : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalNatCeil : PositivityExt where eval {u α} _zα _pα? e := do
   match u, α, e with
   | 0, ~q(ℕ), ~q(@Nat.ceil $α' $ir $io $j $a) =>
     let _i ← synthInstanceQ q(LinearOrder $α')
     let _i ← synthInstanceQ q(IsStrictOrderedRing $α')
     assertInstancesCommute
-    match ← core q(inferInstance) q(inferInstance) a with
+    match ← core q(inferInstance) (some q(inferInstance)) a with
     | .positive pa =>
       assertInstancesCommute
       pure (.positive q(nat_ceil_pos (α := $α') $pa))
@@ -87,10 +87,10 @@ theorem int_ceil_pos [Ring α] [LinearOrder α] [FloorRing α] {a : α} : 0 < a
 
 /-- Extension for the `positivity` tactic: `Int.ceil` is positive/nonnegative if its input is. -/
 @[positivity ⌈_⌉]
-meta def evalIntCeil : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalIntCeil : PositivityExt where eval {u α} _zα _pα? e := do
   match u, α, e with
   | 0, ~q(ℤ), ~q(@Int.ceil $α' $ir $io $j $a) =>
-    match ← core q(inferInstance) q(inferInstance) a with
+    match ← core q(inferInstance) (some q(inferInstance)) a with
     | .positive pa =>
         assertInstancesCommute
         pure (.positive q(int_ceil_pos (α := $α') $pa))

Mathlib/Algebra/Order/Module/Field.lean

@@ -103,28 +103,29 @@ end Module.IsTorsionFree
 
 /-- Positivity extension for scalar multiplication. -/
 @[positivity HSMul.hSMul _ _]
-meta def evalSMul : PositivityExt where eval {_u α} zα pα (e : Q($α)) := do
+meta def evalSMul : PositivityExt where eval {_u α} zα pα? (e : Q($α)) := do
+  let some pα := pα? | pure .none
   let .app (.app (.app (.app (.app (.app
         (.const ``HSMul.hSMul [u1, _, _]) (β : Q(Type u1))) _) _) _)
           (a : Q($β))) (b : Q($α)) ← whnfR e | throwError "failed to match hSMul"
   let zM : Q(Zero $β) ← synthInstanceQ q(Zero $β)
   let pM : Q(PartialOrder $β) ← synthInstanceQ q(PartialOrder $β)
   -- Using `q()` here would be impractical, as we would have to manually `synthInstanceQ` all the
   -- required typeclasses. Ideally we could tell `q()` to do this automatically.
-  match ← core zM pM a, ← core zα pα b with
+  match ← core zM pM a, ← core zα pα? b with
   | .positive pa, .positive pb =>
       try {
         let _hαβ : Q(SMul $β $α) ← synthInstanceQ q(SMul $β $α)
         let _hαβ : Q(PosSMulStrictMono $β $α) ← synthInstanceQ q(PosSMulStrictMono $β $α)
-        pure (.positive (← mkAppM ``smul_pos #[pa, pb]))
+        pure (.positive (ltα := q(($pα).toLT)) (← mkAppM ``smul_pos #[pa, pb]))
       } catch _ =>
-        pure (.nonnegative (← mkAppM ``smul_nonneg_of_pos_of_pos #[pa, pb]))
+        pure (.nonnegative (leα := q(($pα).toLE)) (← mkAppM ``smul_nonneg_of_pos_of_pos #[pa, pb]))
   | .positive pa, .nonnegative pb =>
-      pure (.nonnegative (← mkAppM ``smul_nonneg_of_pos_of_nonneg #[pa, pb]))
+      pure (.nonnegative (leα := q(($pα).toLE)) (← mkAppM ``smul_nonneg_of_pos_of_nonneg #[pa, pb]))
   | .nonnegative pa, .positive pb =>
-      pure (.nonnegative (← mkAppM ``smul_nonneg_of_nonneg_of_pos #[pa, pb]))
+      pure (.nonnegative (leα := q(($pα).toLE)) (← mkAppM ``smul_nonneg_of_nonneg_of_pos #[pa, pb]))
   | .nonnegative pa, .nonnegative pb =>
-      pure (.nonnegative (← mkAppM ``smul_nonneg #[pa, pb]))
+      pure (.nonnegative (leα := q(($pα).toLE)) (← mkAppM ``smul_nonneg #[pa, pb]))
   | .positive pa, .nonzero pb =>
       pure (.nonzero (← mkAppM ``smul_ne_zero_of_pos_of_ne_zero #[pa, pb]))
   | .nonzero pa, .positive pb =>

Mathlib/Analysis/Complex/Order.lean

@@ -145,17 +145,26 @@ meta def evalComplexOfReal : PositivityExt where eval {u α} _ _ e := do
   -- TODO: Can we avoid duplicating the code?
   match u, α, e with
   | 0, ~q(ℂ), ~q(Complex.ofReal $a) =>
-    assumeInstancesCommute
-    match ← core q(inferInstance) q(inferInstance) a with
-    | .positive pa => return .positive q(ofReal_pos $pa)
-    | .nonnegative pa => return .nonnegative q(ofReal_nonneg $pa)
-    | .nonzero pa => return .nonzero q(ofReal_ne_zero_of_ne_zero $pa)
+    match ← core q(inferInstance) (some q(inferInstance)) a with
+    | .positive pa =>
+      assumeInstancesCommute
+      return .positive q(ofReal_pos $pa)
+    | .nonnegative pa =>
+      assumeInstancesCommute
+      return .nonnegative q(ofReal_nonneg $pa)
+    | .nonzero pa =>
+      assumeInstancesCommute
+      return .nonzero q(ofReal_ne_zero_of_ne_zero $pa)
     | _ => return .none
   | 0, ~q(ℂ), ~q(Complex.ofReal $a) =>
     assumeInstancesCommute
-    match ← core q(inferInstance) q(inferInstance) a with
-    | .positive pa => return .positive q(ofReal_pos $pa)
-    | .nonnegative pa => return .nonnegative q(ofReal_nonneg $pa)
+    match ← core q(inferInstance) (some q(inferInstance)) a with
+    | .positive pa =>
+      assumeInstancesCommute
+      return .positive q(ofReal_pos $pa)
+    | .nonnegative pa =>
+      assumeInstancesCommute
+      return .nonnegative q(ofReal_nonneg $pa)
     | .nonzero pa => return .nonzero q(ofReal_ne_zero_of_ne_zero $pa)
     | _ => return .none
   | _, _ => throwError "not Complex.ofReal"

Mathlib/Analysis/SpecialFunctions/Bernstein.lean

@@ -80,10 +80,11 @@ open Lean Meta Qq Function
 
 /-- Extension of the `positivity` tactic for Bernstein polynomials: they are always non-negative. -/
 @[positivity DFunLike.coe (bernstein _ _) _]
-meta def evalBernstein : PositivityExt where eval {_ _} _zα _pα e := do
+meta def evalBernstein : PositivityExt where eval {_ _} _zα pα? e := do
+  let some pα := pα? | pure .none
   let .app (.app _coe (.app (.app _ n) ν)) x ← whnfR e | throwError "not bernstein polynomial"
   let p ← mkAppOptM ``bernstein_nonneg #[n, ν, x]
-  pure (.nonnegative p)
+  pure (.nonnegative (leα := q(($pα).toLE)) p)
 
 end Mathlib.Meta.Positivity
 

Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -488,7 +488,7 @@ open Lean.Meta Qq Mathlib.Meta.Positivity in
 meta def _root_.Mathlib.Meta.Positivity.evalGamma : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(ℝ), ~q(Gamma $a) =>
-    match ← core q(inferInstance) q(inferInstance) a with
+    match ← core q(inferInstance) (some q(inferInstance)) a with
     | .positive pa =>
       assertInstancesCommute
       pure (.positive q(Gamma_pos_of_pos $pa))

Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

@@ -1090,12 +1090,14 @@ meta def evalNNRealRpow : PositivityExt where eval {u α} _ _ e := do
     assertInstancesCommute
     pure (.positive q(NNReal.rpow_zero_pos $a))
   | 0, ~q(ℝ≥0), ~q($a ^ ($b : ℝ)) =>
-    let ra ← core q(inferInstance) q(inferInstance) a
-    assertInstancesCommute
+    let ra ← core q(inferInstance) (some q(inferInstance)) a
     match ra with
     | .positive pa =>
-        pure (.positive q(NNReal.rpow_pos $pa))
-    | _ => pure (.nonnegative q(zero_le $e))
+      assertInstancesCommute
+      pure (.positive q(NNReal.rpow_pos $pa))
+    | _ =>
+      assertInstancesCommute
+      pure (.nonnegative q(zero_le $e))
   | _, _, _ => throwError "not NNReal.rpow"
 
 private meta def isFiniteM? (x : Q(ℝ≥0∞)) : MetaM (Option Q($x ≠ (⊤ : ℝ≥0∞))) := do
@@ -1118,18 +1120,22 @@ meta def evalENNRealRpow : PositivityExt where eval {u α} _ _ e := do
     assertInstancesCommute
     pure (.positive q(ENNReal.rpow_zero_pos $a))
   | 0, ~q(ℝ≥0∞), ~q($a ^ ($b : ℝ)) =>
-    let ra ← core q(inferInstance) q(inferInstance) a
-    let rb ← catchNone <| core q(inferInstance) q(inferInstance) b
-    assertInstancesCommute
+    let ra ← core q(inferInstance) (some q(inferInstance)) a
+    let rb ← catchNone <| core q(inferInstance) (some q(inferInstance)) b
     match ra, rb with
     | .positive pa, .positive pb =>
-        pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa <| le_of_lt $pb))
+      assertInstancesCommute
+      pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa <| le_of_lt $pb))
     | .positive pa, .nonnegative pb =>
-        pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa $pb))
+      assertInstancesCommute
+      pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa $pb))
     | .positive pa, _ =>
-        let some ha ← isFiniteM? a | pure <| .nonnegative q(zero_le $e)
-        pure <| .positive q(ENNReal.rpow_pos $pa $ha)
-    | _, _ => pure <| .nonnegative q(zero_le $e)
+      assertInstancesCommute
+      let some ha ← isFiniteM? a | pure <| .nonnegative q(zero_le $e)
+      pure <| .positive q(ENNReal.rpow_pos $pa $ha)
+    | _, _ =>
+      assertInstancesCommute
+      pure <| .nonnegative q(zero_le $e)
   | _, _, _ => throwError "not ENNReal.rpow"
 
 end Mathlib.Meta.Positivity

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -384,13 +384,14 @@ the base is nonnegative and positive when the base is positive. -/
 meta def evalRpow : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(ℝ), ~q($a ^ ($b : ℝ)) =>
-    let ra ← core q(inferInstance) q(inferInstance) a
-    assertInstancesCommute
+    let ra ← core q(inferInstance) (some q(inferInstance)) a
     match ra with
     | .positive pa =>
-        pure (.positive q(Real.rpow_pos_of_pos $pa $b))
+      assertInstancesCommute
+      pure (.positive q(Real.rpow_pos_of_pos $pa $b))
     | .nonnegative pa =>
-        pure (.nonnegative q(Real.rpow_nonneg $pa $b))
+      assertInstancesCommute
+      pure (.nonnegative q(Real.rpow_nonneg $pa $b))
     | _ => pure .none
   | _, _, _ => throwError "not Real.rpow"