cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
case f
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.toNat (decide (bit b n✝ % 2 = 0)) = (bit b n✝ + 1) % 2
⊢ Bool.toNat (decide (bit b n✝ % 2 = 0)) = (bit b n✝ + 1) % 2
no goals