-- 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
⊢ (if
        ⟦assign,
            {
              aig :=
                (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,
              ref :=
                {
                    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
                        ⋯ }.discr }⟧ =
          true then
      ⟦assign,
        {
          aig :=
            (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,
          ref :=
            {
                    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
                        ⋯ }.lhs.get
              idx hidx }⟧
    else
      ⟦assign,
        {
          aig :=
            (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,
          ref :=
            {
                    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
                        ⋯ }.rhs.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

Tactic:
rw [BVPred.mkUlt_denote_eq (lhs := rbv.shiftConcat (lhs.getLsbD (wn - 1))) (rhs := rhs)]

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
⊢ (if (rbv.shiftConcat (lhs.getLsbD (wn - 1))).ult rhs = true then
      ⟦assign,
        {
          aig :=
            (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,
          ref :=
            {
                    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
                        ⋯ }.lhs.get
              idx hidx }⟧
    else
      ⟦assign,
        {
          aig :=
            (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,
          ref :=
            {
                    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
                        ⋯ }.rhs.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

case hleft
α : 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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        {
          aig :=
            (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,
          ref :=
            { lhs := (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast ⋯,
                    rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }.lhs.get
              idx hidx }⟧ =
      (rbv.shiftConcat (lhs.getLsbD (wn - 1))).getLsbD idx

case hright
α : 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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        {
          aig :=
            (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,
          ref :=
            { lhs := (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast ⋯,
                    rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }.rhs.get
              idx hidx }⟧ =
      rhs.getLsbD idx