-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) :
    DivModState.Lawful args (divSubtractShift args qr)

Proof state:
case pos
w : Nat
qr : DivModState w
n d : BitVec w
h : DivModState.Poised { n := n, d := d } qr
hrwn : qr.wr + qr.wn = w
hd : 0 < { n := n, d := d }.d
hrd : qr.r.toNat < { n := n, d := d }.d.toNat
hr : qr.r.toNat < 2 ^ qr.wr
hn : qr.q.toNat < 2 ^ qr.wr
hrnd : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt : 0 < qr.wn
this : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2
rltd : qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d
⊢ DivModState.Lawful { n := n, d := d }
    { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false, r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }

Tactic:
constructor <;> try bv_omega

Result:
case pos.hrWidth
w : Nat
qr : DivModState w
n d : BitVec w
h : DivModState.Poised { n := n, d := d } qr
hrwn : qr.wr + qr.wn = w
hd : 0 < { n := n, d := d }.d
hrd : qr.r.toNat < { n := n, d := d }.d.toNat
hr : qr.r.toNat < 2 ^ qr.wr
hn : qr.q.toNat < 2 ^ qr.wr
hrnd : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt : 0 < qr.wn
this : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2
rltd : qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d
⊢ { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.r.toNat <
    2 ^
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.wr

case pos.hqWidth
w : Nat
qr : DivModState w
n d : BitVec w
h : DivModState.Poised { n := n, d := d } qr
hrwn : qr.wr + qr.wn = w
hd : 0 < { n := n, d := d }.d
hrd : qr.r.toNat < { n := n, d := d }.d.toNat
hr : qr.r.toNat < 2 ^ qr.wr
hn : qr.q.toNat < 2 ^ qr.wr
hrnd : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt : 0 < qr.wn
this : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2
rltd : qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d
⊢ { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.q.toNat <
    2 ^
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.wr

case pos.hdiv
w : Nat
qr : DivModState w
n d : BitVec w
h : DivModState.Poised { n := n, d := d } qr
hrwn : qr.wr + qr.wn = w
hd : 0 < { n := n, d := d }.d
hrd : qr.r.toNat < { n := n, d := d }.d.toNat
hr : qr.r.toNat < 2 ^ qr.wr
hn : qr.q.toNat < 2 ^ qr.wr
hrnd : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt : 0 < qr.wn
this : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2
rltd : qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d
⊢ { n := n, d := d }.n.toNat >>>
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.wn =
    { n := n, d := d }.d.toNat *
        { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
              r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.q.toNat +
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
            r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.r.toNat

Proof state:
case pos.hrWidth
w : Nat
qr : DivModState w
n d : BitVec w
h : DivModState.Poised { n := n, d := d } qr
hrwn : qr.wr + qr.wn = w
hd : 0 < { n := n, d := d }.d
hrd : qr.r.toNat < { n := n, d := d }.d.toNat
hr : qr.r.toNat < 2 ^ qr.wr
hn : qr.q.toNat < 2 ^ qr.wr
hrnd : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt : 0 < qr.wn
this : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2
rltd : qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d
⊢ { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.r.toNat <
    2 ^
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.wr

case pos.hqWidth
w : Nat
qr : DivModState w
n d : BitVec w
h : DivModState.Poised { n := n, d := d } qr
hrwn : qr.wr + qr.wn = w
hd : 0 < { n := n, d := d }.d
hrd : qr.r.toNat < { n := n, d := d }.d.toNat
hr : qr.r.toNat < 2 ^ qr.wr
hn : qr.q.toNat < 2 ^ qr.wr
hrnd : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt : 0 < qr.wn
this : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2
rltd : qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d
⊢ { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.q.toNat <
    2 ^
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.wr

case pos.hdiv
w : Nat
qr : DivModState w
n d : BitVec w
h : DivModState.Poised { n := n, d := d } qr
hrwn : qr.wr + qr.wn = w
hd : 0 < { n := n, d := d }.d
hrd : qr.r.toNat < { n := n, d := d }.d.toNat
hr : qr.r.toNat < 2 ^ qr.wr
hn : qr.q.toNat < 2 ^ qr.wr
hrnd : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt : 0 < qr.wn
this : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2
rltd : qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d
⊢ { n := n, d := d }.n.toNat >>>
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.wn =
    { n := n, d := d }.d.toNat *
        { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
              r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.q.toNat +
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
            r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.r.toNat

Tactic:
case pos.hrWidth => apply toNat_shiftConcat_lt_of_lt <;> omega

Result:
case pos.hqWidth
w : Nat
qr : DivModState w
n d : BitVec w
h : DivModState.Poised { n := n, d := d } qr
hrwn : qr.wr + qr.wn = w
hd : 0 < { n := n, d := d }.d
hrd : qr.r.toNat < { n := n, d := d }.d.toNat
hr : qr.r.toNat < 2 ^ qr.wr
hn : qr.q.toNat < 2 ^ qr.wr
hrnd : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt : 0 < qr.wn
this : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2
rltd : qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d
⊢ { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.q.toNat <
    2 ^
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.wr

case pos.hdiv
w : Nat
qr : DivModState w
n d : BitVec w
h : DivModState.Poised { n := n, d := d } qr
hrwn : qr.wr + qr.wn = w
hd : 0 < { n := n, d := d }.d
hrd : qr.r.toNat < { n := n, d := d }.d.toNat
hr : qr.r.toNat < 2 ^ qr.wr
hn : qr.q.toNat < 2 ^ qr.wr
hrnd : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt : 0 < qr.wn
this : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2
rltd : qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d
⊢ { n := n, d := d }.n.toNat >>>
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.wn =
    { n := n, d := d }.d.toNat *
        { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
              r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.q.toNat +
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
            r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }.r.toNat