From e43514ac7647d9412c6cd2213dce5d7d140d1dc0 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Fri, 13 Jan 2023 07:01:26 +0800
Subject: [PATCH] test linter

---
 Mathlib/Data/Nat/WithBot.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Nat/WithBot.lean b/Mathlib/Data/Nat/WithBot.lean
index 1ab1c157845a1..893f6c9272580 100644
--- a/Mathlib/Data/Nat/WithBot.lean
+++ b/Mathlib/Data/Nat/WithBot.lean
@@ -56,10 +56,10 @@ theorem add_eq_three_iff {n m : WithBot ℕ} :
 #align nat.with_bot.add_eq_three_iff Nat.WithBot.add_eq_three_iff
 
 @[simp]
-theorem coe_nonneg {n : ℕ} : 0 ≤ (n : WithBot ℕ) := by
+theorem coe_nonneg' {n : ℕ} : 0 ≤ (n : WithBot ℕ) := by
   rw [← WithBot.coe_zero]
   exact WithBot.coe_le_coe.mpr (Nat.zero_le n)
-#align nat.with_bot.coe_nonneg Nat.WithBot.coe_nonneg
+#align nat.with_bot.coe_nonneg Nat.WithBot.coe_nonneg'
 
 @[simp]
 theorem lt_zero_iff (n : WithBot ℕ) : n < 0 ↔ n = ⊥ := by