diff --git a/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean b/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
index b7dfbc8deb7d90..95700ceee5112b 100644
--- a/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
+++ b/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'
 
diff --git a/Mathlib/Algebra/Order/Algebra.lean b/Mathlib/Algebra/Order/Algebra.lean
index 1f6a448200a966..03f9dbd593cd59 100644
--- a/Mathlib/Algebra/Order/Algebra.lean
+++ b/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 $α)
diff --git a/Mathlib/Algebra/Order/BigOperators/Expect.lean b/Mathlib/Algebra/Order/BigOperators/Expect.lean
index cad7cf5781f718..b2e9297b308c4c 100644
--- a/Mathlib/Algebra/Order/BigOperators/Expect.lean
+++ b/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
diff --git a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
index 68fa53bc6b2cd3..5f23b33072b0b7 100644
--- a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
+++ b/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
diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean
index 0cddfeabcbe72a..51e957fc981ad9 100644
--- a/Mathlib/Algebra/Order/Field/Basic.lean
+++ b/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 $α)
diff --git a/Mathlib/Algebra/Order/Field/Power.lean b/Mathlib/Algebra/Order/Field/Power.lean
index 8f888e8a9c5c2a..8812c66d6bf171 100644
--- a/Mathlib/Algebra/Order/Field/Power.lean
+++ b/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 =>
diff --git a/Mathlib/Algebra/Order/Floor/Extended.lean b/Mathlib/Algebra/Order/Floor/Extended.lean
index 605abafb126422..92ba3d6f074821 100644
--- a/Mathlib/Algebra/Order/Floor/Extended.lean
+++ b/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))
diff --git a/Mathlib/Algebra/Order/Floor/Ring.lean b/Mathlib/Algebra/Order/Floor/Ring.lean
index 520d5130ac73ae..16c46aade5a5b0 100644
--- a/Mathlib/Algebra/Order/Floor/Ring.lean
+++ b/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))
diff --git a/Mathlib/Algebra/Order/Module/Field.lean b/Mathlib/Algebra/Order/Module/Field.lean
index 9e248fcace8a25..bc5b10c1ecc0ac 100644
--- a/Mathlib/Algebra/Order/Module/Field.lean
+++ b/Mathlib/Algebra/Order/Module/Field.lean
@@ -103,7 +103,8 @@ 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"
@@ -111,20 +112,20 @@ meta def evalSMul : PositivityExt where eval {_u α} zα pα (e : Q($α)) := do
   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 =>
diff --git a/Mathlib/Analysis/Complex/Order.lean b/Mathlib/Analysis/Complex/Order.lean
index ae4a7d8890b991..04f148e04571be 100644
--- a/Mathlib/Analysis/Complex/Order.lean
+++ b/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"
diff --git a/Mathlib/Analysis/SpecialFunctions/Bernstein.lean b/Mathlib/Analysis/SpecialFunctions/Bernstein.lean
index 54784039bfc4f9..08d7514bd0286b 100644
--- a/Mathlib/Analysis/SpecialFunctions/Bernstein.lean
+++ b/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
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
index e7796a6658bcc4..947e6d3d0ed2d5 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
+++ b/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))
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
index ad3e5809d2230b..6195f84192c908 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
+++ b/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
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
index dae7954a4f79a0..3d51c4fc18386c 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
+++ b/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"
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
index 3aa15a92e4cb0e..0ceab8777ff0aa 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
@@ -411,11 +411,16 @@ meta def evalRealArctan : PositivityExt where eval {u α} z p e := do
   match u, α, e with
   | 0, ~q(ℝ), ~q(Real.arctan $a) =>
     let ra ← core z p a
-    assumeInstancesCommute
     match ra with
-    | .positive pa => return .positive q(Real.arctan_pos.mpr $pa)
-    | .nonnegative na => return .nonnegative q(Real.arctan_nonneg.mpr $na)
-    | .nonzero na => return .nonzero q(mt Real.arctan_eq_zero_iff.mp $na)
+    | .positive pa =>
+      assumeInstancesCommute
+      return .positive q(Real.arctan_pos.mpr $pa)
+    | .nonnegative na =>
+      assumeInstancesCommute
+      return .nonnegative q(Real.arctan_nonneg.mpr $na)
+    | .nonzero na =>
+      assumeInstancesCommute
+      return .nonzero q(mt Real.arctan_eq_zero_iff.mp $na)
     | .none => return .none
   | _ => throwError "not Real.arctan"
 
@@ -433,11 +438,16 @@ meta def evalRealCosArctan : PositivityExt where eval {u α} _ _ e := do
 meta def evalRealSinArctan : PositivityExt where eval {u α} z p e := do
   match u, α, e with
   | 0, ~q(ℝ), ~q(Real.sin (Real.arctan $a)) =>
-    assumeInstancesCommute
     match ← core z p a with
-    | .positive pa => return .positive q(Real.sin_arctan_pos.mpr $pa)
-    | .nonnegative na => return .nonnegative q(Real.sin_arctan_nonneg.mpr $na)
-    | .nonzero na => return .nonzero q(mt Real.sin_arctan_eq_zero.mp $na)
+    | .positive pa =>
+      assumeInstancesCommute
+      return .positive q(Real.sin_arctan_pos.mpr $pa)
+    | .nonnegative na =>
+      assumeInstancesCommute
+      return .nonnegative q(Real.sin_arctan_nonneg.mpr $na)
+    | .nonzero na =>
+      assumeInstancesCommute
+      return .nonzero q(mt Real.sin_arctan_eq_zero.mp $na)
     | .none => return .none
   | _ => throwError "not Real.sin (Real.arctan _)"
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/DerivHyp.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/DerivHyp.lean
index 3c1dd210ba1950..12bb7654cf94db 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/DerivHyp.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/DerivHyp.lean
@@ -803,11 +803,16 @@ meta def evalSinh : PositivityExt where eval {u α} _ _ e := do
   let pα : Q(PartialOrder ℝ) := q(inferInstance)
   match u, α, e with
   | 0, ~q(ℝ), ~q(Real.sinh $a) =>
-    assumeInstancesCommute
     match ← core zα pα a with
-    | .positive pa => return .positive q(sinh_pos_of_pos $pa)
-    | .nonnegative pa => return .nonnegative q(sinh_nonneg_of_nonneg $pa)
-    | .nonzero pa => return .nonzero q(sinh_ne_zero_of_ne_zero $pa)
+    | .positive pa =>
+      assumeInstancesCommute
+      return .positive q(sinh_pos_of_pos $pa)
+    | .nonnegative pa =>
+      assumeInstancesCommute
+      return .nonnegative q(sinh_nonneg_of_nonneg $pa)
+    | .nonzero pa =>
+      assumeInstancesCommute
+      return .nonzero q(sinh_ne_zero_of_ne_zero $pa)
     | _ => return .none
   | _, _, _ => throwError "not Real.sinh"
 
diff --git a/Mathlib/Combinatorics/Enumerative/DyckWord.lean b/Mathlib/Combinatorics/Enumerative/DyckWord.lean
index 7e5508cbd0a109..ece67885a3a941 100644
--- a/Mathlib/Combinatorics/Enumerative/DyckWord.lean
+++ b/Mathlib/Combinatorics/Enumerative/DyckWord.lean
@@ -558,14 +558,17 @@ open Lean Meta Qq
 
 /-- Extension for the `positivity` tactic: `p.firstReturn` is positive if `p` is nonzero. -/
 @[positivity DyckWord.firstReturn _]
-meta def evalDyckWordFirstReturn : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalDyckWordFirstReturn : PositivityExt where eval {u α} _zα _pα? e := do
   match u, α, e with
   | 0, ~q(ℕ), ~q(DyckWord.firstReturn $a) =>
-    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(DyckWord.firstReturn_pos ($pa).ne'))
-    | .nonzero pa => pure (.positive q(DyckWord.firstReturn_pos $pa))
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(DyckWord.firstReturn_pos ($pa).ne'))
+    | .nonzero pa =>
+      assertInstancesCommute
+      pure (.positive q(DyckWord.firstReturn_pos $pa))
     | _ => pure .none
   | _, _, _ => throwError "not DyckWord.firstReturn"
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
index bdf4f169a854ea..86a30849128f1d 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
@@ -179,7 +179,7 @@ This exploits the positivity of the junk value of `triangleRemovalBound ε` for
 meta def evalTriangleRemovalBound : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(ℝ), ~q(triangleRemovalBound $ε) =>
-    let .positive hε ← core q(inferInstance) q(inferInstance) ε | failure
+    let .positive hε ← core q(inferInstance) (some q(inferInstance)) ε | failure
     assertInstancesCommute
     pure (.positive q(triangleRemovalBound_pos $hε))
   | _, _, _ => throwError "failed to match on Int.ceil application"
diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean
index cf9180978d209d..f76aae177961ca 100644
--- a/Mathlib/Data/ENNReal/Basic.lean
+++ b/Mathlib/Data/ENNReal/Basic.lean
@@ -727,7 +727,7 @@ open Lean Meta Qq
 
 /-- Extension for the `positivity` tactic: `ENNReal.toReal`. -/
 @[positivity ENNReal.toReal _]
-meta def evalENNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalENNRealtoReal : PositivityExt where eval {u α} _zα _pα? e := do
   match u, α, e with
   | 0, ~q(ℝ), ~q(ENNReal.toReal $a) =>
     assertInstancesCommute
@@ -736,13 +736,14 @@ meta def evalENNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do
 
 /-- Extension for the `positivity` tactic: `ENNReal.ofNNReal`. -/
 @[positivity ENNReal.ofNNReal _]
-meta def evalENNRealOfNNReal : PositivityExt where eval {u α} _zα _pα e := do
+meta 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
+    let ra ← core q(inferInstance) (some q(inferInstance)) a
     match ra with
-    | .positive pa => pure <| .positive q(ENNReal.coe_pos.mpr $pa)
+    | .positive pa =>
+      assertInstancesCommute
+      pure <| .positive q(ENNReal.coe_pos.mpr $pa)
     | _ => pure .none
   | _, _, _ => throwError "not ENNReal.ofNNReal"
 
diff --git a/Mathlib/Data/ENNReal/Real.lean b/Mathlib/Data/ENNReal/Real.lean
index ff25304075645e..aa70e071cc4913 100644
--- a/Mathlib/Data/ENNReal/Real.lean
+++ b/Mathlib/Data/ENNReal/Real.lean
@@ -398,13 +398,14 @@ open Lean Meta Qq
 
 /-- Extension for the `positivity` tactic: `ENNReal.ofReal`. -/
 @[positivity ENNReal.ofReal _]
-meta def evalENNRealOfReal : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalENNRealOfReal : PositivityExt where eval {u α} _zα _pα? e := do
   match u, α, e with
   | 0, ~q(ℝ≥0∞), ~q(ENNReal.ofReal $a) =>
-    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(Iff.mpr (@ENNReal.ofReal_pos $a) $pa))
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(Iff.mpr (@ENNReal.ofReal_pos $a) $pa))
     | _ => pure .none
   | _, _, _ => throwError "not ENNReal.ofReal"
 end Mathlib.Meta.Positivity
