-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastDivSubtractShift_wn (aig : AIG α) (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)
      :
    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
      =
    (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wn

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
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
⊢ wn - 1 =
    (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 }).wn

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
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
⊢ (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 := posR.cast this_5;
      let negR := negR.cast this_5;
      let discr := ⋯;
      ⋯).wn =
    (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 }).wn

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
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
⊢ wn - 1 =
    (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 }).wn

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
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
⊢ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn =
    (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wn

Tactic:
unfold blastDivSubtractShift BitVec.divSubtractShift

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
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
⊢ (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 := posR.cast this_5;
      let negR := negR.cast this_5;
      let discr := ⋯;
      ⋯).wn =
    (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 }).wn