-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem DivModState.toNat_shiftRight_sub_one_eq
    {args : DivModArgs w} {qr : DivModState w} (h : qr.Poised args) :
    args.n.toNat >>> (qr.wn - 1)
    = (args.n.toNat >>> qr.wn) * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

Proof state:
case hk
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ w - qr.wn < w

Tactic:
omega

Result:
no goals

Proof state:
case hx.hn
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ qr.wn ≤ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ (args.n >>> qr.wn).toNat * 2 + (args.n.getLsbD (qr.wn - 1)).toNat =
    args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ ((args.n >>> qr.wn).shiftConcat (args.n.getLsbD (qr.wn - 1))).toNat =
    args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

Tactic:
rw [toNat_shiftConcat_eq_of_lt (k := w - qr.wn)]

Result:
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ (args.n >>> qr.wn).toNat * 2 + (args.n.getLsbD (qr.wn - 1)).toNat =
    args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

case hk
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ w - qr.wn < w

case hx
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ (args.n >>> qr.wn).toNat < 2 ^ (w - qr.wn)

Proof state:
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
⊢ (args.n >>> (qr.wn - 1)).toNat = args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

Tactic:
have {..} := h

Result:
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ (args.n >>> (qr.wn - 1)).toNat = args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

Proof state:
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
⊢ args.n.toNat >>> (qr.wn - 1) = args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

Tactic:
show BitVec.toNat (args.n >>> (qr.wn - 1)) = _

Result:
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
⊢ (args.n >>> (qr.wn - 1)).toNat = args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

Proof state:
case hx
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ (args.n >>> qr.wn).toNat < 2 ^ (w - qr.wn)

Tactic:
apply BitVec.toNat_ushiftRight_lt

Result:
case hx.hn
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ qr.wn ≤ w

Proof state:
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ (args.n >>> (qr.wn - 1)).toNat = args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

Tactic:
rw [shiftRight_sub_one_eq_shiftConcat args.n h.hwn_lt]

Result:
w : Nat
args : DivModArgs w
qr : DivModState w
h : Poised args qr
hwrn✝ : qr.wr + qr.wn = w
hdPos✝ : 0 < args.d
hrLtDivisor✝ : qr.r.toNat < args.d.toNat
hrWidth✝ : qr.r.toNat < 2 ^ qr.wr
hqWidth✝ : qr.q.toNat < 2 ^ qr.wr
hdiv✝ : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
hwn_lt✝ : 0 < qr.wn
⊢ ((args.n >>> qr.wn).shiftConcat (args.n.getLsbD (qr.wn - 1))).toNat =
    args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat