let f' : α → Nat → α → α :=
  λ a₁ n x => UInt.when ((a₁ &&& bitmask (OfNat.ofNat n)) ≠ 0) (1 <<< OfNat.ofNat (α:=α) n) ||| x
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
⊢ ∀ (a : α), UInt.ctz a = UInt.ctz' a
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
⊢ ∀ (a : α), UInt.ctz a = UInt.ctz' a