-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
theorem go_decl_eq (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
     (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
        (go aig curr falseRef trueRef n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastUdivOutput aig w
curr✝¹ curr✝ : Nat
hgo :
  {
      aig :=
        (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯) (trueRef.cast ⋯)
            (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).aig,
      q :=
        (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯) (trueRef.cast ⋯)
            (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).q,
      r :=
        (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯) (trueRef.cast ⋯)
            (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).r,
      hle := ⋯ } =
    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 h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastUdivOutput aig w
curr✝¹ curr✝ : Nat
hgo :
  {
      aig :=
        (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯) (trueRef.cast ⋯)
            (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).aig,
      q :=
        (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯) (trueRef.cast ⋯)
            (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).q,
      r :=
        (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯) (trueRef.cast ⋯)
            (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
            (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).r,
      hle := ⋯ } =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        {
                aig :=
                  (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                      (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯)
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).aig,
                q :=
                  (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                      (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯)
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).q,
                r :=
                  (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                      (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯)
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                      (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).r,
                hle := ⋯ }.aig.decls.size),
    {
              aig :=
                (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                    (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).aig,
              q :=
                (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                    (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).q,
              r :=
                (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                    (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).r,
              hle := ⋯ }.aig.decls[idx] =
      aig.decls[idx]