-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem DivModState.umod_eq_of_lawful {qr : DivModState w}
    (h : DivModState.Lawful {n, d} qr)
    (h_final  : qr.wn = 0) :
    n % d = qr.r

Proof state:
w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ { n := n, d := d }.d.toNat * BitVec.toNat ?m.63092 + qr.r.toNat = n.toNat

w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ BitVec w

Tactic:
have hdiv := h.hdiv

Result:
w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
hdiv : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
⊢ { n := n, d := d }.d.toNat * BitVec.toNat ?m.63092 + qr.r.toNat = n.toNat

w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ BitVec w

Proof state:
w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
hdiv : n.toNat >>> qr.wn = d.toNat * qr.q.toNat + qr.r.toNat
⊢ { n := n, d := d }.d.toNat * BitVec.toNat ?m.63092 + qr.r.toNat = n.toNat

w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ BitVec w

Tactic:
simp only [h_final] at *

Result:
w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final✝ : qr.wn = 0
h_final : True
hdiv : n.toNat >>> 0 = d.toNat * qr.q.toNat + qr.r.toNat
⊢ d.toNat * BitVec.toNat ?m.63092 + qr.r.toNat = n.toNat

w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ BitVec w

Proof state:
w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
hdiv : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
⊢ { n := n, d := d }.d.toNat * BitVec.toNat ?m.63092 + qr.r.toNat = n.toNat

w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ BitVec w

Tactic:
simp only [shiftRight_zero] at hdiv

Result:
w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
hdiv : n.toNat >>> qr.wn = d.toNat * qr.q.toNat + qr.r.toNat
⊢ { n := n, d := d }.d.toNat * BitVec.toNat ?m.63092 + qr.r.toNat = n.toNat

w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ BitVec w

Proof state:
w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ n % d = qr.r

Tactic:
apply umod_eq_of_mul_add_toNat h.hrLtDivisor

Result:
w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ { n := n, d := d }.d.toNat * BitVec.toNat ?m.63092 + qr.r.toNat = n.toNat

w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ BitVec w

Proof state:
w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final✝ : qr.wn = 0
h_final : True
hdiv : n.toNat >>> 0 = d.toNat * qr.q.toNat + qr.r.toNat
⊢ d.toNat * BitVec.toNat ?m.63092 + qr.r.toNat = n.toNat

w : Nat
n d : BitVec w
qr : DivModState w
h : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ BitVec w

Tactic:
exact hdiv.symm

Result:
no goals