case succ n h_ind =>
  dsimp [bitIndices.aux]
  cases hbit : UInt.getBit a n
  case false =>
    simp [h_ind]
    intro h
    have : i ≠ n := λ hcontra => by cases (hbit ▸ hcontra ▸ h)
    constructor
    . exact Nat.lt_succ_of_lt
    . intro hle; exact Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hle) ‹i≠n›
  case true =>
    simp
    constructor
    . intro h
      cases h
      case inl h => cases h; exact ⟨i.lt_succ_self, hbit⟩
      case inr h => exact ⟨Nat.le.step (h_ind.mp h).left, (h_ind.mp h).right⟩
    . intro h
      cases (Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h.left))
      case inl hlt => exact Or.inr (h_ind.mpr ⟨hlt, h.right⟩)
      case inr heq => cases heq; exact Or.inl rfl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ i ∈ bitIndices.aux a (Nat.succ n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true
no goals