case succ k h_ind =>
  cases i
  case zero =>
    dsimp [Nat.getBit]; apply decide_eq_decide.mpr
    have := calc
      (2^k.succ - 1) % 2
        = (2^k*2 - 1) % 2 := by rw [Nat.pow_succ]
      _ = (2-1)%2 :=
        Nat.mul_sub_mod_right (Nat.pos_pow_of_pos (n:=2) _ (by decide)) (.step .refl)
      _ = 1 := rfl
    rw [this]
    constructor <;> intros; exact k.zero_lt_succ; rfl
  case succ i =>
    have := calc
      (2^k.succ - 1).getBit i.succ
        = ((2^k*2 - 1)/2).getBit i := by rw [Nat.pow_succ, Nat.getBit]
      _ = (2^k - 1).getBit i :=
        by rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]; rfl
    rw [this, h_ind]; apply decide_eq_decide.mpr
    exact ⟨Nat.succ_lt_succ, Nat.lt_of_succ_lt_succ⟩
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) i = decide (i < succ k)
no goals