From 0bd140e40b23a558dcd319f3e27d3862ff2aff88 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 10 May 2024 13:26:52 +0100
Subject: [PATCH] correct error message

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Tactic/Positivity/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Positivity/Basic.lean b/Mathlib/Tactic/Positivity/Basic.lean
index 8137385077e63..1b38b8b695c40 100644
--- a/Mathlib/Tactic/Positivity/Basic.lean
+++ b/Mathlib/Tactic/Positivity/Basic.lean
@@ -449,7 +449,7 @@ def evalNNRatDen : PositivityExt where eval {u α} _ _ e := do
   | 0, ~q(ℕ), ~q(NNRat.den $a) =>
     assumeInstancesCommute
     return .positive q(den_pos $a)
-  | _, _, _ => throwError "not NNRat.num"
+  | _, _, _ => throwError "not NNRat.den"
 
 variable {q : ℚ≥0}