Theorem: BitTree.karatsuba_eq_mul (Karatsuba.lean)

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)
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))

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)
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))

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)
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))

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)
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))

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]
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))

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)
⊢ 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))
Tactic:
apply Eq.trans
State after:
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)
⊢ 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) =
    ?b

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)
⊢ ?b = ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))

case b
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

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)
⊢ 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) =
    ?b

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)
⊢ ?b = ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))

case b
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
Tactic:
apply add_toNat (()::()::H)
State after:
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))

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
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)

State before:
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)
Tactic:
apply Eq.trans
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)
⊢ 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)) =
    ?h₂.h.b

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)
⊢ ?h₂.h.b = toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo)

case h₂.h.b
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)
⊢ ℕ

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)
        (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)) =
    ?h₂.h.b

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)
⊢ ?h₂.h.b = toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo)

case h₂.h.b
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)
⊢ ℕ
Tactic:
apply congrArg₂
State after:
case h₂.h.h₁.hx
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))) =
    ?h₂.h.h₁.x'

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

State before:
case h₂.h.h₁.hx
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))) =
    ?h₂.h.h₁.x'

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

State before:
case h₂.h.h₁.hx.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)
⊢ node (karatsuba H xhi yhi) (zero (() :: 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 Eq.trans
State after:
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)
⊢ node (karatsuba H xhi yhi) (zero (() :: H)) +
      lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)) =
    ?h₂.h.h₁.hx.h.b

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)
⊢ ?h₂.h.h₁.hx.h.b = ?h₂.h.h₁.hx.a₂

case h₂.h.h₁.hx.h.b
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₁.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)

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)
⊢ node (karatsuba H xhi yhi) (zero (() :: H)) +
      lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)) =
    ?h₂.h.h₁.hx.h.b

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)
⊢ ?h₂.h.h₁.hx.h.b = ?h₂.h.h₁.hx.a₂

case h₂.h.h₁.hx.h.b
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₁.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 add_toNat (()::()::H)
State after:
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)

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
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)

State before:
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)
Tactic:
apply congrArg
State after:
case h₂.h.h₁.hx.h.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) (lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo))) =
    ?h₂.h.h₁.hx.h.h₂.h.a₂

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

State before:
case h₂.h.h₁.hx.h.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) (lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo))) =
    ?h₂.h.h₁.hx.h.h₂.h.a₂

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

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

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]
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

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)
⊢ (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
Tactic:
apply Eq.trans
State after:
case h₂.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) =
    ?h₂.h.h₂.b

case h₂.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)
⊢ ?h₂.h.h₂.b =
    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

case h₂.h.h₂.b
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)
⊢ ℕ

State before:
case h₂.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) =
    ?h₂.h.h₂.b

case h₂.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)
⊢ ?h₂.h.h₂.b =
    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

case h₂.h.h₂.b
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)
⊢ ℕ
Tactic:
apply congrArg₂
State after:
case h₂.h.h₂.h₁.hx
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)) =
    ?h₂.h.h₂.h₁.x'

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.h.h₂.h₁.x'
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₁.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₂
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)
⊢ ?h₂.h.h₂.h₁.x' % ?h₂.h.h₂.h₁.y' =
    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

State before:
case h₂.h.h₂.h₁.hx
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)) =
    ?h₂.h.h₂.h₁.x'

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.h.h₂.h₁.x'
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₁.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₂
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)
⊢ ?h₂.h.h₂.h₁.x' % ?h₂.h.h₂.h₁.y' =
    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
Tactic:
apply congrArg
State after:
case h₂.h.h₂.h₁.hx.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 * ((toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo) % (bound H * bound H * bound H * bound H)) =
    ?h₂.h.h₂.h₁.hx.a₂

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

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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 + ?h₂.h.h₂.h₁.hx.a₂) % ?h₂.h.h₂.h₁.y' =
    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

State before:
case h₂.h.h₂.h₁.hx.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 * ((toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo) % (bound H * bound H * bound H * bound H)) =
    ?h₂.h.h₂.h₁.hx.a₂

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

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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 + ?h₂.h.h₂.h₁.hx.a₂) % ?h₂.h.h₂.h₁.y' =
    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
