Theorem: bitvec_229 (Eval/bitvec_229.lean)

State before:
⊢ ∀ (X C1 Op1 : BitVec 64), (X + C1) * Op1 = X * Op1 + C1 * Op1
Tactic:
intros
State after:
X✝ C1✝ Op1✝ : BitVec 64
⊢ (X✝ + C1✝) * Op1✝ = X✝ * Op1✝ + C1✝ * Op1✝

State before:
X✝ C1✝ Op1✝ : BitVec 64
⊢ (X✝ + C1✝) * Op1✝ = X✝ * Op1✝ + C1✝ * Op1✝
Tactic:
bv_decide
State after:
no goals