Theorem: UInt.lsb_zero (Algdata/Classes/UInt.lean)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ UInt.lsb 0 = 0
Tactic:
unfold UInt.lsb
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ 0 ^^^ 0 &&& 0 - 1 = 0

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ 0 ^^^ 0 &&& 0 - 1 = 0
Tactic:
rw [UInt.zero_land, UInt.zero_xor]
State after:
no goals