internlm/Lean-Github huggingface dataset:
Theorem: BitTree.karatsubaHelper₁_toNat
Proof 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)))
Proof 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
Theorem: BitTree.karatsubaHelper₁_toNat
Proof 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 _ _)
Proof 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
Theorem: BitTree.karatsubaHelper₁_toNat
Proof 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 _ _
Proof state after:
no goals
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Tactic:
have h: ∀ {H: List Unit} {x y: BitTree} [Perfect H x] [Perfect H y], x.toNat H * y.toNat H % (bound (()::H)) = x.toNat H * y.toNat H :=
  Nat.mod_eq_of_lt (lt_of_lt_of_eq (Nat.mul_lt_mul_for_real (toNat_lt _) (toNat_lt _)) (bound_cons _).symm)
Proof state after:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Tactic:
have karatsuba_toNat: ∀ {x y} [Perfect H x] [Perfect H y], toNat (()::H) (karatsuba H x y) = x.toNat H * y.toNat H :=
  (congrArg _ (karatsuba_eq_mul _ _ _)).trans ((toNat_ofNat _ _).trans h)
Proof state after:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Tactic:
have h₃:
    (karatsubaHelper₃ H
      (karatsuba H
        (addWithCarry xhi xlo 0).2
        (addWithCarry yhi ylo 0).2)
      (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0)) =
    ofNat (()::()::H) ((xhi.toNat H + xlo.toNat H) * (yhi.toNat H + ylo.toNat H)) :=
  toNat_inj (H := (()::()::H))
    (((karatsubaHelper₃_toNat _ _ _  karatsuba_toNat).trans
      (congrArg₂ _
        (addWithCarry_eq_add₀ _ _)
        (addWithCarry_eq_add₀ _ _))).trans
      (toNat_ofNat_lt (mul_lt_bound_cons
        (add_lt_bound_cons (toNat_lt _) (toNat_lt _))
         (add_lt_bound_cons (toNat_lt _) (toNat_lt _)))).symm)
Proof state after:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Tactic:
have h₁:
      (karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
          (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo)))) =
      ofNat (()::()::H) (xlo.toNat H * yhi.toNat H + xhi.toNat H * ylo.toNat H) :=
    toNat_inj (H := (()::()::H))
      (((karatsubaHelper₁_toNat xhi xlo yhi ylo _ _ _ karatsuba_toNat karatsuba_toNat
        (toNat_ofNat_lt (mul_lt_bound_cons
          (add_lt_bound_cons (toNat_lt _) (toNat_lt _))
          (add_lt_bound_cons (toNat_lt _) (toNat_lt _))))).trans
        (add_comm _ _)).trans
        (toNat_ofNat_lt (add_lt_bound_cons
          (mul_lt_bound_cons (toNat_lt _) (toNat_lt _))
          (mul_lt_bound_cons (toNat_lt _) (toNat_lt _)))).symm)
Proof state after:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Tactic:
simp only [karatsuba, h₃, h₁, mkPerfect_id, hi, lo]
Proof state after:
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ node (karatsuba H xhi yhi) (zero (() :: H)) +
        lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)) +
      node (zero (() :: H)) (karatsuba H xlo ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case h₂
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ ofNat (() :: () :: H)
      (toNat (() :: () :: H)
          (node (karatsuba H xhi yhi) (zero (() :: H)) +
            lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo))) +
        toNat (() :: () :: H) (node (zero (() :: H)) (karatsuba H xlo ylo))) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
Tactic:
apply congrArg
Proof state after:
case h₂.h
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ toNat (() :: () :: H)
        (node (karatsuba H xhi yhi) (zero (() :: H)) +
          lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo))) +
      toNat (() :: () :: H) (node (zero (() :: H)) (karatsuba H xlo ylo)) =
    toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo)
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case h₂.h.h₂
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ toNat (() :: () :: H)
        (ofNat (() :: () :: H)
          (toNat (() :: () :: H) (node (karatsuba H xhi yhi) (zero (() :: H))) +
            toNat (() :: () :: H) (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)) *
                bound H %
              bound (() :: () :: H))) +
      toNat (() :: () :: H) (node (zero (() :: H)) (karatsuba H xlo ylo)) =
    toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo)
Tactic:
simp only [toNat_ofNat, toNat_node, toNat_zero, add_zero, karatsuba_toNat,
  mul_zero, zero_add, left_distrib, right_distrib,
  bound_cons, ← mul_assoc, ← add_assoc,
  mul_right_comm _ _ (bound H), mul_comm (toNat _ _) (bound H), mul_comm (_ % _) (bound H),
  Nat.add_mod_mod, add_left_inj]
Proof state after:
case h₂.h.h₂
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ (bound H * bound H * toNat H xhi * toNat H yhi +
        bound H * ((toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo) % (bound H * bound H * bound H * bound H))) %
      (bound H * bound H * bound H * bound H) =
    bound H * bound H * toNat H xhi * toNat H yhi + bound H * toNat H xlo * toNat H yhi +
      bound H * toNat H xhi * toNat H ylo