case inr hpos =>
  rw [decide_eq_true hpos, Bool.true_and]
  dsimp [UInt.getBit]; rw [UInt.toNat_ofNat]
  have := calc
    1 ≤ length α := hpos
    _ < 2^length α := Nat.exp_lt_pow _ .refl
  rw [Nat.mod_eq_of_lt this]
  calc
    Nat.getBit 1 i = decide (0 = i) := Nat.getBit_two_pow 0 i
    _              = decide (i = 0) := decide_eq_decide.mpr ⟨Eq.symm, Eq.symm⟩
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
no goals