Theorem: BitTree.karatsubaHelper₃_toNat (Karatsuba.lean)

State before:
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)
Tactic:
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 _)))
State after:
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)

State before:
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)
Tactic:
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 _))
State after:
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)

State before:
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)
Tactic:
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 _)))))
State after:
no goals