-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
theorem go_decl_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (acc : AIG.RefVec aig w)
    (lhs rhs : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
       (go aig lhs rhs curr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case isTrue.isFalse
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
res : AIG.RefVecEntry BVBit w
h✝¹ : curr < w
h✝ : ¬aig.isConstant (rhs.get curr h✝¹) false = true
hgo :
  go
      (AIG.RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).aig
      (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1)
      (AIG.RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).vec =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go
                (AIG.RefVec.ite
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                    { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                      lhs :=
                        (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                            { lhs := acc.cast ⋯,
                              rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                      rhs := (acc.cast ⋯).cast ⋯ }).aig
                (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1)
                (AIG.RefVec.ite
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                    { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                      lhs :=
                        (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                            { lhs := acc.cast ⋯,
                              rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                      rhs := (acc.cast ⋯).cast ⋯ }).vec).aig.decls.size),
    (go
              (AIG.RefVec.ite
                  (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                      { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                  { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                    lhs :=
                      (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                          { lhs := acc.cast ⋯,
                            rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                    rhs := (acc.cast ⋯).cast ⋯ }).aig
              (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1)
              (AIG.RefVec.ite
                  (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                      { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                  { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                    lhs :=
                      (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                          { lhs := acc.cast ⋯,
                            rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                    rhs := (acc.cast ⋯).cast ⋯ }).vec).aig.decls[idx] =
      aig.decls[idx]

Tactic:
intro idx h1 h2

Result:
case isTrue.isFalse
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
res : AIG.RefVecEntry BVBit w
h✝¹ : curr < w
h✝ : ¬aig.isConstant (rhs.get curr h✝¹) false = true
hgo :
  go
      (AIG.RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).aig
      (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1)
      (AIG.RefVec.ite
          (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
              { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
          { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
            lhs :=
              (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                  { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
            rhs := (acc.cast ⋯).cast ⋯ }).vec =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go
            (AIG.RefVec.ite
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                    { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                  lhs :=
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                  rhs := (acc.cast ⋯).cast ⋯ }).aig
            (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1)
            (AIG.RefVec.ite
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                    { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                  lhs :=
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                  rhs := (acc.cast ⋯).cast ⋯ }).vec).aig.decls.size
⊢ (go
            (AIG.RefVec.ite
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                    { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                  lhs :=
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                  rhs := (acc.cast ⋯).cast ⋯ }).aig
            (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1)
            (AIG.RefVec.ite
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                    { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                  lhs :=
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                  rhs := (acc.cast ⋯).cast ⋯ }).vec).aig.decls[idx] =
    aig.decls[idx]