-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
    (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
    (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
    (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
    (hfalse : ⟦aig, falseRef, assign⟧ = false)
    (htrue : ⟦aig, trueRef, assign⟧ = true)
      :
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q.get idx hidx,
        assign
      ⟧
        =
      (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
lhs rhs : BitVec w
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
qbv rbv : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx
hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (let wn_1 := wn - 1;
            let wr := wr + 1;
            let res := blastShiftConcat aig { lhs := r, bit := n.getD wn_1 falseRef };
            let aig_1 := res.aig;
            let r' := res.vec;
            let_fun this := ⋯;
            let falseRef_1 := falseRef.cast this;
            let trueRef_1 := trueRef.cast this;
            let d_1 := d.cast this;
            let q_1 := q.cast this;
            let res_1 := blastShiftConcat aig_1 { lhs := q_1, bit := falseRef_1 };
            let aig_2 := res_1.aig;
            let posQ := res_1.vec;
            let_fun this_1 := ⋯;
            let trueRef_2 := trueRef_1.cast this_1;
            let d_2 := d_1.cast this_1;
            let q_2 := q_1.cast this_1;
            let r' := r'.cast this_1;
            let res := blastShiftConcat aig_2 { lhs := q_2, bit := trueRef_2 };
            let aig_3 := res.aig;
            let negQ := res.vec;
            let_fun this_2 := ⋯;
            let d_3 := d_2.cast this_2;
            let r' := r'.cast this_2;
            let posQ := posQ.cast this_2;
            let res_2 := blastSub aig_3 { lhs := r', rhs := d_3 };
            let aig_4 := res_2.aig;
            let negR := res_2.vec;
            let_fun this_3 := ⋯;
            let d_4 := d_3.cast this_3;
            let r'_1 := r'.cast this_3;
            let posQ := posQ.cast this_3;
            let negQ := negQ.cast this_3;
            let posR := r'_1;
            let res := BVPred.mkUlt aig_4 { lhs := r'_1, rhs := d_4 };
            let aig_5 := res.aig;
            let discr := res.ref;
            let_fun this_4 := ⋯;
            let posQ := posQ.cast this_4;
            let negQ := negQ.cast this_4;
            let posR := posR.cast this_4;
            let negR := negR.cast this_4;
            let res_3 := RefVec.ite aig_5 { discr := discr, lhs := posQ, rhs := negQ };
            let aig_6 := res_3.aig;
            let nextQ := res_3.vec;
            let_fun this_5 := ⋯;
            let posR := ⋯;
            ⋯).aig,
        ref :=
          (let wn_1 := wn - 1;
                let wr := wr + 1;
                let res := blastShiftConcat aig { lhs := r, bit := n.getD wn_1 falseRef };
                let aig_1 := res.aig;
                let r' := res.vec;
                let_fun this := ⋯;
                let falseRef_1 := falseRef.cast this;
                let trueRef_1 := trueRef.cast this;
                let d_1 := d.cast this;
                let q_1 := q.cast this;
                let res_1 := blastShiftConcat aig_1 { lhs := q_1, bit := falseRef_1 };
                let aig_2 := res_1.aig;
                let posQ := res_1.vec;
                let_fun this_1 := ⋯;
                let trueRef_2 := trueRef_1.cast this_1;
                let d_2 := d_1.cast this_1;
                let q_2 := q_1.cast this_1;
                let r' := r'.cast this_1;
                let res := blastShiftConcat aig_2 { lhs := q_2, bit := trueRef_2 };
                let aig_3 := res.aig;
                let negQ := res.vec;
                let_fun this_2 := ⋯;
                let d_3 := d_2.cast this_2;
                let r' := r'.cast this_2;
                let posQ := posQ.cast this_2;
                let res_2 := blastSub aig_3 { lhs := r', rhs := d_3 };
                let aig_4 := res_2.aig;
                let negR := res_2.vec;
                let_fun this_3 := ⋯;
                let d_4 := d_3.cast this_3;
                let r'_1 := r'.cast this_3;
                let posQ := posQ.cast this_3;
                let negQ := negQ.cast this_3;
                let posR := r'_1;
                let res := BVPred.mkUlt aig_4 { lhs := r'_1, rhs := d_4 };
                let aig_5 := res.aig;
                let discr := res.ref;
                let_fun this_4 := ⋯;
                let posQ := posQ.cast this_4;
                let negQ := negQ.cast this_4;
                let posR := posR.cast this_4;
                let negR := negR.cast this_4;
                let res_3 := RefVec.ite aig_5 { discr := discr, lhs := posQ, rhs := negQ };
                let aig_6 := res_3.aig;
                let nextQ := res_3.vec;
                let_fun this_5 := ⋯;
                ⋯).q.get
            idx hidx }⟧ =
    (match { n := lhs, d := rhs } with
          | { n := n, d := d } =>
            let wn_1 := { wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1;
            let wr_1 := { wn := wn, wr := wr, q := qbv, r := rbv }.wr + 1;
            let r' := { wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat (n.getLsbD wn_1);
            if r' < d then
              { wn := wn_1, wr := wr_1, q := { wn := wn, wr := wr, q := qbv, r := rbv }.q.shiftConcat false, r := r' }
            else
              { wn := wn_1, wr := wr_1, q := { wn := wn, wr := wr, q := qbv, r := rbv }.q.shiftConcat true,
                r := r' - d }).q.getLsbD
      idx

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
lhs rhs : BitVec w
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
qbv rbv : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx
hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (RefVec.ite
              (RefVec.ite
                  (BVPred.mkUlt
                      (blastSub
                          (blastShiftConcat
                              (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                  { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                              { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                            rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                      {
                        lhs :=
                          (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                ⋯).cast
                            ⋯,
                        rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                  {
                    discr :=
                      (BVPred.mkUlt
                          (blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯).cast
                                ⋯,
                            rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                    lhs :=
                      (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                                ⋯).cast
                            ⋯).cast
                        ⋯,
                    rhs :=
                      ((blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                            ⋯).cast
                        ⋯ }).aig
              {
                discr :=
                  (BVPred.mkUlt
                          (blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯).cast
                                ⋯,
                            rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref.cast
                    ⋯,
                lhs :=
                  (((((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                            ⋯).cast
                        ⋯).cast
                    ⋯,
                rhs :=
                  ((blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).vec.cast
                        ⋯).cast
                    ⋯ }).aig,
        ref :=
          ((RefVec.ite
                      (BVPred.mkUlt
                          (blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯).cast
                                ⋯,
                            rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                      {
                        discr :=
                          (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                        lhs :=
                          (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                                    ⋯).cast
                                ⋯).cast
                            ⋯,
                        rhs :=
                          ((blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                                ⋯).cast
                            ⋯ }).vec.cast
                ⋯).get
            idx hidx }⟧ =
    (if rbv.shiftConcat (lhs.getLsbD (wn - 1)) < rhs then
            { wn := wn - 1, wr := wr + 1, q := qbv.shiftConcat false, r := rbv.shiftConcat (lhs.getLsbD (wn - 1)) }
          else
            { wn := wn - 1, wr := wr + 1, q := qbv.shiftConcat true,
              r := rbv.shiftConcat (lhs.getLsbD (wn - 1)) - rhs }).q.getLsbD
      idx