Theorem: BitTree.addWithCarry_eq_ofNat_add (Karatsuba.lean)

State before:
val✝¹ val✝ x✝ : Fin 2
⊢ addWithCarry (bit val✝¹) (bit val✝) x✝ =
    ({ val := (toNat [] (bit val✝¹) + toNat [] (bit val✝) + ↑x✝) / bound [],
        isLt := (_ : (toNat [] (bit val✝¹) + toNat [] (bit val✝) + ↑x✝) / bound [] < 2) },
      ofNat [] (toNat [] (bit val✝¹) + toNat [] (bit val✝) + ↑x✝))
Tactic:
simp [addWithCarry, toNat, toNatHelper, bound_zero]
State after:
no goals

State before:
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
⊢ ∀ {m xh xl yh yl c : ℕ}, m * xh + xl + (m * yh + yl) + c = m * (xh + yh) + (xl + yl + c)
Tactic:
intro _ _ _ _ _ _
State after:
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
m✝ xh✝ xl✝ yh✝ yl✝ c✝ : ℕ
⊢ m✝ * xh✝ + xl✝ + (m✝ * yh✝ + yl✝) + c✝ = m✝ * (xh✝ + yh✝) + (xl✝ + yl✝ + c✝)

State before:
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
m✝ xh✝ xl✝ yh✝ yl✝ c✝ : ℕ
⊢ m✝ * xh✝ + xl✝ + (m✝ * yh✝ + yl✝) + c✝ = m✝ * (xh✝ + yh✝) + (xl✝ + yl✝ + c✝)
Tactic:
ring
State after:
no goals

State before:
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
rearrange : ∀ {m xh xl yh yl c : ℕ}, m * xh + xl + (m * yh + yl) + c = m * (xh + yh) + (xl + yl + c)
⊢ addWithCarry (node l✝¹ r✝¹) (node l✝ r✝) x✝ =
    ({ val := (toNat (() :: H) (node l✝¹ r✝¹) + toNat (() :: H) (node l✝ r✝) + ↑x✝) / bound (() :: H),
        isLt := (_ : (toNat (() :: H) (node l✝¹ r✝¹) + toNat (() :: H) (node l✝ r✝) + ↑x✝) / bound (() :: H) < 2) },
      ofNat (() :: H) (toNat (() :: H) (node l✝¹ r✝¹) + toNat (() :: H) (node l✝ r✝) + ↑x✝))
Tactic:
simp [addWithCarry, @addWithCarry_eq_ofNat_add H, rearrange, toNat_node, bound_cons,
  ← Nat.div_div_eq_div_mul, Nat.mul_add_div (bound_pos _),  divBound]
State after:
no goals