case true =>
  calc
    true = n.lsb.getBit i := Eq.symm $ n.lsb_getBit_iff.mpr ⟨hni, h_ind⟩
    _    = Nat.getBit 0 i := by rw [h]
    _    = false          := Nat.zero_getBit i
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = true
⊢ true = false
no goals