-- 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:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastUdivOutput aig w
hgo : go aig curr falseRef trueRef n d wn wr q r = 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:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastUdivOutput aig w
hgo :
  (match curr with
    | 0 => { aig := aig, q := q, r := r, hle := ⋯ }
    | curr.succ =>
      let res := blastDivSubtractShift aig falseRef trueRef n d wn wr q r;
      let aig_1 := res.aig;
      let wn_1 := res.wn;
      let wr_1 := res.wr;
      let q_1 := res.q;
      let r_1 := res.r;
      let_fun this := ⋯;
      let falseRef_1 := falseRef.cast this;
      let trueRef_1 := trueRef.cast this;
      let n_1 := n.cast this;
      let d_1 := d.cast this;
      let res := go aig_1 curr falseRef_1 trueRef_1 n_1 d_1 wn_1 wr_1 q_1 r_1;
      let aig_2 := res.aig;
      let q_2 := res.q;
      let r_2 := res.r;
      let_fun this := ⋯;
      { aig := aig_2, q := q_2, r := r_2, hle := this }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastUdivOutput aig w
hgo :
  (match curr with
    | 0 => { aig := aig, q := q, r := r, hle := ⋯ }
    | curr.succ =>
      let res := blastDivSubtractShift aig falseRef trueRef n d wn wr q r;
      let aig_1 := res.aig;
      let wn_1 := res.wn;
      let wr_1 := res.wr;
      let q_1 := res.q;
      let r_1 := res.r;
      let_fun this := ⋯;
      let falseRef_1 := falseRef.cast this;
      let trueRef_1 := trueRef.cast this;
      let n_1 := n.cast this;
      let d_1 := d.cast this;
      let res := go aig_1 curr falseRef_1 trueRef_1 n_1 d_1 wn_1 wr_1 q_1 r_1;
      let aig_2 := res.aig;
      let q_2 := res.q;
      let r_2 := res.r;
      let_fun this := ⋯;
      { aig := aig_2, q := q_2, r := r_2, hle := this }) =
    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:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastUdivOutput aig w
hgo :
  (match curr with
    | 0 => { aig := aig, q := q, r := r, hle := ⋯ }
    | curr.succ =>
      {
        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]

Proof state:
case h_2.h2.a
α : 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
⊢ idx < ?h_2.h2.m

Tactic:
exact h1

Result:
no goals