Theorem: BitTree.toNatHelper_acc (Karatsuba.lean)

State before:
val✝ : Fin 2
x✝ : ℕ
⊢ toNatHelper [] (bit val✝) x✝ = bound [] * x✝ + toNatHelper [] (bit val✝) 0
Tactic:
simpa [toNatHelper, bound_zero] using Nat.add_comm _ _
State after:
no goals

State before:
H : List Unit
left✝ right✝ : BitTree
lhs✝ : Perfect H left✝
rhs✝ : Perfect H right✝
x : ℕ
⊢ toNatHelper (() :: H) (node left✝ right✝) x = bound (() :: H) * x + toNatHelper (() :: H) (node left✝ right✝) 0
Tactic:
simp [bound_cons, toNatHelper, toNatHelper_acc H _ x, toNatHelper_acc H _ (_ + _),
  toNatHelper_acc H _ (toNatHelper _ _ _),
  left_distrib, right_distrib, ← mul_assoc, ← add_assoc]
State after:
no goals