simpa only [karatsubaHelper₁,
  sub_toNat (()::()::H), h₃, left_distrib, right_distrib, add_comm (xhi.toNat _ * yhi.toNat _), ←
  add_assoc, add_right_comm _ (xhi.toNat _ * yhi.toNat _), bound_cons, ← mul_assoc, toNat_node,
  toNat_zero, mul_zero, h₂, zero_add, add_tsub_cancel_right, toNat_ofNat, Nat.add_mod_right, h,
  h₀, hs, h'] using Nat.add_comm _ _
H : List Unit
xhi xlo yhi ylo : BitTree
inst✝⁶ : Perfect H xhi
inst✝⁵ : Perfect H xlo
inst✝⁴ : Perfect H yhi
inst✝³ : Perfect H ylo
z₀ z₂ z₃ : BitTree
inst✝² : Perfect (() :: H) z₀
inst✝¹ : Perfect (() :: H) z₂
inst✝ : Perfect (() :: () :: H) z₃
h₀ : toNat (() :: H) z₀ = toNat H xlo * toNat H ylo
h₂ : toNat (() :: H) z₂ = toNat H xhi * toNat H yhi
h₃ : toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo)
h :
  ∀ {H : List Unit} {a b c d e f : BitTree} [inst : Perfect H a] [inst : Perfect H a] [inst : Perfect H b]
    [inst : Perfect H c] [inst : Perfect H d] [inst : Perfect H e] [inst : Perfect H f],
    (toNat H a * toNat H b + toNat H c * toNat H d + toNat H e * toNat H f) % (bound H * bound H * bound H * bound H) =
      toNat H a * toNat H b + toNat H c * toNat H d + toNat H e * toNat H f
h' :
  ∀ {H : List Unit} {a b c d : BitTree} [inst : Perfect H a] [inst : Perfect H b] [inst : Perfect H c]
    [inst : Perfect H d],
    (toNat H a * toNat H b + toNat H c * toNat H d) % (bound H * bound H * bound H * bound H) =
      toNat H a * toNat H b + toNat H c * toNat H d
hs : ∀ {a b c : ℕ}, a + b + c - b = a + c
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
no goals