-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
    (acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
    (hacc : ∀ (idx : Nat) (hidx : idx < w),
                ⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
                  =
                (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (go aig lhs rhs (curr + 1) acc).aig,
          (go aig lhs rhs (curr + 1) acc).vec.get idx hidx,
          assign.toAIGAssignment
        ⟧
          =
        (BitVec.mulRec lexpr rexpr w).getLsbD idx

Proof state:
case isTrue.isFalse
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝¹ : curr + 1 < w
h✝ : ¬aig.isConstant (rhs.get (curr + 1) h✝¹) false = true
hgo :
  go
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).aig
      (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1 + 1)
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).vec =
    res
⊢ ⟦assign.toAIGAssignment,
      {
        aig :=
          (go
              (RefVec.ite
                  (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                      { lhs := acc.cast ⋯,
                        rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
                  { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
                    lhs :=
                      (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                          { lhs := acc.cast ⋯,
                            rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
                    rhs := (acc.cast ⋯).cast ⋯ }).aig
              (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1 + 1)
              (RefVec.ite
                  (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                      { lhs := acc.cast ⋯,
                        rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
                  { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
                    lhs :=
                      (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                          { lhs := acc.cast ⋯,
                            rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
                    rhs := (acc.cast ⋯).cast ⋯ }).vec).aig,
        ref :=
          (go
                  (RefVec.ite
                      (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                          { lhs := acc.cast ⋯,
                            rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
                      { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
                        lhs :=
                          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                              { lhs := acc.cast ⋯,
                                rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
                        rhs := (acc.cast ⋯).cast ⋯ }).aig
                  (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1 + 1)
                  (RefVec.ite
                      (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                          { lhs := acc.cast ⋯,
                            rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
                      { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
                        lhs :=
                          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                              { lhs := acc.cast ⋯,
                                rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
                        rhs := (acc.cast ⋯).cast ⋯ }).vec).vec.get
            idx hidx }⟧ =
    (lexpr.mulRec rexpr w).getLsbD idx

Tactic:
rw [go_denote_eq]

Result:
case isTrue.isFalse.hcurr
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝¹ : curr + 1 < w
h✝ : ¬aig.isConstant (rhs.get (curr + 1) h✝¹) false = true
hgo :
  go
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).aig
      (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1 + 1)
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).vec =
    res
⊢ curr + 1 + 1 ≤ w

case isTrue.isFalse.hleft
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝¹ : curr + 1 < w
h✝ : ¬aig.isConstant (rhs.get (curr + 1) h✝¹) false = true
hgo :
  go
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).aig
      (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1 + 1)
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).vec =
    res
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment,
        {
          aig :=
            (RefVec.ite
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                    { lhs := acc.cast ⋯,
                      rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
                { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
                  lhs :=
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
                  rhs := (acc.cast ⋯).cast ⋯ }).aig,
          ref := (((lhs.cast ⋯).cast ⋯).cast ⋯).get idx hidx }⟧ =
      lexpr.getLsbD idx

case isTrue.isFalse.hright
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝¹ : curr + 1 < w
h✝ : ¬aig.isConstant (rhs.get (curr + 1) h✝¹) false = true
hgo :
  go
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).aig
      (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1 + 1)
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).vec =
    res
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment,
        {
          aig :=
            (RefVec.ite
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                    { lhs := acc.cast ⋯,
                      rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
                { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
                  lhs :=
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
                  rhs := (acc.cast ⋯).cast ⋯ }).aig,
          ref := (((rhs.cast ⋯).cast ⋯).cast ⋯).get idx hidx }⟧ =
      rexpr.getLsbD idx

case isTrue.isFalse.hacc
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝¹ : curr + 1 < w
h✝ : ¬aig.isConstant (rhs.get (curr + 1) h✝¹) false = true
hgo :
  go
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).aig
      (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1 + 1)
      (RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).vec =
    res
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment,
        {
          aig :=
            (RefVec.ite
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                    { lhs := acc.cast ⋯,
                      rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
                { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
                  lhs :=
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
                  rhs := (acc.cast ⋯).cast ⋯ }).aig,
          ref :=
            (RefVec.ite
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).aig
                    { discr := ((rhs.cast ⋯).cast ⋯).get (curr + 1) h✝¹,
                      lhs :=
                        (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).aig
                            { lhs := acc.cast ⋯,
                              rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr + 1 }).vec }).vec,
                      rhs := (acc.cast ⋯).cast ⋯ }).vec.get
              idx hidx }⟧ =
      (lexpr.mulRec rexpr (curr + 1)).getLsbD idx