case succ i h_ind =>
  dsimp [getBit]
  cases k
  case zero =>
    conv => change getBit 0 i = false
    simp
  case succ k =>
    conv => lhs; arg 1; change 2^k*2/2; simp
    have : k = i ↔ k.succ = i.succ := ⟨λ h => h ▸ rfl, λ h => Nat.succ.inj h⟩
    rw [h_ind, decide_eq_decide.mpr this]
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) (succ i) = decide (k = succ i)
no goals