From a3c333dcd697a6553d44a552ee1f8a72f39aaab5 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 19 Oct 2024 12:42:34 +0100
Subject: [PATCH] avoid some unused variables

---
 src/Init/Data/Int/Lemmas.lean | 4 ++--
 src/Init/Omega/Int.lean       | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index e3c2db105bd4..ddc32205fadc 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -24,9 +24,9 @@ theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat
 theorem subNatNat_of_sub {m n : Nat} (h : n ≤ m) : subNatNat m n = ↑(m - n) := by
   rw [subNatNat, ofNat_eq_coe]
   split
-  case h_1 x h' =>
+  case h_1 _ _ =>
     simp
-  case h_2 x h' =>
+  case h_2 _ h' =>
     rw [Nat.sub_eq_zero_of_le h] at h'
     simp at h'
 
diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean
index 8487cdd8bf45..6c4c1b4c34ca 100644
--- a/src/Init/Omega/Int.lean
+++ b/src/Init/Omega/Int.lean
@@ -94,7 +94,7 @@ theorem ofNat_sub_dichotomy {a b : Nat} :
     b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0 := by
   by_cases h : b ≤ a
   · left
-    have t := Int.ofNat_sub h
+    have := Int.ofNat_sub h
     simp [h]
   · right
     have t := Nat.not_le.mp h