-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat) (lhs rhs rbv qbv : BitVec w)
    (falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w) (wn wr : Nat)
    (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),
      ⟦
        (go aig curr falseRef trueRef n d wn wr q r).aig,
        (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx,
        assign
      ⟧
        =
      (BitVec.divRec curr { n := lhs, d := rhs} { wn, wr, q := qbv, r := rbv }).q.getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ ⟦assign,
      {
        aig :=
          {
              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,
        ref :=
          {
                  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 := ⋯ }.q.get
            idx hidx }⟧ =
    (BitVec.divRec curr { n := lhs, d := rhs }
            { wn := { wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1,
              wr := { wn := wn, wr := wr, q := qbv, r := rbv }.wr + 1,
              q := { wn := wn, wr := wr, q := qbv, r := rbv }.q.shiftConcat true,
              r :=
                { wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
                    (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) -
                  rhs }).q.getLsbD
      idx

Tactic:
rw [ih]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ (BitVec.divRec curr { n := lhs, d := rhs }
            { wn := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn,
              wr := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr, q := ?qbv, r := ?rbv }).q.getLsbD
      idx =
    (BitVec.divRec curr { n := lhs, d := rhs }
            { wn := { wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1,
              wr := { wn := wn, wr := wr, q := qbv, r := rbv }.wr + 1,
              q := { wn := wn, wr := wr, q := qbv, r := rbv }.q.shiftConcat true,
              r :=
                { wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
                    (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) -
                  rhs }).q.getLsbD
      idx

case rbv
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ BitVec w

case qbv
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ BitVec w

case hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        { aig := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig, ref := (n.cast ⋯).get idx hidx }⟧ =
      lhs.getLsbD idx

case hright
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        { aig := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig, ref := (d.cast ⋯).get idx hidx }⟧ =
      rhs.getLsbD idx

case hq
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        { aig := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
          ref := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
      BitVec.getLsbD ?qbv idx

case hr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        { aig := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
          ref := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r.get idx hidx }⟧ =
      BitVec.getLsbD ?rbv idx

case hfalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ ⟦assign, { aig := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig, ref := falseRef.cast ⋯ }⟧ = false

case htrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
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
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ ⟦assign, { aig := (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig, ref := trueRef.cast ⋯ }⟧ = true