if hlength : length α = 0
then simp only [UInt.toNat_of_length_eq_zero hlength]
else
have hlength : length α > 0 := Nat.pos_of_ne_zero hlength
have : 1 % 2^length α = 1 :=
  Nat.mod_eq_of_lt $ calc
    1 = 2^0 := Eq.symm $ Nat.pow_zero 2
    _ < 2^length α := Nat.pow_lt_pow_right (n:=2) .refl ‹length α > 0›
suffices (UInt.toNat a &&& UInt.toNat (a-1)) = (UInt.toNat a &&& (UInt.toNat a - 1)) by
  unfold UInt.lsb; simp only [UInt.toNat_xor, UInt.toNat_land]
  rw [this]; rfl
rw [UInt.toNat_sub, UInt.toNat_ofNat, ‹1%2^length α = 1›]
cases ha : UInt.toNat a
case zero => simp
case succ n =>
  have := calc
    n.succ + (2^length α - 1)
      = n.succ + 2^length α - 1 :=
        by rw [Nat.add_sub_assoc (Nat.pos_pow_of_pos (n:=2) (length α) (by decide))]
    _ = (n + 2^length α).succ - 1 := by rw [Nat.succ_add]
    _ = n + 2^length α := Nat.succ_sub_one ..
  rw [this, Nat.add_mod_right]
  have := calc
    n < n.succ := n.lt_succ_self
    _ = toNat a := ha.symm
    _ < 2^length α := UInt.toNat_lt a
  simp only [Nat.mod_eq_of_lt this, Nat.succ_sub_one]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
no goals