diff --git a/Mathlib/Data/EReal/Basic.lean b/Mathlib/Data/EReal/Basic.lean
index 270b3d638eb935..efa6b0f8779299 100644
--- a/Mathlib/Data/EReal/Basic.lean
+++ b/Mathlib/Data/EReal/Basic.lean
@@ -856,12 +856,17 @@ open Lean Meta Qq Function
 meta def evalRealToEReal : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(EReal), ~q(Real.toEReal $a) =>
-    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(EReal.coe_pos.2 $pa))
-    | .nonnegative pa => pure (.nonnegative q(EReal.coe_nonneg.2 $pa))
-    | .nonzero pa => pure (.nonzero q(EReal.coe_ne_zero.2 $pa))
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(EReal.coe_pos.2 $pa))
+    | .nonnegative pa =>
+      assertInstancesCommute
+      pure (.nonnegative q(EReal.coe_nonneg.2 $pa))
+    | .nonzero pa =>
+      assertInstancesCommute
+      pure (.nonzero q(EReal.coe_ne_zero.2 $pa))
     | _ => pure .none
   | _, _, _ => throwError "not Real.toEReal"
 
@@ -870,12 +875,17 @@ meta def evalRealToEReal : PositivityExt where eval {u α} _zα _pα e := do
 meta def evalENNRealToEReal : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(EReal), ~q(ENNReal.toEReal $a) =>
-    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(EReal.coe_ennreal_pos.2 $pa))
-    | .nonzero pa => pure (.positive q(EReal.coe_ennreal_pos_iff_ne_zero.2 $pa))
-    | _ => pure (.nonnegative q(EReal.coe_ennreal_nonneg $a))
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(EReal.coe_ennreal_pos.2 $pa))
+    | .nonzero pa =>
+      assertInstancesCommute
+      pure (.positive q(EReal.coe_ennreal_pos_iff_ne_zero.2 $pa))
+    | _ =>
+      assertInstancesCommute
+      pure (.nonnegative q(EReal.coe_ennreal_nonneg $a))
   | _, _, _ => throwError "not ENNReal.toEReal"
 
 /-- Extension for the `positivity` tactic: projection from `EReal` to `ℝ`.
@@ -888,7 +898,7 @@ meta def evalERealToReal : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(Real), ~q(EReal.toReal $a) =>
     assertInstancesCommute
-    match (← core q(inferInstance) q(inferInstance) a).toNonneg with
+    match (← core q(inferInstance) (some q(inferInstance)) a).toNonneg with
     | .some pa => pure (.nonnegative q(EReal.toReal_nonneg $pa))
     | _ => pure .none
   | _, _, _ => throwError "not EReal.toReal"
@@ -903,10 +913,13 @@ We cannot deduce any corollaries from `x ≠ 0`, since `EReal.toENNReal x = 0` f
 meta def evalERealToENNReal : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(ENNReal), ~q(EReal.toENNReal $a) =>
-    assertInstancesCommute
-    match ← core q(inferInstance) q(inferInstance) a with
-    | .positive pa => pure (.positive q(EReal.toENNReal_pos_iff.2 $pa))
-    | _ => pure (.nonnegative q(zero_le $e))
+    match ← core q(inferInstance) (some q(inferInstance)) a with
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(EReal.toENNReal_pos_iff.2 $pa))
+    | _ =>
+      assertInstancesCommute
+      pure (.nonnegative q(zero_le $e))
   | _, _, _ => throwError "not EReal.toENNReal"
 
 end Mathlib.Meta.Positivity
diff --git a/Mathlib/Data/EReal/Inv.lean b/Mathlib/Data/EReal/Inv.lean
index 36cfae4282e3b4..c9feac33cbcd7b 100644
--- a/Mathlib/Data/EReal/Inv.lean
+++ b/Mathlib/Data/EReal/Inv.lean
@@ -551,24 +551,24 @@ open Lean Meta Qq Function
 
 /-- Extension for the `positivity` tactic: inverse of an `EReal`. -/
 @[positivity (_⁻¹ : EReal)]
-meta def evalERealInv : PositivityExt where eval {u α} zα pα e := do
+meta def evalERealInv : PositivityExt where eval {u α} _ _ e := do
   match u, α, e with
   | 0, ~q(EReal), ~q($a⁻¹) =>
     assertInstancesCommute
-    match (← core zα pα a).toNonneg with
+    match (← core q(inferInstance) (some q(inferInstance)) a).toNonneg with
     | some pa => pure (.nonnegative q(EReal.inv_nonneg_of_nonneg <| $pa))
     | none => pure .none
   | _, _, _ => throwError "not an inverse of an `EReal`"
 
 /-- Extension for the `positivity` tactic: ratio of two `EReal`s. -/
 @[positivity (_ / _ : EReal)]
-meta def evalERealDiv : PositivityExt where eval {u α} zα pα e := do
+meta def evalERealDiv : PositivityExt where eval {u α} _ _ e := do
   match u, α, e with
   | 0, ~q(EReal), ~q($a / $b) =>
     assertInstancesCommute
-    match (← core zα pα a).toNonneg with
+    match (← core q(inferInstance) (some q(inferInstance)) a).toNonneg with
     | some pa =>
-      match (← core zα pα b).toNonneg with
+      match (← core q(inferInstance) (some q(inferInstance)) b).toNonneg with
       | some pb => pure (.nonnegative q(EReal.div_nonneg $pa $pb))
       | none => pure .none
     | _ => pure .none
diff --git a/Mathlib/Data/EReal/Operations.lean b/Mathlib/Data/EReal/Operations.lean
index b6ac68dc15c3af..1cfe84b2f7b3c5 100644
--- a/Mathlib/Data/EReal/Operations.lean
+++ b/Mathlib/Data/EReal/Operations.lean
@@ -825,43 +825,61 @@ open Lean Meta Qq Function
 
 /-- Extension for the `positivity` tactic: sum of two `EReal`s. -/
 @[positivity (_ + _ : EReal)]
-meta def evalERealAdd : PositivityExt where eval {u α} zα pα e := do
+meta def evalERealAdd : PositivityExt where eval {u α} zα pα? e := do
+  let some pα := pα? | pure .none
   match u, α, e with
   | 0, ~q(EReal), ~q($a + $b) =>
-    assertInstancesCommute
     match ← core zα pα a with
     | .positive pa =>
       match (← core zα pα b).toNonneg with
-      | some pb => pure (.positive q(EReal.add_pos_of_pos_of_nonneg $pa $pb))
+      | some pb =>
+        assertInstancesCommute
+        pure (.positive q(EReal.add_pos_of_pos_of_nonneg $pa $pb))
       | _ => pure .none
     | .nonnegative pa =>
       match ← core zα pα b with
-      | .positive pb => pure (.positive q(Right.add_pos_of_nonneg_of_pos $pa $pb))
-      | .nonnegative pb => pure (.nonnegative q(add_nonneg $pa $pb))
+      | .positive pb =>
+        assertInstancesCommute
+        pure (.positive q(Right.add_pos_of_nonneg_of_pos $pa $pb))
+      | .nonnegative (leα := leα) pb =>
+        haveI' : $leα =Q ($pα).toLE := ⟨⟩
+        assertInstancesCommute
+        pure (.nonnegative q(add_nonneg $pa $pb))
       | _ => pure .none
     | _ => pure .none
   | _, _, _ => throwError "not a sum of 2 `EReal`s"
 
 /-- Extension for the `positivity` tactic: product of two `EReal`s. -/
 @[positivity (_ * _ : EReal)]
-meta def evalERealMul : PositivityExt where eval {u α} zα pα e := do
+meta def evalERealMul : PositivityExt where eval {u α} zα pα? e := do
+  let some pα := pα? | pure .none
   match u, α, e with
   | 0, ~q(EReal), ~q($a * $b) =>
-    assertInstancesCommute
     match ← core zα pα a with
     | .positive pa =>
       match ← core zα pα b with
-      | .positive pb => pure <| .positive q(EReal.mul_pos $pa $pb)
-      | .nonnegative pb => pure <| .nonnegative q(EReal.mul_nonneg (le_of_lt $pa) $pb)
-      | .nonzero pb => pure <| .nonzero q(mul_ne_zero (ne_of_gt $pa) $pb)
+      | .positive (ltα := ltα) pb =>
+        haveI' : $ltα =Q ($pα).toLT := ⟨⟩
+        assertInstancesCommute
+        pure <| .positive q(EReal.mul_pos $pa $pb)
+      | .nonnegative pb =>
+        assertInstancesCommute
+        pure <| .nonnegative q(EReal.mul_nonneg (le_of_lt $pa) $pb)
+      | .nonzero pb =>
+        assertInstancesCommute
+        pure <| .nonzero q(mul_ne_zero (ne_of_gt $pa) $pb)
       | _ => pure .none
     | .nonnegative pa =>
       match (← core zα pα b).toNonneg with
-      | some pb => pure (.nonnegative q(EReal.mul_nonneg $pa $pb))
+      | some pb =>
+        assertInstancesCommute
+        pure (.nonnegative q(EReal.mul_nonneg $pa $pb))
       | none => pure .none
     | .nonzero pa =>
       match (← core zα pα b).toNonzero with
