rw [decide_eq_false this, UInt.when_false_eq]
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a)
      (toNat
        (Nat.fold
          (fun n x => UInt.when (decide ¬UInt.lsb a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
          (Nat.log2RU (length α)) (UInt.when (decide (UInt.lsb a = 0)) (OfNat.ofNat (length α))))) =
    true
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a)
      (toNat
        (Nat.fold
          (fun n x => UInt.when (decide ¬UInt.lsb a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
          (Nat.log2RU (length α)) 0)) =
    true