-- 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.h2
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
⊢ idx <
    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
            { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig.decls.size

Tactic:
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastAdd)

Result:
case isTrue.isFalse.h2.h
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
⊢ idx < (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig.decls.size

Proof state:
case isTrue.isTrue
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 lhs rhs (curr + 1) acc = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
rw [← hgo]

Result:
case isTrue.isTrue
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 lhs rhs (curr + 1) acc = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs rhs (curr + 1) acc).aig.decls.size),
    (go aig lhs rhs (curr + 1) acc).aig.decls[idx] = aig.decls[idx]