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
this : 1 < 2 ^ length α
⊢ Nat.getBit 1 i = decide (i = 0)
no goals