-- 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 :
  (let res := blastShiftLeftConst aig { vec := lhs, distance := curr };
    let aig_1 := res.aig;
    let shifted := res.vec;
    let_fun this := ⋯;
    let lhs_1 := lhs.cast this;
    let rhs_1 := rhs.cast this;
    let acc_1 := acc.cast this;
    let res := blastAdd aig_1 { lhs := acc_1, rhs := shifted };
    let aig_2 := res.aig;
    let added := res.vec;
    let_fun this_1 := ⋯;
    let lhs_2 := lhs_1.cast this_1;
    let rhs_2 := rhs_1.cast this_1;
    let acc_2 := acc_1.cast this_1;
    let res := AIG.RefVec.ite aig_2 { discr := rhs_2.get curr h✝¹, lhs := added, rhs := acc_2 };
    let aig_3 := res.aig;
    let acc_3 := res.vec;
    let_fun this := ⋯;
    let lhs := lhs_2.cast this;
    let rhs := rhs_2.cast this;
    go aig_3 lhs rhs (curr + 1) acc_3) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
dsimp only at hgo

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 < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Proof state:
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
res : AIG.RefVecEntry BVBit w
hgo : go aig lhs rhs curr acc = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
unfold go at hgo

Result:
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
res : AIG.RefVecEntry BVBit w
hgo :
  (if h : curr < w then
      if aig.isConstant (rhs.get curr h) false = true then go aig lhs rhs (curr + 1) acc
      else
        let res := blastShiftLeftConst aig { vec := lhs, distance := curr };
        let aig_1 := res.aig;
        let shifted := res.vec;
        let_fun this := ⋯;
        let lhs_1 := lhs.cast this;
        let rhs_1 := rhs.cast this;
        let acc_1 := acc.cast this;
        let res := blastAdd aig_1 { lhs := acc_1, rhs := shifted };
        let aig_2 := res.aig;
        let added := res.vec;
        let_fun this_1 := ⋯;
        let lhs_2 := lhs_1.cast this_1;
        let rhs_2 := rhs_1.cast this_1;
        let acc_2 := acc_1.cast this_1;
        let res := AIG.RefVec.ite aig_2 { discr := rhs_2.get curr h, lhs := added, rhs := acc_2 };
        let aig_3 := res.aig;
        let acc_3 := res.vec;
        let_fun this := ⋯;
        let lhs := lhs_2.cast this;
        let rhs := rhs_2.cast this;
        go aig_3 lhs rhs (curr + 1) acc_3
    else { aig := aig, vec := acc }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]