English
For all n and bit indicator m, testBit (bit b n) (Nat.succ m) equals testBit n m.
Русский
Для всех n и индикатора бита m: testBit (bit b n) (Nat.succ m) = testBit n m.
LaTeX
$$$$ \forall n \in \mathbb{Z},\ \text{testBit}(\operatorname{bit}(b,n),\mathsf{succ}(m)) = \text{testBit}(n,m). $$$$
Lean4
@[simp]
theorem testBit_bit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m
| (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_succ
| -[n+1] => by
dsimp only [testBit]
simp only [bit_negSucc]
cases b <;>
simp only [Bool.not_false, Bool.not_true, Nat.testBit_bit_succ]
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO
-- private unsafe def bitwise_tac : tactic Unit :=
-- sorry
-- Porting note: Was `bitwise_tac` in mathlib
