case step i hstep =>
  dsimp [getBit]
  exact h_ind ‹n/2 < 2^k› i (Nat.le_of_succ_le hstep)
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
i : Nat
hstep : Nat.le (succ k) i
⊢ getBit n (succ i) = false
no goals