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

State before:
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₃
⊢ toNat (() :: H) z₀ = toNat H xlo * toNat H ylo →
    toNat (() :: H) z₂ = toNat H xhi * toNat H yhi →
      toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo) →
        toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) =
          toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
Tactic:
intro h₀ h₂ h₃
State after:
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)
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi

State before:
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)
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
Tactic:
have h: ∀ {H: List Unit} {a b c d e f: BitTree} [Perfect H a] [Perfect H a] [Perfect H b] [Perfect H c] [Perfect H d] [Perfect H e] [Perfect H f],
    (a.toNat H * b.toNat H + c.toNat H * d.toNat H + e.toNat H * f.toNat H) % (bound H * bound H * bound H * bound H) =
    a.toNat H * b.toNat H + c.toNat H * d.toNat H + e.toNat H * f.toNat H :=
  Nat.mod_eq_of_lt (add_lt_mul_bound
    (add_le_mul_bound
      (Nat.mul_le_mul
        (le_of_lt (toNat_lt _))
        (le_of_lt (toNat_lt _)))
      (Nat.mul_le_mul
        (le_of_lt (toNat_lt _))
        (le_of_lt (toNat_lt _))))
     (add_lt_mul_bound
      (Nat.mul_le_mul
        (le_of_lt (toNat_lt _))
        (le_of_lt (toNat_lt _)))
      (Nat.mul_lt_mul_for_real
        (bound_pos _)
        (bound_pos _))))
State after:
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
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi

State before:
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
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
Tactic:
have h': ∀ {H: List Unit} {a b c d: BitTree} [Perfect H a] [Perfect H b] [Perfect H c] [Perfect H d],
    (a.toNat H * b.toNat H + c.toNat H * d.toNat H) % (bound H * bound H * bound H * bound H) =
    a.toNat H * b.toNat H + c.toNat H * d.toNat H :=
  (congrArg₂ _ (congrArg _ (congrArg₂ _
    toNat_zero.symm toNat_zero.symm)) rfl).trans
  (h.trans (congrArg _ (congrArg₂ _
    toNat_zero toNat_zero)))
State after:
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
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi

State before:
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
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
Tactic:
have hs: ∀ {a b c: ℕ}, a + b + c - b = a + c :=
  (congrArg₂ _ (Nat.add_right_comm _ _ _) rfl).trans (Nat.add_sub_cancel _ _)
State after:
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

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