-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastDivSubtractShift_r (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)
    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
    (hfalse : ⟦aig, falseRef, assign⟧ = false)
      :
    ∀ (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).r.get idx hidx,
        assign
      ⟧
        =
      (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).r.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
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
hidx : idx < w
hdiscr : rbv.shiftConcat (lhs.getLsbD (wn - 1)) < rhs
⊢ ⟦assign,
      {
        aig :=
          (BVPred.mkUlt
              (blastSub
                  (blastShiftConcat
                      (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                          { lhs := q.cast ⋯, bit := { gate := falseRef.gate, hgate := ⋯ } }).aig
                      { lhs := (q.cast ⋯).cast ⋯, bit := { gate := trueRef.gate, hgate := ⋯ } }).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 :=
          { gate := ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.get idx hidx).gate,
            hgate := ?m.33965 } }⟧ =
    (rbv.shiftConcat (lhs.getLsbD (wn - 1))).getLsbD idx

α : 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
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
hidx : idx < w
hdiscr : rbv.shiftConcat (lhs.getLsbD (wn - 1)) < rhs
⊢ ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.get idx hidx).gate <
    (BVPred.mkUlt
            (blastSub
                (blastShiftConcat
                    (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                        { lhs := q.cast ⋯, bit := { gate := falseRef.gate, hgate := ⋯ } }).aig
                    { lhs := (q.cast ⋯).cast ⋯, bit := { gate := trueRef.gate, hgate := ⋯ } }).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.decls.size

Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]

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
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
hidx : idx < w
hdiscr : rbv.shiftConcat (lhs.getLsbD (wn - 1)) < rhs
⊢ ⟦assign,
      {
        aig :=
          (blastSub
              (blastShiftConcat
                  (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                      { lhs := q.cast ⋯, bit := { gate := falseRef.gate, hgate := ⋯ } }).aig
                  { lhs := (q.cast ⋯).cast ⋯, bit := { gate := trueRef.gate, hgate := ⋯ } }).aig
              { lhs := ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig,
        ref :=
          { gate := ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.get idx hidx).gate,
            hgate := ?m.34491 } }⟧ =
    (rbv.shiftConcat (lhs.getLsbD (wn - 1))).getLsbD idx

α : 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
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
hidx : idx < w
hdiscr : rbv.shiftConcat (lhs.getLsbD (wn - 1)) < rhs
⊢ ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.get idx hidx).gate <
    (blastSub
            (blastShiftConcat
                (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                    { lhs := q.cast ⋯, bit := { gate := falseRef.gate, hgate := ⋯ } }).aig
                { lhs := (q.cast ⋯).cast ⋯, bit := { gate := trueRef.gate, hgate := ⋯ } }).aig
            { lhs := ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig.decls.size