Theorem: BitTree.add_toNat_negate (Karatsuba.lean)

State before:
H✝ : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H✝ l✝
rhs✝ : Perfect H✝ r✝
⊢ ∀ {m a b c d e : ℕ}, m * a + b + (m * c + d) + e = m * (a + c) + (b + d + e)
Tactic:
intro _ _ _ _ _ _
State after:
H✝ : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H✝ l✝
rhs✝ : Perfect H✝ r✝
m✝ a✝ b✝ c✝ d✝ e✝ : ℕ
⊢ m✝ * a✝ + b✝ + (m✝ * c✝ + d✝) + e✝ = m✝ * (a✝ + c✝) + (b✝ + d✝ + e✝)

State before:
H✝ : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H✝ l✝
rhs✝ : Perfect H✝ r✝
m✝ a✝ b✝ c✝ d✝ e✝ : ℕ
⊢ m✝ * a✝ + b✝ + (m✝ * c✝ + d✝) + e✝ = m✝ * (a✝ + c✝) + (b✝ + d✝ + e✝)
Tactic:
ring
State after:
no goals

State before:
H✝ : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H✝ l✝
rhs✝ : Perfect H✝ r✝
rearrange : ∀ {m a b c d e : ℕ}, m * a + b + (m * c + d) + e = m * (a + c) + (b + d + e)
⊢ toNat (() :: H✝) (node l✝ r✝) + toNat (() :: H✝) (negate (node l✝ r✝)) + 1 = bound (() :: H✝)
Tactic:
simp [toNat_node, rearrange, negate, add_toNat_negate _, ← Nat.mul_succ, Nat.succ_eq_add_one, bound_cons]
State after:
no goals