m : ℕ
b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n)) (Nat.succ m) = testBit (↑n) m
m : ℕ
b : Bool
n : ℕ
⊢ testBit (bit b ↑n) (Nat.succ m) = testBit (↑n) m
rw [bit_coe_nat]
no goals
m : ℕ
b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n)) (Nat.succ m) = testBit (↑n) m
apply Nat.testBit_succ
m : ℕ
b : Bool
n : ℕ
⊢ (match bit b -[n+1], Nat.succ m with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    !Nat.testBit n m
m : ℕ
b : Bool
n : ℕ
⊢ testBit (bit b -[n+1]) (Nat.succ m) = testBit -[n+1] m
dsimp [testBit]
m : ℕ
b : Bool
n : ℕ
⊢ (!Nat.testBit (Nat.bit (!b) n) (Nat.succ m)) = !Nat.testBit n m
m : ℕ
b : Bool
n : ℕ
⊢ (match bit b -[n+1], Nat.succ m with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    !Nat.testBit n m
simp only [bit_negSucc]
no goals
m : ℕ
b : Bool
n : ℕ
⊢ (!Nat.testBit (Nat.bit (!b) n) (Nat.succ m)) = !Nat.testBit n m
cases b <;> simp [Nat.testBit_succ]