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