From c25b5e84e08297566dd5f24080e391825947a6ce Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 21 Jan 2025 16:20:12 +0000 Subject: [PATCH] chore: remove useless theorem --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 19fbf08d4603..3f57854a6d22 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3079,7 +3079,7 @@ theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w): · simp only [h₁, decide_true, Bool.true_and] have h₂ : (r + n) < 2 * (w + 1) := by omega congr 1 - rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega), Nat.mul_one] + rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega)] omega · simp [h₁]