avoid some unused variables

opencompl · Oct 19, 2024 · a3c333d · a3c333d
1 parent 514d0da
commit a3c333d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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