rw [UInt.shiftLeft_zero]
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
x y : α
hn : Nat.zero < length α
⊢ (x, y) = (x, y <<< OfNat.ofNat 0)
no goals