have h₀: ∀ {x y: Fin 2} {H: List Unit}, x.val * y.val % (bound H * bound H) = x.val * y.val :=
  Nat.mod_eq_of_lt (Nat.mul_lt_mul_for_real
    (lt_of_lt_of_le (Fin.isLt _) (two_le_bound _))
    (lt_of_lt_of_le (Fin.isLt _) (two_le_bound _)))
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
⊢ 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
⊢ 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)