Theorem: BVDecide.Normalize.BitVec.lt_ult (LeanSAT/Reflect/Tactics/Normalize/Canonicalize.lean)

State before:
w : Nat
x y : BitVec w
⊢ (x < y) = (x.ult y = true)
Tactic:
rw [BitVec.ult]
State after:
w : Nat
x y : BitVec w
⊢ (x < y) = (decide (x.toNat < y.toNat) = true)

State before:
w : Nat
x y : BitVec w
⊢ (x < y) = (decide (x.toNat < y.toNat) = true)
Tactic:
rw [LT.lt]
State after:
w : Nat
x y : BitVec w
⊢ BitVec.instLT.1 x y = (decide (x.toNat < y.toNat) = true)

State before:
w : Nat
x y : BitVec w
⊢ BitVec.instLT.1 x y = (decide (x.toNat < y.toNat) = true)
Tactic:
rw [BitVec.instLT]
State after:
w : Nat
x y : BitVec w
⊢ { lt := fun x x_1 => x.toNat < x_1.toNat }.1 x y = (decide (x.toNat < y.toNat) = true)

State before:
w : Nat
x y : BitVec w
⊢ { lt := fun x x_1 => x.toNat < x_1.toNat }.1 x y = (decide (x.toNat < y.toNat) = true)
Tactic:
simp
State after:
no goals