case inl hlt =>
  rw [decide_eq_false (Nat.not_le_of_gt hlt), Bool.false_and]
  exact shiftLeft_getBit_lt n k hlt
n k i : Nat
hlt : i < k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
no goals