-      | some pb => pure (.nonzero q(mul_ne_zero $pa $pb))
+      | some pb =>
+        assertInstancesCommute
+        pure (.nonzero q(mul_ne_zero $pa $pb))
       | none => pure .none
     | _ => pure .none
   | _, _, _ => throwError "not a product of 2 `EReal`s"
diff --git a/Mathlib/Data/NNReal/Defs.lean b/Mathlib/Data/NNReal/Defs.lean
index 916e999fa135f2..9601397aff997b 100644
--- a/Mathlib/Data/NNReal/Defs.lean
+++ b/Mathlib/Data/NNReal/Defs.lean
@@ -987,14 +987,17 @@ alias ⟨_, nnreal_coe_pos⟩ := coe_pos
 
 /-- Extension for the `positivity` tactic: cast from `ℝ≥0` to `ℝ`. -/
 @[positivity NNReal.toReal _]
-meta def evalNNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalNNRealtoReal : PositivityExt where eval {u α} _zα _pα? e := do
   match u, α, e with
   | 0, ~q(ℝ), ~q(NNReal.toReal $a) =>
-    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_coe_pos $pa))
-    | _ => pure (.nonnegative q(NNReal.coe_nonneg $a))
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(nnreal_coe_pos $pa))
+    | _ =>
+      assertInstancesCommute
+      pure (.nonnegative q(NNReal.coe_nonneg $a))
   | _, _, _ => throwError "not NNReal.toReal"
 
 /-- Extension for the `positivity` tactic: `Real.toNNReal` -/
@@ -1003,8 +1006,10 @@ 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))
+    match (← core q(inferInstance) (some q(inferInstance)) a) with
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(toNNReal_pos.mpr $pa))
     | _ => failure
   | _, _, _ => throwError "not Real.toNNReal"
 
@@ -1016,7 +1021,7 @@ 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
+    match (← core q(inferInstance) (some q(inferInstance)) a).toNonzero with
     | some pa => pure (.positive q(nnabs_pos_of_pos $pa))
     | _ => failure
   | _, _, _ => throwError "not Real.nnabs"
diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean
index e5b09ed35a3b25..e0ad3079825f97 100644
--- a/Mathlib/Data/Nat/Totient.lean
+++ b/Mathlib/Data/Nat/Totient.lean
@@ -448,9 +448,10 @@ open Lean Meta Qq
 meta def evalNatTotient : PositivityExt where eval {u α} z p e := do
   match u, α, e with
   | 0, ~q(ℕ), ~q(Nat.totient $n) =>
-    assumeInstancesCommute
     match ← core z p n with
-    | .positive pa => return .positive q(Nat.totient_pos.mpr $pa)
+    | .positive pa =>
+      assumeInstancesCommute
+      return .positive q(Nat.totient_pos.mpr $pa)
     | _ => failure
   | _, _, _ => throwError "not Nat.totient"
 
diff --git a/Mathlib/Data/Rat/Cast/Order.lean b/Mathlib/Data/Rat/Cast/Order.lean
index 76212c9c0f2df6..dec67caef1138e 100644
--- a/Mathlib/Data/Rat/Cast/Order.lean
+++ b/Mathlib/Data/Rat/Cast/Order.lean
@@ -260,9 +260,9 @@ open Lean Meta Qq Function
 
 /-- Extension for Rat.cast. -/
 @[positivity Rat.cast _]
-meta def evalRatCast : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalRatCast : PositivityExt where eval {u α} _zα _pα? e := do
   let ~q(@Rat.cast _ (_) ($a : ℚ)) := e | throwError "not Rat.cast"
-  match ← core q(inferInstance) q(inferInstance) a with
+  match ← core q(inferInstance) (some q(inferInstance)) a with
   | .positive pa =>
     let _oα ← synthInstanceQ q(Field $α)
     let _oα ← synthInstanceQ q(LinearOrder $α)
@@ -284,9 +284,9 @@ meta def evalRatCast : PositivityExt where eval {u α} _zα _pα e := do
 
 /-- Extension for NNRat.cast. -/
 @[positivity NNRat.cast _]
-meta def evalNNRatCast : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalNNRatCast : PositivityExt where eval {u α} _zα _pα? e := do
   let ~q(@NNRat.cast _ (_) ($a : ℚ≥0)) := e | throwError "not NNRat.cast"
-  match ← core q(inferInstance) q(inferInstance) a with
+  match ← core q(inferInstance) (some q(inferInstance)) a with
   | .positive pa =>
     let _oα ← synthInstanceQ q(Semifield $α)
     let _oα ← synthInstanceQ q(LinearOrder $α)
diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean
index 7adc89de310c12..eee272ad0f653a 100644
--- a/Mathlib/Data/Real/Sqrt.lean
+++ b/Mathlib/Data/Real/Sqrt.lean
@@ -309,13 +309,14 @@ open Lean Meta Qq Function
 /-- Extension for the `positivity` tactic: a square root of a strictly positive nonnegative real is
 positive. -/
 @[positivity NNReal.sqrt _]
-meta def evalNNRealSqrt : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalNNRealSqrt : PositivityExt where eval {u α} _zα _pα? e := do
   match u, α, e with
   | 0, ~q(NNReal), ~q(NNReal.sqrt $a) =>
-    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.sqrt_pos_of_pos $pa))
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(NNReal.sqrt_pos_of_pos $pa))
     | _ => failure -- this case is dealt with by generic nonnegativity of nnreals
   | _, _, _ => throwError "not NNReal.sqrt"
 
@@ -325,11 +326,14 @@ its input is. -/
 meta def evalSqrt : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(ℝ), ~q(√$a) =>
-    let ra ← catchNone <| core q(inferInstance) q(inferInstance) a
-    assertInstancesCommute
+    let ra ← catchNone <| core q(inferInstance) (some q(inferInstance)) a
     match ra with
-    | .positive pa => pure (.positive q(Real.sqrt_pos_of_pos $pa))
-    | _ => pure (.nonnegative q(Real.sqrt_nonneg $a))
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(Real.sqrt_pos_of_pos $pa))
+    | _ =>
+      assertInstancesCommute
+      pure (.nonnegative q(Real.sqrt_nonneg $a))
   | _, _, _ => throwError "not Real.sqrt"
 
 end Mathlib.Meta.Positivity
diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
index 3914f8693d3c79..508c4dfd5c13c2 100644
--- a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
+++ b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
@@ -1450,12 +1450,12 @@ attribute [local instance] monadLiftOptionMetaM in
 This extension only proves non-negativity, strict positivity is more delicate for integration and
 requires more assumptions. -/
 @[positivity MeasureTheory.integral _ _]
-meta def evalIntegral : PositivityExt where eval {u α} zα pα e := do
+meta def evalIntegral : PositivityExt where eval {u α} _ _ e := do
   match u, α, e with
   | 0, ~q(ℝ), ~q(@MeasureTheory.integral $i ℝ _ $inst2 _ _ $f) =>
     let i : Q($i) ← mkFreshExprMVarQ q($i) .syntheticOpaque
     have body : Q(ℝ) := .betaRev f #[i]
-    let rbody ← core zα pα body
+    let rbody ← core q(inferInstance) (some q(inferInstance)) body
     let pbody ← rbody.toNonneg
     let pr : Q(∀ x, 0 ≤ $f x) ← mkLambdaFVars #[i] pbody
     assertInstancesCommute
diff --git a/Mathlib/MeasureTheory/Measure/Real.lean b/Mathlib/MeasureTheory/Measure/Real.lean
index b7889e340cdb39..fc1c8252fad8e4 100644
--- a/Mathlib/MeasureTheory/Measure/Real.lean
+++ b/Mathlib/MeasureTheory/Measure/Real.lean
@@ -450,9 +450,10 @@ open Lean Meta Qq Function
 
 /-- Extension for the `positivity` tactic: applications of `μ.real` are nonnegative. -/
 @[positivity MeasureTheory.Measure.real _ _]
-meta def evalMeasureReal : PositivityExt where eval {_ _} _zα _pα e := do
+meta def evalMeasureReal : PositivityExt where eval {_ _} _zα pα? e := do
+  let some pα := pα? | pure .none
   let .app (.app _ a) b ← whnfR e | throwError "not measureReal"
   let p ← mkAppOptM ``MeasureTheory.measureReal_nonneg #[none, none, a, b]
-  pure (.nonnegative p)
+  pure (.nonnegative (leα := q(($pα).toLE)) p)
 
 end Mathlib.Meta.Positivity
diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean b/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean
index 947fd4ac05e8ac..36a4700d94f263 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean
@@ -454,10 +454,13 @@ meta def evalArithmeticFunctionSigma : PositivityExt where eval {u α} z p e :=
   match u, α, e with
   | 0, ~q(ℕ), ~q(ArithmeticFunction.sigma $k $n) =>
     let rn ← core z p n
-    assumeInstancesCommute
     match rn with
-    | .positive pn => return .positive q(Iff.mpr ArithmeticFunction.sigma_pos_iff $pn)
-    | _ => return .nonnegative q(Nat.zero_le _)
+    | .positive pn =>
+      assumeInstancesCommute
+      return .positive q(Iff.mpr ArithmeticFunction.sigma_pos_iff $pn)
+    | _ =>
+      assumeInstancesCommute
+      return .nonnegative q(Nat.zero_le _)
   | _, _, _ => throwError "not ArithmeticFunction.sigma"
 
 
diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean
index ab67f48c8097c5..9b7b0559107619 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean
@@ -230,10 +230,13 @@ meta def evalArithmeticFunctionZeta : PositivityExt where eval {u α} z p e := d
   match u, α, e with
   | 0, ~q(ℕ), ~q(ArithmeticFunction.zeta $n) =>
     let rn ← core z p n
-    assumeInstancesCommute
     match rn with
-    | .positive pn => return .positive q(Iff.mpr ArithmeticFunction.zeta_pos $pn)
-    | _ => return .nonnegative q(Nat.zero_le _)
+    | .positive pn =>
+      assumeInstancesCommute
+      return .positive q(Iff.mpr ArithmeticFunction.zeta_pos $pn)
+    | _ =>
+      assumeInstancesCommute
+      return .nonnegative q(Nat.zero_le _)
   | _, _, _ => throwError "not ArithmeticFunction.zeta"
 
 end Mathlib.Meta.Positivity
