chore: @[simp] for Nat.testBit_one_eq_true_iff_self_eq_zero

opencompl · Jun 28, 2024 · 37e8ef9 · 37e8ef9
1 parent faf6697
commit 37e8ef9
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -311,6 +311,7 @@ theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
         Nat.mod_eq_of_lt]
 
 /-- `testBit 1 i` is true iff the index `i` equals 0. -/
+@[simp]
 theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
     Nat.testBit 1 i = true ↔ i = 0 := by
   cases i <;> simp