. rw [bitwise_mod_two and (by decide)]
  simp
  have : ∀ (l : Nat), l > 0 → (2*l - 1) % 2 = 1 := by
    intro l hl
    cases l
    case zero => cases hl
    case succ l =>
      conv =>
        lhs; rw [Nat.mul_succ]; change (2*l+1+1-1)%2
        rw [Nat.add_sub_cancel, Nat.add_comm, Nat.add_mul_mod_self_left]
  simp [this (2^k) (Nat.pos_pow_of_pos k (by decide))]
  rw [Nat.mod_mul_mod_left n 2 _]
  apply (n.mod_two_eq_zero_or_one).elim <;> intro h <;> simp [h]
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) % 2 = n % (2 * 2 ^ k) % 2
no goals