fix Tactic.Positivity.Core

leanprover-community · May 9, 2024 · 08e4eb0 · 08e4eb0
1 parent e0ef14e
commit 08e4eb0
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean
@@ -178,6 +178,7 @@ def throwNone [Monad m] [Alternative m]
   | .none => failure
   | r => pure r
 
+attribute [instance 1000] OrderedSemiring.toSemiring StrictOrderedRing.toRing in
 /-- Attempts to prove a `Strictness` result when `e` evaluates to a literal number. -/
 def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone do
   match ← NormNum.derive e with