case succ k h_ind =>
  conv =>
    change bitwise and n (2^k*2 - 1) = n % (2^k*2)
    rw [Nat.mul_comm _ 2]
  apply eq_of_div_mod_two_eq
  . rw [bitwise_div_two]
    rw [Nat.mul_sub_div 0 2 (2^k) (by rw [Nat.mul_comm]; exact Nat.pos_pow_of_pos (n:=2) (k+1) (by decide))]
    rw [Nat.mod_mul_div_left n 2 (2^k)]
    exact h_ind (n/2)
  . 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]
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ n &&& 2 ^ succ k - 1 = n % 2 ^ succ k
no goals