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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ UInt.when false a = 0
Tactic:
unfold UInt.when
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 - ofBool false &&& a = 0

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 - ofBool false &&& a = 0
Tactic:
rw [UInt.ofBool_false, UInt.sub_self, UInt.zero_land a]
State after:
no goals