simpa only [karatsubaHelper₃,
  add_toNat (()::()::H), mulBit_ofNat, mulBit'_ofNat,
  bound_cons, ← mul_assoc, mul_zero,
  mul_right_comm _ _ (bound H),
  mul_right_comm _ (toNat _ _) (Fin.val _),
  mul_comm (toNat _ _) (bound H),
  Nat.add_right_comm _ (_ * toNat H y) (_ * toNat H x),
  Nat.add_right_comm _ (toNat _ _ * toNat _ _),
  left_distrib, right_distrib,
  toNat_ofNat, toNat_node, h, toNat_zero,
  add_zero, zero_add, Nat.mod_add_mod, ← Nat.add_assoc,
  h₀, h₁] using Nat.mod_eq_of_lt (lt_of_eq_of_lt
  (Nat.add_assoc _ _ _)
  (add_lt_mul_bound
    (add_le_mul_bound
      (le_trans
        (mul_le_of_le_one_right' (Nat.le_of_lt_succ (Fin.isLt _)))
        (mul_le_of_le_one_right' (Nat.le_of_lt_succ (Fin.isLt _))))
      (Nat.mul_le_mul
        (mul_le_of_le_one_right' (Nat.le_of_lt_succ (Fin.isLt _)))
        (le_of_lt (toNat_lt _))))
    (add_lt_mul_bound
      (Nat.mul_le_mul (mul_le_of_le_one_right' (Nat.le_of_lt_succ (Fin.isLt _))) (le_of_lt (toNat_lt _)))
      (Nat.mul_lt_mul_for_real (toNat_lt _) (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
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)
no goals