diff --git a/Mathlib/NumberTheory/LucasLehmer.lean b/Mathlib/NumberTheory/LucasLehmer.lean
index 165567d52d3d4f..fdf3d2213a2a92 100644
--- a/Mathlib/NumberTheory/LucasLehmer.lean
+++ b/Mathlib/NumberTheory/LucasLehmer.lean
@@ -81,11 +81,14 @@ alias ⟨_, mersenne_pos_of_pos⟩ := mersenne_pos
 meta def evalMersenne : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(ℕ), ~q(mersenne $a) =>
-    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(mersenne_pos_of_pos $pa))
-    | _ => pure (.nonnegative q(Nat.zero_le (mersenne $a)))
+    | .positive pa =>
+      assertInstancesCommute
+      pure (.positive q(mersenne_pos_of_pos $pa))
+    | _ =>
+      assertInstancesCommute
+      pure (.nonnegative q(Nat.zero_le (mersenne $a)))
   | _, _, _ => throwError "not mersenne"
 
 end Mathlib.Meta.Positivity
diff --git a/Mathlib/Tactic/Positivity/Basic.lean b/Mathlib/Tactic/Positivity/Basic.lean
index f006104443763a..1a2d3fc786c1a5 100644
--- a/Mathlib/Tactic/Positivity/Basic.lean
+++ b/Mathlib/Tactic/Positivity/Basic.lean
@@ -58,14 +58,15 @@ end ite
 
 /-- The `positivity` extension which identifies expressions of the form `ite p a b`,
 such that `positivity` successfully recognises both `a` and `b`. -/
-@[positivity ite _ _ _] def evalIte : PositivityExt where eval {u α} zα pα e := do
+@[positivity ite _ _ _] def evalIte : PositivityExt where eval {u α} zα pα? e := do
   let .app (.app (.app (.app f (p : Q(Prop))) (_ : Q(Decidable $p))) (a : Q($α))) (b : Q($α))
     ← withReducible (whnf e) | throwError "not ite"
   haveI' : $e =Q ite $p $a $b := ⟨⟩
-  let ra ← core zα pα a; let rb ← core zα pα b
+  let ra ← core zα pα? a; let rb ← core zα pα? b
   guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(ite (α := $α))
   match ra, rb with
   | .positive pa, .positive pb =>
+    assumeInstancesCommute
     pure (.positive q(ite_pos $p $pa $pb))
   | .positive pa, .nonnegative pb =>
     let _b ← synthInstanceQ q(Preorder $α)
@@ -76,6 +77,7 @@ such that `positivity` successfully recognises both `a` and `b`. -/
     assumeInstancesCommute
     pure (.nonnegative q(ite_nonneg_of_nonneg_of_pos $p $pa $pb))
   | .nonnegative pa, .nonnegative pb =>
+    assumeInstancesCommute
     pure (.nonnegative q(ite_nonneg $p $pa $pb))
   | .positive pa, .nonzero pb =>
     let _b ← synthInstanceQ q(Preorder $α)
@@ -105,113 +107,149 @@ end LinearOrder
 
 /-- The `positivity` extension which identifies expressions of the form `min a b`,
 such that `positivity` successfully recognises both `a` and `b`. -/
-@[positivity min _ _] def evalMin : PositivityExt where eval {u α} zα pα e := do
+@[positivity min _ _] def evalMin : PositivityExt where eval {u α} zα pα? e := do
   let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
     | throwError "not min"
   let _e_eq : $e =Q $f $a $b := ⟨⟩
-  let _a ← synthInstanceQ q(LinearOrder $α)
+  let lα ← synthInstanceQ q(LinearOrder $α)
   assumeInstancesCommute
   let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(min)
-  match ← core zα pα a, ← core zα pα b with
-  | .positive pa, .positive pb => pure (.positive q(lt_min $pa $pb))
-  | .positive pa, .nonnegative pb => pure (.nonnegative q(le_min_of_lt_of_le $pa $pb))
-  | .nonnegative pa, .positive pb => pure (.nonnegative q(le_min_of_le_of_lt $pa $pb))
-  | .nonnegative pa, .nonnegative pb => pure (.nonnegative q(le_min $pa $pb))
-  | .positive pa, .nonzero pb => pure (.nonzero q(min_ne_of_lt_of_ne $pa $pb))
-  | .nonzero pa, .positive pb => pure (.nonzero q(min_ne_of_ne_of_lt $pa $pb))
-  | .nonzero pa, .nonzero pb => pure (.nonzero q(min_ne $pa $pb))
+  match ← core zα pα? a, ← core zα pα? b with
+  | .positive (ltα := ltα) pa, .positive pb =>
+    haveI' : $ltα =Q ($lα).toLT := ⟨⟩
+    assumeInstancesCommute
+    pure (.positive q(lt_min $pa $pb))
+  | .positive pa, .nonnegative pb =>
+    assumeInstancesCommute
+    pure (.nonnegative q(le_min_of_lt_of_le $pa $pb))
+  | .nonnegative pa, .positive pb =>
+    assumeInstancesCommute
+    pure (.nonnegative q(le_min_of_le_of_lt $pa $pb))
+  | .nonnegative pa (leα := leα), .nonnegative pb =>
+    haveI' : $leα =Q ($lα).toLE := ⟨⟩
+    assumeInstancesCommute
+    pure (.nonnegative q(le_min $pa $pb))
+  | .positive pa, .nonzero pb =>
+    assumeInstancesCommute
+    pure (.nonzero q(min_ne_of_lt_of_ne $pa $pb))
+  | .nonzero pa, .positive pb =>
+    assumeInstancesCommute
+    pure (.nonzero q(min_ne_of_ne_of_lt $pa $pb))
+  | .nonzero pa, .nonzero pb => do
+    assumeInstancesCommute
+    pure (.nonzero q(min_ne $pa $pb))
   | _, _ => pure .none
 
 /-- Extension for the `max` operator. The `max` of two numbers is nonnegative if at least one
 is nonnegative, strictly positive if at least one is positive, and nonzero if both are nonzero. -/
-@[positivity max _ _] def evalMax : PositivityExt where eval {u α} zα pα e := do
+@[positivity max _ _] def evalMax : PositivityExt where eval {u α} zα pα? e := do
   let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
     | throwError "not max"
   let _e_eq : $e =Q $f $a $b := ⟨⟩
   let _a ← synthInstanceQ q(LinearOrder $α)
   assumeInstancesCommute
   let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(max)
-  let result : Strictness zα pα e ← catchNone do
-    let ra ← core zα pα a
+  let result : Strictness zα pα? e ← catchNone do
+    let ra ← core zα pα? a
     match ra with
-    | .positive pa => pure (.positive q(lt_max_of_lt_left $pa))
-    | .nonnegative pa => pure (.nonnegative q(le_max_of_le_left $pa))
+    | .positive pa =>
+      assumeInstancesCommute
+      pure (.positive q(lt_max_of_lt_left $pa))
+    | .nonnegative pa =>
+      assumeInstancesCommute
+      pure (.nonnegative q(le_max_of_le_left $pa))
     -- If `a ≠ 0`, we might prove `max a b ≠ 0` if `b ≠ 0` but we don't want to evaluate
     -- `b` before having ruled out `0 < a`, for performance. So we do that in the second branch
     -- of the `orElse'`.
     | _ => pure .none
   orElse result do
-    let rb ← core zα pα b
+    let rb ← core zα pα? b
     match rb with
-    | .positive pb => pure (.positive q(lt_max_of_lt_right $pb))
-    | .nonnegative pb => pure (.nonnegative q(le_max_of_le_right $pb))
+    | .positive pb =>
+      assumeInstancesCommute
+      pure (.positive q(lt_max_of_lt_right $pb))
+    | .nonnegative pb =>
+      assumeInstancesCommute
+      pure (.nonnegative q(le_max_of_le_right $pb))
     | .nonzero pb => do
-      match ← core zα pα a with
+      match ← core zα pα? a with
       | .nonzero pa => pure (.nonzero q(max_ne $pa $pb))
       | _ => pure .none
     | _ => pure .none
 
 /-- The `positivity` extension which identifies expressions of the form `a + b`,
 such that `positivity` successfully recognises both `a` and `b`. -/
-@[positivity _ + _] def evalAdd : PositivityExt where eval {u α} zα pα e := do
+@[positivity _ + _] def evalAdd : 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 := ⟨⟩
   let _a ← synthInstanceQ q(AddZeroClass $α)
   assumeInstancesCommute
   let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HAdd.hAdd)
-  let ra ← core zα pα a; let rb ← core zα pα b
+  let ra ← core zα pα? a; let rb ← core zα pα? b
+  let some pα := pα? | pure .none
   match ra, rb with
-  | .positive pa, .positive pb =>
+  | .positive (ltα := ltα) pa, .positive pb =>
     let _a ← synthInstanceQ q(AddLeftMono $α)