Tactic:
apply congrArg
State after:
case h₂.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)
⊢ (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo) % (bound H * bound H * bound H * bound H) =
    ?h₂.h.h₂.h₁.hx.h.a₂

case h₂.h.h₂.h₁.hx.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₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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 * ?h₂.h.h₂.h₁.hx.h.a₂) % ?h₂.h.h₂.h₁.y' =
    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

State before:
case h₂.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)
⊢ (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo) % (bound H * bound H * bound H * bound H) =
    ?h₂.h.h₂.h₁.hx.h.a₂

case h₂.h.h₂.h₁.hx.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₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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 * ?h₂.h.h₂.h₁.hx.h.a₂) % ?h₂.h.h₂.h₁.y' =
    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
Tactic:
apply Nat.mod_eq_of_lt
State after:
case h₂.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 xlo * toNat H yhi + toNat H xhi * toNat H ylo < bound H * bound H * bound H * bound H

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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)) %
      ?h₂.h.h₂.h₁.y' =
    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

State before:
case h₂.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 xlo * toNat H yhi + toNat H xhi * toNat H ylo < bound H * bound H * bound H * bound H

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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)) %
      ?h₂.h.h₂.h₁.y' =
    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
Tactic:
apply add_lt_mul_bound
State after:
case h₂.h.h₂.h₁.hx.h.h.h.ha
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 xlo * toNat H yhi ≤ bound H * bound H * bound H

case h₂.h.h₂.h₁.hx.h.h.h.hb
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 xhi * toNat H ylo < bound H * bound H * bound H

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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)) %
      ?h₂.h.h₂.h₁.y' =
    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

State before:
case h₂.h.h₂.h₁.hx.h.h.h.ha
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 xlo * toNat H yhi ≤ bound H * bound H * bound H

case h₂.h.h₂.h₁.hx.h.h.h.hb
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 xhi * toNat H ylo < bound H * bound H * bound H

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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)) %
      ?h₂.h.h₂.h₁.y' =
    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
Tactic:
apply le_trans _
State after:
case h₂.h.h₂.h₁.hx.h.h.h.ha
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)
⊢ ?m.127684 ≤ bound H * bound H * bound 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)
⊢ ℕ

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 xlo * toNat H yhi ≤ ?m.127684

case h₂.h.h₂.h₁.hx.h.h.h.hb
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 xhi * toNat H ylo < bound H * bound H * bound H

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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)) %
      ?h₂.h.h₂.h₁.y' =
    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

State before:
case h₂.h.h₂.h₁.hx.h.h.h.ha
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)
⊢ ?m.127684 ≤ bound H * bound H * bound 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)
⊢ ℕ

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 xlo * toNat H yhi ≤ ?m.127684

case h₂.h.h₂.h₁.hx.h.h.h.hb
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 xhi * toNat H ylo < bound H * bound H * bound H

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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)) %
      ?h₂.h.h₂.h₁.y' =
    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
Tactic:
apply Nat.le_mul_of_pos_right (bound_pos _)
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)
⊢ toNat H xlo * toNat H yhi ≤ bound H * bound H

case h₂.h.h₂.h₁.hx.h.h.h.hb
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 xhi * toNat H ylo < bound H * bound H * bound H

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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)) %
      ?h₂.h.h₂.h₁.y' =
    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

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)
⊢ toNat H xlo * toNat H yhi ≤ bound H * bound H

case h₂.h.h₂.h₁.hx.h.h.h.hb
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 xhi * toNat H ylo < bound H * bound H * bound H

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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)) %
      ?h₂.h.h₂.h₁.y' =
    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
Tactic:
apply le_of_lt
State after:
case 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)
⊢ toNat H xlo * toNat H yhi < bound H * bound H

case h₂.h.h₂.h₁.hx.h.h.h.hb
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 xhi * toNat H ylo < bound H * bound H * bound H

case h₂.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)
⊢ bound H * bound H * bound H * bound H = ?h₂.h.h₂.h₁.y'

case h₂.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₂
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)) %
      ?h₂.h.h₂.h₁.y' =
    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