have h₁: ∀ {x: Fin 2} {H: List Unit} {y: BitTree} [Perfect H y], x.val * y.toNat H % bound H = x.val * y.toNat H
  | 0, _, _, _ => Nat.mod_eq_of_lt (lt_of_eq_of_lt (zero_mul _) (bound_pos _))
  | 1, _, _, _ => Nat.mod_eq_of_lt (lt_of_eq_of_lt (one_mul _) (toNat_lt _))
H : List Unit
xy : BitTree
xc : Fin 2
x : BitTree
yc : Fin 2
y : BitTree
x✝² : Perfect (() :: H) xy
x✝¹ : Perfect H (xc, x).2
x✝ : Perfect H (yc, y).2
h : toNat (() :: H) xy = toNat H (xc, x).2 * toNat H (yc, y).2
h₀ : ∀ {x y : Fin 2} {H : List Unit}, ↑x * ↑y % (bound H * bound H) = ↑x * ↑y
⊢ toNat (() :: () :: H) (karatsubaHelper₃ H xy (xc, x) (yc, y)) =
    (bound H * ↑(xc, x).1 + toNat H (xc, x).2) * (bound H * ↑(yc, y).1 + toNat H (yc, y).2)
H : List Unit
xy : BitTree
xc : Fin 2
x : BitTree
yc : Fin 2
y : BitTree
x✝² : Perfect (() :: H) xy
x✝¹ : Perfect H (xc, x).2
x✝ : Perfect H (yc, y).2
h : toNat (() :: H) xy = toNat H (xc, x).2 * toNat H (yc, y).2
h₀ : ∀ {x y : Fin 2} {H : List Unit}, ↑x * ↑y % (bound H * bound H) = ↑x * ↑y
h₁ : ∀ {x : Fin 2} {H : List Unit} {y : BitTree} [inst : Perfect H y], ↑x * toNat H y % bound H = ↑x * toNat H y
⊢ toNat (() :: () :: H) (karatsubaHelper₃ H xy (xc, x) (yc, y)) =
    (bound H * ↑(xc, x).1 + toNat H (xc, x).2) * (bound H * ↑(yc, y).1 + toNat H (yc, y).2)