have := calc
  1 ≤ length α := hpos
  _ < 2^length α := Nat.exp_lt_pow _ .refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
this : 1 < 2 ^ length α
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)