From 43f82c4e473c7815b4f193c55d0e0af8d3c73e59 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 13 Jan 2025 18:09:55 +0000 Subject: [PATCH] chore: remove useless rw in testBit_mul_two_pow_gt --- src/Init/Data/Nat/Bitwise/Lemmas.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index af72b2797848..0b11e229d147 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -133,10 +133,8 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) : rw [Nat.mul_comm, Nat.div_mul_cancel] suffices hs : 2 * (x * 2 ^ (k - 1)) = x * 2 ^ k by exact ⟨_, hs.symm⟩ - let j := k - 1 - have hj : 2 ^ (k - 1) = 2 ^ j := by simp only [j] - have hj' : 2 ^ k = 2 ^ (j + 1) := by simp only [j]; rw [Nat.sub_add_cancel]; omega - rw [hj, hj', Nat.pow_add, Nat.pow_one, Nat.mul_comm, Nat.mul_assoc] + rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.sub_add_cancel] + omega omega theorem testBit_mul_two_pow (x i n : Nat) :