From 350923248006a91215adcf9589b896f6061eb23c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 7 May 2024 23:14:06 +0200
Subject: [PATCH] Unused variable

---
 src/Init/Data/Nat/Div.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index f49aae34757c..ae531772cb0a 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -102,7 +102,7 @@ protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
     exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
   | 1, 0 => rw [Nat.modCore]; rfl
   | 1, 1 => rw [Nat.modCore, Nat.modCore]; rfl
-  | 1, (y+2) => rw [Nat.modCore]; rfl
+  | 1, (_+2) => rw [Nat.modCore]; rfl
   | (_ + 2), _ => rfl
 
 theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by