Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case h₂.h.h₁.hx.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)
⊢ ofNat (() :: () :: H)
      (toNat (() :: () :: H) (node (karatsuba H xhi yhi) (zero (() :: H))) +
        toNat (() :: () :: H)
          (lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)))) =
    ?h₂.h.h₁.hx.a₂

case h₂.h.h₁.hx.a₂
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)
⊢ BitTree

case h₂.h.h₁.hy
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 (zero (() :: H)) (karatsuba H xlo ylo)) = ?h₂.h.h₁.y'

case h₂.h.h₁.y'
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)
⊢ ℕ

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) ?h₂.h.h₁.hx.a₂ + ?h₂.h.h₁.y' = toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo)
Tactic:
apply congrArg
Proof state after:
case h₂.h.h₁.hx.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) (node (karatsuba H xhi yhi) (zero (() :: H))) +
      toNat (() :: () :: H)
        (lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo))) =
    ?h₂.h.h₁.hx.h.h₂.a₂

case h₂.h.h₁.hx.h.h₂.a₂
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)
⊢ ℕ

case h₂.h.h₁.hy
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 (zero (() :: H)) (karatsuba H xlo ylo)) = ?h₂.h.h₁.y'

case h₂.h.h₁.y'
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)
⊢ ℕ

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) ?h₂.h.h₁.hx.h.h₂.a₂) + ?h₂.h.h₁.y' =
    toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo)