∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (n d : aig.RefVec w)
  (wn wr : ℕ) (q r : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r =
    match curr with
    | 0 => { aig := aig, q := q, r := r, hle := ⋯ }
    | curr.succ =>
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r;
      let aig_1 := res.aig;
      let wn_1 := res.wn;
      let wr_1 := res.wr;
      let q_1 := res.q;
      let r_1 := res.r;
      have this := ⋯;
      let n_1 := n.cast this;
      let d_1 := d.cast this;
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig_1 curr n_1 d_1 wn_1 wr_1 q_1 r_1;
      let aig_2 := res.aig;
      have q_2 := res.q;
      have r_2 := res.r;
      have this := ⋯;
      { aig := aig_2, q := q_2, r := r_2, hle := this }