+    haveI' : $ltα =Q ($pα).toLT := ⟨⟩
+    assumeInstancesCommute
     pure (.positive q(add_pos' $pa $pb))
   | .positive pa, .nonnegative pb =>
     let _a ← synthInstanceQ q(AddLeftMono $α)
+    assumeInstancesCommute
     pure (.positive q(add_pos_of_pos_of_nonneg $pa $pb))
   | .nonnegative pa, .positive pb =>
     let _a ← synthInstanceQ q(AddRightMono $α)
+    assumeInstancesCommute
     pure (.positive q(Right.add_pos_of_nonneg_of_pos $pa $pb))
-  | .nonnegative pa, .nonnegative pb =>
+  | .nonnegative (leα := leα) pa, .nonnegative pb =>
     let _a ← synthInstanceQ q(AddLeftMono $α)
+    haveI' : $leα =Q ($pα).toLE := ⟨⟩
+    assumeInstancesCommute
     pure (.nonnegative q(add_nonneg $pa $pb))
   | _, _ => failure
 
 /-- The `positivity` extension which identifies expressions of the form `a * b`,
 such that `positivity` successfully recognises both `a` and `b`. -/
-@[positivity _ * _] def evalMul : PositivityExt where eval {u α} zα pα e := do
+@[positivity _ * _] def evalMul : 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 := ⟨⟩
   let _a ← synthInstanceQ q(Mul $α)
   let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HMul.hMul)
-  let ra ← core zα pα a; let rb ← core zα pα b
-  let tryProveNonzero (pa? : Option Q($a ≠ 0)) (pb? : Option Q($b ≠ 0)) :
-      MetaM (Strictness zα pα e) := do
+  let ra ← core zα pα? a; let rb ← core zα pα? b
+  let tryProveNonzero (pα? : Option Q(PartialOrder $α))
+      (pa? : Option Q($a ≠ 0)) (pb? : Option Q($b ≠ 0)) :
+      MetaM (Strictness zα pα? e) := do
     let pa ← liftOption pa?
     let pb ← liftOption pb?
     let _a ← synthInstanceQ q(NoZeroDivisors $α)
     pure (.nonzero q(mul_ne_zero $pa $pb))
-  let tryProveNonneg (pa? : Option Q(0 ≤ $a)) (pb? : Option Q(0 ≤ $b)) :
-      MetaM (Strictness zα pα e) := do
+  let tryProveNonneg (pα : Q(PartialOrder $α)) (pa? : Option Q(0 ≤ $a)) (pb? : Option Q(0 ≤ $b)) :
+      MetaM (Strictness zα (some pα) e) := do
     let pa ← liftOption pa?
     let pb ← liftOption pb?
     let _a ← synthInstanceQ q(MulZeroClass $α)
     let _a ← synthInstanceQ q(PosMulMono $α)
     assumeInstancesCommute
     pure (.nonnegative q(mul_nonneg $pa $pb))
-  let tryProvePositive (pa? : Option Q(0 < $a)) (pb? : Option Q(0 < $b)) :
-      MetaM (Strictness zα pα e) := do
+  let tryProvePositive (pα : Q(PartialOrder $α)) (pa? : Option Q(0 < $a)) (pb? : Option Q(0 < $b)) :
+      MetaM (Strictness zα (some pα) e) := do
     let pa ← liftOption pa?
     let pb ← liftOption pb?
     let _a ← synthInstanceQ q(MulZeroClass $α)
     let _a ← synthInstanceQ q(PosMulStrictMono $α)
     assumeInstancesCommute
     pure (.positive q(mul_pos $pa $pb))
-  let mut result := .none
-  result ← orElse result (tryProvePositive ra.toPositive rb.toPositive)
-  result ← orElse result (tryProveNonneg ra.toNonneg rb.toNonneg)
-  result ← orElse result (tryProveNonzero ra.toNonzero rb.toNonzero)
-  return result
+  match pα? with
+  | .some pα =>
+    let mut result : Strictness zα (some pα) e := .none
+    result ← orElse result (tryProvePositive pα ra.toPositive rb.toPositive)
+    result ← orElse result (tryProveNonneg pα ra.toNonneg rb.toNonneg)
+    result ← orElse result (tryProveNonzero (some pα) ra.toNonzero rb.toNonzero)
+    return result
+  | .none =>
+    return ← catchNone <| tryProveNonzero .none ra.toNonzero rb.toNonzero
 
 lemma int_div_self_pos {a : ℤ} (ha : 0 < a) : 0 < a / a := by
   rw [Int.ediv_self ha.ne']; exact zero_lt_one
@@ -230,8 +268,8 @@ where `a` and `b` are integers. -/
 @[positivity (_ : ℤ) / (_ : ℤ)] def evalIntDiv : PositivityExt where eval {u α} _ _ e := do
   match u, α, e with
   | 0, ~q(ℤ), ~q($a / $b) =>
-    let ra ← core q(inferInstance) q(inferInstance) a
-    let rb ← core q(inferInstance) q(inferInstance) b
+    let ra ← core q(inferInstance) (some q(inferInstance)) a
+    let rb ← core q(inferInstance) (some q(inferInstance)) b
     assertInstancesCommute
     match ra, rb with
     | .positive (pa : Q(0 < $a)), .positive (pb : Q(0 < $b)) =>
@@ -252,32 +290,44 @@ theorem pow_zero_pos [Semiring α] [PartialOrder α] [IsOrderedRing α] [Nontriv
     (a : α) : 0 < a ^ 0 :=
   zero_lt_one.trans_le (pow_zero a).ge
 
+private theorem pow_zero_ne_zero [Semiring α] [Nontrivial α] (a : α) : a ^ 0 ≠ 0 :=
+  pow_zero a ▸ one_ne_zero
+
 /-- The `positivity` extension which identifies expressions of the form `a ^ (0 : ℕ)`.
 This extension is run in addition to the general `a ^ b` extension (they are overlapping). -/
 @[positivity _ ^ (0 : ℕ)]
-meta def evalPowZeroNat : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalPowZeroNat : PositivityExt where eval {u α} _zα pα? e := do
   let .app (.app _ (a : Q($α))) _ ← withReducible (whnf e) | throwError "not ^"
   let _a ← synthInstanceQ q(Semiring $α)
-  let _a ← synthInstanceQ q(PartialOrder $α)
+  assumeInstancesCommute
+  haveI' : $e =Q $a ^ 0 := ⟨⟩
+  let _a ← synthInstanceQ q(Nontrivial $α)
+  let some _pα := pα? | pure (.nonzero q(pow_zero_ne_zero $a))
   let _a ← synthInstanceQ q(IsOrderedRing $α)
-  _ ← synthInstanceQ q(Nontrivial $α)
-  pure (.positive (q(pow_zero_pos $a) : Expr))
+  pure (.positive q(pow_zero_pos $a))
 
 /-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℕ)`,
 such that `positivity` successfully recognises both `a` and `b`. -/
 @[positivity _ ^ (_ : ℕ)]
-meta def evalPow : PositivityExt where eval {u α} zα pα e := do
+meta def evalPow : PositivityExt where eval {u α} zα pα? e := do
   let .app (.app _ (a : Q($α))) (b : Q(ℕ)) ← withReducible (whnf e) | throwError "not ^"
+  let some pα := pα? | do
+    let _a ← synthInstanceQ q(MonoidWithZero $α)
+    let _a ← synthInstanceQ q(NoZeroDivisors $α)
+    assumeInstancesCommute
+    haveI' : $e =Q $a ^ $b := ⟨⟩
+    let .nonzero nza ← core zα .none a | pure .none
+    pure (.nonzero q(pow_ne_zero $b $nza))
   let result ← catchNone do
+    let _a ← synthInstanceQ q(Ring $α)
+    let _a ← synthInstanceQ q(LinearOrder $α)
+    let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
+    assumeInstancesCommute
     let .true := b.isAppOfArity ``OfNat.ofNat 3 | throwError "not a ^ n where n is a literal"
     let some n := (b.getRevArg! 1).rawNatLit? | throwError "not a ^ n where n is a literal"
     guard (n % 2 = 0)
     have m : Q(ℕ) := mkRawNatLit (n / 2)
     haveI' : $b =Q 2 * $m := ⟨⟩
-    let _a ← synthInstanceQ q(Ring $α)
-    let _a ← synthInstanceQ q(LinearOrder $α)
-    let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
-    assumeInstancesCommute
     haveI' : $e =Q $a ^ $b := ⟨⟩
     pure (.nonnegative q((even_two_mul $m).pow_nonneg $a))
   orElse result do
@@ -305,10 +355,12 @@ meta def evalPow : PositivityExt where eval {u α} zα pα e := do
         trace[Tactic.positivity.failure] "{e.toMessageData}"
         let rα ← synthInstanceQ q(Semiring $α)
         let oα ← synthInstanceQ q(IsOrderedRing $α)
+        assumeInstancesCommute
         orElse (← catchNone (ofNonneg q(le_of_lt $pa) rα oα)) (ofNonzero q(ne_of_gt $pa) rα oα)
     | .nonnegative pa =>
         let sα ← synthInstanceQ q(Semiring $α)
         let oα ← synthInstanceQ q(IsOrderedRing $α)
+        assumeInstancesCommute
         ofNonneg q($pa) q($sα) q($oα)
     | .nonzero pa =>
         let sα ← synthInstanceQ q(Semiring $α)
@@ -321,20 +373,21 @@ theorem abs_pos_of_ne_zero {α : Type*} [AddGroup α] [LinearOrder α]
 
 /-- The `positivity` extension which identifies expressions of the form `|a|`. -/
 @[positivity |_|]
-meta def evalAbs : PositivityExt where eval {_u} (α zα pα) (e : Q($α)) := do
+meta def evalAbs : PositivityExt where eval {_u} (α zα pα?) (e : Q($α)) := do
   let ~q(@abs _ (_) (_) $a) := e | throwError "not |·|"
+  let some pα := pα? | pure .none
   try
-    match ← core zα pα a with
+    match ← core zα (some pα) a with
     | .positive pa =>
       let pa' ← mkAppM ``abs_pos_of_pos #[pa]
-      pure (.positive pa')
+      pure (.positive (ltα := q(($pα).toLT)) pa')
     | .nonzero pa =>
       let pa' ← mkAppM ``abs_pos_of_ne_zero #[pa]
-      pure (.positive pa')
+      pure (.positive (ltα := q(($pα).toLT)) pa')
     | _ => throwError "goto catch"
   catch _ => do
     let pa' ← mkAppM ``abs_nonneg #[a]
-    pure (.nonnegative pa')
+    pure (.nonnegative (leα := q(($pα).toLE)) pa')
 
 theorem int_natAbs_pos {n : ℤ} (hn : 0 < n) : 0 < n.natAbs :=
   Int.natAbs_pos.mpr hn.ne'
@@ -366,17 +419,24 @@ meta def evalNatAbs : PositivityExt where eval {u α} _zα _pα e := do
 /-- Extension for the `positivity` tactic: `Nat.cast` is always non-negative,
 and positive when its input is. -/
 @[positivity Nat.cast _]
-meta def evalNatCast : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalNatCast : PositivityExt where eval {u α} _zα pα? e := do
   let ~q(@Nat.cast _ (_) ($a : ℕ)) := e | throwError "not Nat.cast"
   let zα' : Q(Zero Nat) := q(inferInstance)
-  let pα' : Q(PartialOrder Nat) := q(inferInstance)
   let (_i1 : Q(AddMonoidWithOne $α)) ← synthInstanceQ q(AddMonoidWithOne $α)
+  let some _pα := pα? | do
+    let (_cz : Q(CharZero $α)) ← synthInstanceQ q(CharZero $α)
+    assumeInstancesCommute
+    match ← core zα' .none a with
+    | .nonzero nza => pure (.nonzero q(Nat.cast_ne_zero.2 $nza))
+    | _ => pure .none
+  let pα' : Q(PartialOrder Nat) := q(inferInstance)
   let (_i2 : Q(AddLeftMono $α)) ← synthInstanceQ q(AddLeftMono $α)
   let (_i3 : Q(ZeroLEOneClass $α)) ← synthInstanceQ q(ZeroLEOneClass $α)
   assumeInstancesCommute
   match ← core zα' pα' a with
   | .positive pa =>
     let _nz ← synthInstanceQ q(NeZero (1 : $α))
+    assumeInstancesCommute
     pure (.positive q(Nat.cast_pos'.2 $pa))
   | _ =>
     pure (.nonnegative q(Nat.cast_nonneg' _))
@@ -384,30 +444,30 @@ meta def evalNatCast : PositivityExt where eval {u α} _zα _pα e := do
 /-- Extension for the `positivity` tactic: `Int.cast` is positive (resp. non-negative)
 if its input is. -/
 @[positivity Int.cast _]
-meta def evalIntCast : PositivityExt where eval {u α} _zα _pα e := do
+meta def evalIntCast : PositivityExt where eval {u α} _zα pα? e := do
   let ~q(@Int.cast _ (_) ($a : ℤ)) := e | throwError "not Int.cast"
   let zα' : Q(Zero Int) := q(inferInstance)
   let pα' : Q(PartialOrder Int) := q(inferInstance)
   let ra ← core zα' pα' a
-  match ra with
-  | .positive pa =>
+  match ra, pα? with
+  | .positive pa, some _ =>
     let _rα ← synthInstanceQ q(Ring $α)
     let _oα ← synthInstanceQ q(IsOrderedRing $α)
     let _nt ← synthInstanceQ q(Nontrivial $α)
     assumeInstancesCommute
     pure (.positive q(Int.cast_pos.mpr $pa))
-  | .nonnegative pa =>
+  | .nonnegative pa, some _ =>
     let _rα ← synthInstanceQ q(Ring $α)
     let _oα ← synthInstanceQ q(IsOrderedRing $α)
     let _nt ← synthInstanceQ q(Nontrivial $α)
     assumeInstancesCommute
     pure (.nonnegative q(Int.cast_nonneg $pa))
-  | .nonzero pa =>
+  | .nonzero pa, _ =>
     let _oα ← synthInstanceQ q(AddGroupWithOne $α)
     let _nt ← synthInstanceQ q(CharZero $α)
     assumeInstancesCommute
     pure (.nonzero q(Int.cast_ne_zero.mpr $pa))
-  | .none =>
+  | _ , _ =>
     pure .none
 
 /-- Extension for `Nat.succ`. -/
@@ -456,10 +516,14 @@ meta def evalNatGCD : PositivityExt where eval {u α} z p e := do
   | 0, ~q(ℕ), ~q(Nat.gcd $a $b) =>
     assertInstancesCommute
     match ← core z p a with
-    | .positive pa => return .positive q(Nat.gcd_pos_of_pos_left $b $pa)
+    | .positive pa =>
+      assertInstancesCommute
+      return .positive q(Nat.gcd_pos_of_pos_left $b $pa)
     | _ =>
       match ← core z p b with
-      | .positive pb => return .positive q(Nat.gcd_pos_of_pos_right $a $pb)
+      | .positive pb =>
+        assertInstancesCommute
+        return .positive q(Nat.gcd_pos_of_pos_right $a $pb)
       | _ => failure
   | _, _, _ => throwError "not Nat.gcd"
 
@@ -471,8 +535,10 @@ meta def evalNatLCM : PositivityExt where eval {u α} z p e := do
     assertInstancesCommute
     match ← core z p a with
     | .positive pa =>
+      assertInstancesCommute
       match ← core z p b with
       | .positive pb =>
+        assertInstancesCommute
         return .positive q(Nat.lcm_pos $pa $pb)
       | _ => failure
     | _ => failure
@@ -485,7 +551,9 @@ meta def evalNatSqrt : PositivityExt where eval {u α} z p e := do
   | 0, ~q(ℕ), ~q(Nat.sqrt $n) =>
     assumeInstancesCommute
     match ← core z p n with
-    | .positive pa => return .positive q(Nat.sqrt_pos.mpr $pa)
+    | .positive pa =>
+      assumeInstancesCommute
+      return .positive q(Nat.sqrt_pos.mpr $pa)
     | _ => failure
   | _, _, _ => throwError "not Nat.sqrt"
 
@@ -498,10 +566,10 @@ meta def evalIntGCD : PositivityExt where eval {u α} _ _ e := do
     let z ← synthInstanceQ (q(Zero ℤ) : Q(Type))
     let p ← synthInstanceQ (q(PartialOrder ℤ) : Q(Type))
     assertInstancesCommute
-    match (← catchNone (core z p a)).toNonzero with
+    match (← catchNone (core z (some p) a)).toNonzero with
     | some na => return .positive q(Int.gcd_pos_of_ne_zero_left $b $na)
     | none =>
-      match (← core z p b).toNonzero with
+      match (← core z (some p) b).toNonzero with
       | some nb => return .positive q(Int.gcd_pos_of_ne_zero_right $a $nb)
       | none => failure
   | _, _, _ => throwError "not Int.gcd"
@@ -514,9 +582,9 @@ meta def evalIntLCM : PositivityExt where eval {u α} _ _ e := do
     let z ← synthInstanceQ (q(Zero ℤ) : Q(Type))
     let p ← synthInstanceQ (q(PartialOrder ℤ) : Q(Type))
     assertInstancesCommute
-    match (← core z p a).toNonzero with
+    match (← core z (some p) a).toNonzero with
     | some na =>
-      match (← core z p b).toNonzero with
+      match (← core z (some p) b).toNonzero with
       | some nb => return .positive q(Int.lcm_pos $na $nb)
       | _ => failure
     | _ => failure
@@ -536,9 +604,12 @@ meta def evalNNRatNum : PositivityExt where eval {u α} _ _ e := do
   | 0, ~q(ℕ), ~q(NNRat.num $a) =>
     let zα : Q(Zero ℚ≥0) := q(inferInstance)
     let pα : Q(PartialOrder ℚ≥0) := q(inferInstance)
+    trace[Tactic.positivity] "I'm evalNNRatNum: {e}"
     assumeInstancesCommute
     match ← core zα pα a with
-    | .positive pa => return .positive q(NNRat.num_pos_of_pos $pa)
+    | .positive pa =>
+      assumeInstancesCommute
+      return .positive q(NNRat.num_pos_of_pos $pa)
     | .nonzero pa => return .nonzero q(NNRat.num_ne_zero_of_ne_zero $pa)
     | _ => return .none
   | _, _, _ => throwError "not NNRat.num"
@@ -576,8 +647,12 @@ meta def evalRatNum : PositivityExt where eval {u α} _ _ e := do
     let pα : Q(PartialOrder ℚ) := q(inferInstance)
     assumeInstancesCommute
     match ← core zα pα a with
-    | .positive pa => pure <| .positive q(num_pos_of_pos $pa)
-    | .nonnegative pa => pure <| .nonnegative q(num_nonneg_of_nonneg $pa)
+    | .positive pa =>
+      assumeInstancesCommute
+      pure <| .positive q(num_pos_of_pos $pa)
+    | .nonnegative pa =>
+      assumeInstancesCommute
+      pure <| .nonnegative q(num_nonneg_of_nonneg $pa)
     | .nonzero pa => pure <| .nonzero q(num_ne_zero_of_ne_zero $pa)
     | .none => pure .none
   | _, _ => throwError "not Rat.num"
@@ -603,7 +678,9 @@ meta def evalPosPart : PositivityExt where eval {u α} zα pα e := do
     -- `.none`) here sometimes. See e.g. the first test for `posPart`. This is why we need
     -- `catchNone`
     match ← catchNone (core zα pα a) with
-    | .positive pf => return .positive q(posPart_pos $pf)
+    | .positive pf =>
+      assumeInstancesCommute
+      return .positive q(posPart_pos $pf)
     | _ => return .nonnegative q(posPart_nonneg $a)
   | _ => throwError "not `posPart`"
 
@@ -620,11 +697,12 @@ meta def evalNegPart : PositivityExt where eval {u α} _ _ e := do
 
 /-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/
 @[positivity DFunLike.coe _ _]
-meta def evalMap : PositivityExt where eval {_ β} _ _ e := do
+meta def evalMap : PositivityExt where eval {_ β} _ pβ? e := do
+  let some pβ := pβ? | pure .none
   let .app (.app _ f) a ← whnfR e
     | throwError "not ↑f · where f is of NonnegHomClass"
   let pa ← mkAppOptM ``apply_nonneg #[none, none, β, none, none, none, none, f, a]
-  pure (.nonnegative pa)
+  pure (.nonnegative (leα := q(($pβ).toLE)) pa)
 
 end Positivity
 
diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean
index d3df8b04546968..cdd2a28e1dfd6d 100644
--- a/Mathlib/Tactic/Positivity/Core.lean
+++ b/Mathlib/Tactic/Positivity/Core.lean
@@ -32,46 +32,53 @@ lemma ne_of_ne_of_eq' {α : Sort*} {a c b : α} (hab : (a : α) ≠ c) (hbc : a
 
 namespace Mathlib.Meta.Positivity
 
-variable {u : Level} {α : Q(Type u)} (zα : Q(Zero $α)) (pα : Q(PartialOrder $α))
+variable {u : Level} {α : Q(Type u)} (zα : Q(Zero $α)) (pα? : Option Q(PartialOrder $α))
 
 /-- The result of `positivity` running on an expression `e` of type `α`. -/
-inductive Strictness (e : Q($α)) where
-  | positive (pf : Q(0 < $e))
-  | nonnegative (pf : Q(0 ≤ $e))
+inductive Strictness (pα? : Option Q(PartialOrder $α)) (e : Q($α)) where
+  | positive {ltα : Q(LT $α)} (pf : Q(0 < $e))
+  | nonnegative {leα : Q(LE $α)} (pf : Q(0 ≤ $e))
   | nonzero (pf : Q($e ≠ 0))
   | none
   deriving Repr
 
 /-- Gives a generic description of the `positivity` result. -/
-def Strictness.toString {e : Q($α)} : Strictness zα pα e → String
+def Strictness.toString {e : Q($α)} : Strictness zα pα? e → String
   | positive _ => "positive"
   | nonnegative _ => "nonnegative"
   | nonzero _ => "nonzero"
   | none => "none"
 
 /-- Extract a proof that `e` is positive, if possible, from `Strictness` information about `e`. -/
-def Strictness.toPositive {e} : Strictness zα pα e → Option Q(0 < $e)
+def Strictness.toPositive (pα : Q(PartialOrder $α)) {e} :
+    Strictness zα (some pα) e → Option Q(0 < $e)
   | .positive pf => some pf
   | _ => .none
 
 /-- Extract a proof that `e` is nonnegative, if possible, from `Strictness` information about `e`.
 -/
-def Strictness.toNonneg {e} : Strictness zα pα e → Option Q(0 ≤ $e)
-  | .positive pf => some q(le_of_lt $pf)
+def Strictness.toNonneg (pα : Q(PartialOrder $α)) {e} :
+    Strictness zα (some pα) e → Option Q(0 ≤ $e)
+  | .positive pf => do
+    assumeInstancesCommute
+    some q(le_of_lt $pf)
   | .nonnegative pf => some pf
   | _ => .none
 
 /-- Extract a proof that `e` is nonzero, if possible, from `Strictness` information about `e`. -/
-def Strictness.toNonzero {e} : Strictness zα pα e → Option Q($e ≠ 0)
-  | .positive pf => some q(ne_of_gt $pf)
+def Strictness.toNonzero {e} : Strictness zα pα? e → Option Q($e ≠ 0)
+  | .positive pf => do
+    let some _ := pα? | .none
+    assumeInstancesCommute
+    some q(ne_of_gt $pf)
   | .nonzero pf => some pf
   | _ => .none
 
 /-- An extension for `positivity`. -/
 structure PositivityExt where
   /-- Attempts to prove an expression `e : α` is `>0`, `≥0`, or `≠0`. -/
-  eval {u : Level} {α : Q(Type u)} (zα : Q(Zero $α)) (pα : Q(PartialOrder $α)) (e : Q($α)) :
-    MetaM (Strictness zα pα e)
+  eval {u : Level} {α : Q(Type u)} (zα : Q(Zero $α)) (pα? : Option Q(PartialOrder $α)) (e : Q($α)) :
+    MetaM (Strictness zα pα? e)
 
 /-- Read a `positivity` extension from a declaration of the right type. -/
 def mkPositivityExt (n : Name) : ImportM PositivityExt := do
@@ -191,24 +198,26 @@ lemma nz_of_isRat {n : ℤ} {d : ℕ} [Ring A] [LinearOrder A] [IsStrictOrderedR
     rw [eq]
     exact ne_iff_lt_or_gt.2 (Or.inl neg)
 
-variable {zα pα} in
+variable {zα pα?} in
 /-- Converts a `MetaM Strictness` which can fail
 into one that never fails and returns `.none` instead. -/
-def catchNone {e : Q($α)} (t : MetaM (Strictness zα pα e)) : MetaM (Strictness zα pα e) :=
+def catchNone {e : Q($α)} (t : MetaM (Strictness zα pα? e)) : MetaM (Strictness zα pα? e) :=
   try t catch e =>
     trace[Tactic.positivity.failure] "{e.toMessageData}"
     pure .none
 
-variable {zα pα} in
+variable {zα pα?} in
 /-- Converts a `MetaM Strictness` which can return `.none`
 into one which never returns `.none` but fails instead. -/
-def throwNone {e : Q($α)} (t : MetaM (Strictness zα pα e)) : MetaM (Strictness zα pα e) := do
+def throwNone {e : Q($α)} (t : MetaM (Strictness zα pα? e)) : MetaM (Strictness zα pα? e) := do
   match ← t with
   | .none => throwError "Strictness result was `{.ofConstName ``Strictness.none}`."
   | r => pure r
 
 /-- Attempts to prove a `Strictness` result when `e` evaluates to a literal number. -/
-def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone do
+def normNumPositivity (pα : Q(PartialOrder $α)) (e : Q($α))
+    : MetaM (Strictness zα pα e) := catchNone do
+  trace[Tactic.positivity] "Is {e} rawNatLit? : {e.isRawNatLit}"
   match ← NormNum.derive e with
   | .isBool .. => failure
   | .isNat _ lit p =>
@@ -290,7 +299,7 @@ def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone d
       pure (.nonnegative q(nonneg_of_isRat $p $w))
 
 /-- Attempts to prove that `e ≥ 0` using `zero_le` in a `CanonicallyOrderedAdd` monoid. -/
-def positivityCanon (e : Q($α)) : MetaM (Strictness zα pα e) := do
+def positivityCanon (pα : Q(PartialOrder $α)) (e : Q($α)) : MetaM (Strictness zα pα e) := do
   let _add ← synthInstanceQ q(AddMonoid $α)
   let _le ← synthInstanceQ q(PartialOrder $α)
   let _i ← synthInstanceQ q(CanonicallyOrderedAdd $α)
@@ -298,33 +307,46 @@ def positivityCanon (e : Q($α)) : MetaM (Strictness zα pα e) := do
   pure (.nonnegative q(zero_le $e))
 
 /-- A variation on `assumption` when the hypothesis is `lo ≤ e` where `lo` is a numeral. -/
-def compareHypLE (lo e : Q($α)) (p₂ : Q($lo ≤ $e)) : MetaM (Strictness zα pα e) := do
+def compareHypLE (pα : Q(PartialOrder $α)) (lo e : Q($α)) (p₂ : Q($lo ≤ $e)) :
+    MetaM (Strictness zα pα e) := do
   match ← normNumPositivity zα pα lo with
-  | .positive p₁ => pure (.positive q(lt_of_lt_of_le $p₁ $p₂))
-  | .nonnegative p₁ => pure (.nonnegative q(le_trans $p₁ $p₂))
+  | .positive p₁ => do
+    assumeInstancesCommute
+    pure (.positive q(lt_of_lt_of_le $p₁ $p₂))
+  | .nonnegative p₁ => do
+    assumeInstancesCommute
+    pure (.nonnegative q(le_trans $p₁ $p₂))
   | _ => pure .none
 
 /-- A variation on `assumption` when the hypothesis is `lo < e` where `lo` is a numeral. -/
-def compareHypLT (lo e : Q($α)) (p₂ : Q($lo < $e)) : MetaM (Strictness zα pα e) := do
+def compareHypLT (pα : Q(PartialOrder $α)) (lo e : Q($α)) (p₂ : Q($lo < $e)) :
+    MetaM (Strictness zα pα e) := do
   match ← normNumPositivity zα pα lo with
-  | .positive p₁ => pure (.positive q(lt_trans $p₁ $p₂))
-  | .nonnegative p₁ => pure (.positive q(lt_of_le_of_lt $p₁ $p₂))
+  | .positive p₁ => do
+    assumeInstancesCommute
+    pure (.positive q(lt_trans $p₁ $p₂))
+  | .nonnegative p₁ => do
+    assumeInstancesCommute
+    pure (.positive q(lt_of_le_of_lt $p₁ $p₂))
   | _ => pure .none
 
 /-- A variation on `assumption` when the hypothesis is `x = e` where `x` is a numeral. -/
-def compareHypEq (e x : Q($α)) (p₂ : Q($x = $e)) : MetaM (Strictness zα pα e) := do
+def compareHypEq (pα : Q(PartialOrder $α)) (e x : Q($α)) (p₂ : Q($x = $e)) :
+    MetaM (Strictness zα pα e) := do
   match ← normNumPositivity zα pα x with
   | .positive p₁ => pure (.positive q(lt_of_lt_of_eq $p₁ $p₂))
   | .nonnegative p₁ => pure (.nonnegative q(le_of_le_of_eq $p₁ $p₂))
   | .nonzero p₁ => pure (.nonzero q(ne_of_ne_of_eq' $p₁ $p₂))
   | .none => pure .none
 
+
 initialize registerTraceClass `Tactic.positivity
 initialize registerTraceClass `Tactic.positivity.failure
 
 /-- A variation on `assumption` which checks if the hypothesis `ldecl` is `a [</≤/=] e`
 where `a` is a numeral. -/
-def compareHyp (e : Q($α)) (ldecl : LocalDecl) : MetaM (Strictness zα pα e) := do
+def compareHyp (pα : Q(PartialOrder $α)) (e : Q($α)) (ldecl : LocalDecl) :
+    MetaM (Strictness zα pα e) := do
   have e' : Q(Prop) := ldecl.type
   let p : Q($e') := .fvar ldecl.fvarId
   match e' with
@@ -356,7 +378,23 @@ def compareHyp (e : Q($α)) (ldecl : LocalDecl) : MetaM (Strictness zα pα e) :
       match rhs with
       | ~q(0) => pure <| .nonnegative q(ge_of_eq $p)
       | _ => compareHypEq zα pα e rhs q(Eq.symm $p)
-  | ~q(@Ne.{u + 1} $α' $lhs $rhs) =>
+  | ~q(@Ne.{u+1} $α' $lhs $rhs) =>
+    let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none
+    match lhs, rhs with
+    | ~q(0), _ =>
+      let .defEq _ ← isDefEqQ e rhs | pure .none
+      pure <| .nonzero q(Ne.symm $p)
+    | _, ~q(0) =>
+      let .defEq _ ← isDefEqQ e lhs | pure .none
+      pure <| .nonzero q($p)
+    | _, _ => pure .none
+  | _ => pure .none
+
+def compareHypNonzero (e : Q($α)) (ldecl : LocalDecl) : MetaM (Strictness zα .none e) := do
+  have e' : Q(Prop) := ldecl.type
+  let p : Q($e') := .fvar ldecl.fvarId
+  match e' with
+  | ~q(@Ne.{u+1} $α' $lhs $rhs) =>
     let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none
     match lhs, rhs with
     | ~q(0), _ =>
@@ -368,46 +406,69 @@ def compareHyp (e : Q($α)) (ldecl : LocalDecl) : MetaM (Strictness zα pα e) :
     | _, _ => pure .none
   | _ => pure .none
 
-variable {zα pα} in
+variable {zα pα?} in
 /-- The main combinator which combines multiple `positivity` results.
 It assumes `t₁` has already been run for a result, and runs `t₂` and takes the best result.
 It will skip `t₂` if `t₁` is already a proof of `.positive`, and can also combine
 `.nonnegative` and `.nonzero` to produce a `.positive` result. -/
-def orElse {e : Q($α)} (t₁ : Strictness zα pα e) (t₂ : MetaM (Strictness zα pα e)) :
-    MetaM (Strictness zα pα e) := do
+def orElse {e : Q($α)} (t₁ : Strictness zα pα? e) (t₂ : MetaM (Strictness zα pα? e)) :
+    MetaM (Strictness zα pα? e) := do
   match t₁ with
   | .none => catchNone t₂
   | p@(.positive _) => pure p
   | .nonnegative p₁ =>
     match ← catchNone t₂ with
     | p@(.positive _) => pure p
-    | .nonzero p₂ => pure (.positive q(lt_of_le_of_ne' $p₁ $p₂))
+    | .nonzero p₂ =>
+      let some _ := pα? | throwError "cannot synth PartialOrd for {α}"
+      assumeInstancesCommute
+      pure (.positive q(lt_of_le_of_ne' $p₁ $p₂))
     | _ => pure (.nonnegative p₁)
   | .nonzero p₁ =>
     match ← catchNone t₂ with
     | p@(.positive _) => pure p
-    | .nonnegative p₂ => pure (.positive q(lt_of_le_of_ne' $p₂ $p₁))
+    | .nonnegative p₂ =>
+      let some _ := pα? | throwError "cannot synth PartialOrd for {α}"
+      assumeInstancesCommute
+      pure (.positive q(lt_of_le_of_ne' $p₂ $p₁))
     | _ => pure (.nonzero p₁)
 
 /-- Run each registered `positivity` extension on an expression, returning a `NormNum.Result`. -/
-def core (e : Q($α)) : MetaM (Strictness zα pα e) := do
+def core (e : Q($α)) : MetaM (Strictness zα pα? e) := do
   let mut result := .none
   trace[Tactic.positivity] "trying to prove positivity of {e}"
   for ext in ← (positivityExt.getState (← getEnv)).2.getMatch e do
     try
-      result ← orElse result <| ext.eval zα pα e
+      result ← orElse result <| ext.eval zα pα? e
     catch err =>
-      trace[Tactic.positivity] "{e} failed: {err.toMessageData}"
-  result ← orElse result <| normNumPositivity zα pα e
-  result ← orElse result <| positivityCanon zα pα e
-  if let .positive _ := result then
+      trace[Tactic.positivity] "{e} ext failed: {err.toMessageData}"
+  trace[Tactic.positivity] "current result from ext: {result.toString}" -- ??
+  match pα? with
+  | some pα =>
+    trace[Tactic.positivity] "{α} has some {pα}"
+    result ← orElse result <| normNumPositivity zα pα e
+    trace[Tactic.positivity] "current result from normNum: {result.toString}"
+    result ← orElse result <| positivityCanon zα pα e
+    trace[Tactic.positivity] "current result from canonicity: {result.toString}"
+    if let .positive _ := result then
+      trace[Tactic.positivity] "{e} => {result.toString}"
+      return result
+    for ldecl in ← getLCtx do
+      if !ldecl.isImplementationDetail then
+        result ← orElse result <| compareHyp zα pα e ldecl
     trace[Tactic.positivity] "{e} => {result.toString}"
-    return result
-  for ldecl in ← getLCtx do
-    if !ldecl.isImplementationDetail then
-      result ← orElse result <| compareHyp zα pα e ldecl
-  trace[Tactic.positivity] "{e} => {result.toString}"
-  throwNone (pure result)
+    throwNone (pure result)
+  | .none =>
+    trace[Tactic.positivity] "{α} has no PartialOrder"
+    if let .nonzero _ := result then
+      trace[Tactic.positivity] "{e} => {result.toString}"
+      return result
+    for ldecl in ← getLCtx do
+      if !ldecl.isImplementationDetail then
+        result ← orElse result <| compareHypNonzero zα e ldecl
+    trace[Tactic.positivity] "{e} => {result.toString}"
+    throwNone (pure result)
+
 
 private inductive OrderRel : Type
 | le : OrderRel -- `0 ≤ a`
@@ -424,8 +485,8 @@ inequality was established) together with the proof as an expression. -/
 def bestResult (e : Expr) : MetaM (Bool × Expr) := do
   let ⟨u, α, _⟩ ← inferTypeQ' e
   let zα ← synthInstanceQ q(Zero $α)
-  let pα ← synthInstanceQ q(PartialOrder $α)
-  match ← try? (Meta.Positivity.core zα pα e) with
+  let pα? ← try? <| synthInstanceQ q(PartialOrder $α)
+  match ← try? (Meta.Positivity.core zα pα? e) with
   | some (.positive pf) => pure (true, pf)
   | some (.nonnegative pf) => pure (false, pf)
   | _ => throwError "could not establish the nonnegativity of {e}"
@@ -444,26 +505,41 @@ def solve (t : Q(Prop)) : MetaM Expr := do
     let zα ← synthInstanceQ q(Zero $α)
     assumeInstancesCommute
     let .true ← isDefEq z q(0 : $α) | throwError "not a positivity goal"
-    let pα ← synthInstanceQ q(PartialOrder $α)
+    let pα? ← try? <| synthInstanceQ q(PartialOrder $α)
     assumeInstancesCommute
-    let r ← catchNone <| Meta.Positivity.core zα pα e
+    let r ← catchNone <| Meta.Positivity.core zα pα? e
     let throw (a b : String) : MetaM Expr := throwError
       "failed to prove {a}, but it would be possible to prove {b} if desired"
-    let p ← show MetaM Expr from match relDesired, r with
-    | .lt, .positive p
-    | .le, .nonnegative p
-    | .ne, .nonzero p => pure p
-    | .le, .positive p => pure q(le_of_lt $p)
-    | .ne, .positive p => pure q(ne_of_gt $p)
-    | .ne', .positive p => pure q(ne_of_lt $p)
-    | .ne', .nonzero p => pure q(Ne.symm $p)
-    | .lt, .nonnegative _ => throw "strict positivity" "nonnegativity"
-    | .lt, .nonzero _ => throw "strict positivity" "nonzeroness"
-    | .le, .nonzero _ => throw "nonnegativity" "nonzeroness"
-    | .ne, .nonnegative _
-    | .ne', .nonnegative _ => throw "nonzeroness" "nonnegativity"
-    | _, .none => throwError "failed to prove positivity/nonnegativity/nonzeroness"
-    pure p
+    if let some _ := pα? then
+      let p ← show MetaM Expr from match relDesired, r with
+      | .lt, .positive p
+      | .le, .nonnegative p
+      | .ne, .nonzero p => pure p
+      | .le, .positive p => do
+        assumeInstancesCommute
+        pure q(le_of_lt $p)
+      | .ne, .positive p => do
+        assumeInstancesCommute
+        pure q(ne_of_gt $p)
+      | .ne', .positive p => do
+        assumeInstancesCommute
+        pure q(ne_of_lt $p)
+      | .ne', .nonzero p => pure q(Ne.symm $p)
+      | .lt, .nonnegative _ => throw "strict positivity" "nonnegativity"
+      | .lt, .nonzero _ => throw "strict positivity" "nonzeroness"
+      | .le, .nonzero _ => throw "nonnegativity" "nonzeroness"
+      | .ne, .nonnegative _
+      | .ne', .nonnegative _ => throw "nonzeroness" "nonnegativity"
+      | _, .none => throwError "failed to prove positivity/nonnegativity/nonzeroness"
+      pure p
+    else
+      let p ← show MetaM Expr from match relDesired, r with
+      | .ne, .nonzero p => pure p
+      | .ne', .nonzero p => pure q(Ne.symm $p)
+      | .lt, .nonzero _ => throw "strict positivity" "nonzeroness"
+      | .le, .nonzero _ => throw "nonnegativity" "nonzeroness"
+      | _, _ => throwError "failed to prove nonzeroness"
+      pure p
   match t with
   | ~q(@LE.le $α $_a $z $e) => rest α z e .le
   | ~q(@LT.lt $α $_a $z $e) => rest α z e .lt
diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean
index 380fcac4608664..21d273da5c8e5b 100644
--- a/Mathlib/Tactic/Positivity/Finset.lean
+++ b/Mathlib/Tactic/Positivity/Finset.lean
@@ -68,12 +68,13 @@ example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.sum
 because `compareHyp` can't look for assumptions behind binders.
 -/
 @[positivity Finset.sum _ _]
-meta def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
+meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e := do
   match e with
   | ~q(@Finset.sum $ι _ $instα $s $f) =>
     let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque
     have body : Q($α) := .betaRev f #[i]
-    let rbody ← core zα pα body
+    let rbody ← core zα pα? body
+    let some pα := pα? | pure .none -- TODO: the case without PartialOrder
     let p_pos : Option Q(0 < $e) := ← (do
       let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
       let some ps ← proveFinsetNonempty s | pure none
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean
index daf6e373fa1c49..0d07c61e5ffef9 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean
@@ -369,7 +369,8 @@ attribute [local instance] monadLiftOptionMetaM in
 This extension only proves non-negativity, strict positivity is more delicate for infinite sums and
 requires more assumptions. -/
 @[positivity tsum _]
-meta def evalTsum : PositivityExt where eval {u α} zα pα e := do
+meta def evalTsum : PositivityExt where eval {u α} zα pα? e := do
+  let some pα := pα? | pure .none
   match e with
   | ~q(@tsum _ $ι $instCommMonoid $instTopSpace $f $L) =>
     lambdaBoundedTelescope f 1 fun args (body : Q($α)) => do