case inr hge =>
  have := calc
    false = UInt.getBit x i := (UInt.getBit_high x i hge).symm
    _     = true := ‹_›
  cases this
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
hge : i ≥ length α
⊢ i < length α
no goals