-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem lawful_divRec {args : DivModArgs w} {qr : DivModState w}
    (h : DivModState.Lawful args qr) :
    DivModState.Lawful args (divRec qr.wn args qr)

Proof state:
case hm
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ (divSubtractShift args qr).wn = wn'

Tactic:
simp only [divSubtractShift, hm]

Result:
case hm
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ (if qr.r.shiftConcat (args.n.getLsbD (wn' + 1 - 1)) < args.d then
        { wn := wn' + 1 - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (args.n.getLsbD (wn' + 1 - 1)) }
      else
        { wn := wn' + 1 - 1, wr := qr.wr + 1, q := qr.q.shiftConcat true,
          r := qr.r.shiftConcat (args.n.getLsbD (wn' + 1 - 1)) - args.d }).wn =
    wn'

Proof state:
case h
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ DivModState.Lawful args (divSubtractShift args qr)

Tactic:
apply lawful_divSubtractShift

Result:
case h.h
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ DivModState.Poised args qr

Proof state:
case h.h
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ DivModState.Poised args qr

Tactic:
constructor

Result:
case h.h.toLawful
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ DivModState.Lawful args qr

case h.h.hwn_lt
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ 0 < qr.wn

Proof state:
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ DivModState.Lawful args (divRec (wn' + 1) args qr)

Tactic:
simp only [divRec_succ]

Result:
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ DivModState.Lawful args (divRec wn' args (divSubtractShift args qr))

Proof state:
w : Nat
args : DivModArgs w
qr : DivModState w
h : DivModState.Lawful args qr
m : Nat
hm : qr.wn = m
⊢ DivModState.Lawful args (divRec m args qr)

Tactic:
induction m generalizing qr

Result:
case zero
w : Nat
args : DivModArgs w
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = 0
⊢ DivModState.Lawful args (divRec 0 args qr)

case succ
w : Nat
args : DivModArgs w
n✝ : Nat
a✝ : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = n✝ → DivModState.Lawful args (divRec n✝ args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = n✝ + 1
⊢ DivModState.Lawful args (divRec (n✝ + 1) args qr)

Proof state:
w : Nat
args : DivModArgs w
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = 0
⊢ DivModState.Lawful args (divRec 0 args qr)

Tactic:
exact h

Result:
no goals

Proof state:
w : Nat
args : DivModArgs w
qr : DivModState w
h : DivModState.Lawful args qr
⊢ DivModState.Lawful args (divRec qr.wn args qr)

Tactic:
generalize hm : qr.wn = m

Result:
w : Nat
args : DivModArgs w
qr : DivModState w
h : DivModState.Lawful args qr
m : Nat
hm : qr.wn = m
⊢ DivModState.Lawful args (divRec m args qr)

Proof state:
case zero
w : Nat
args : DivModArgs w
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = 0
⊢ DivModState.Lawful args (divRec 0 args qr)

case succ
w : Nat
args : DivModArgs w
n✝ : Nat
a✝ : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = n✝ → DivModState.Lawful args (divRec n✝ args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = n✝ + 1
⊢ DivModState.Lawful args (divRec (n✝ + 1) args qr)

Tactic:
case zero =>
  exact h

Result:
case succ
w : Nat
args : DivModArgs w
n✝ : Nat
a✝ : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = n✝ → DivModState.Lawful args (divRec n✝ args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = n✝ + 1
⊢ DivModState.Lawful args (divRec (n✝ + 1) args qr)

Proof state:
case hm
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ (if qr.r.shiftConcat (args.n.getLsbD (wn' + 1 - 1)) < args.d then
        { wn := wn' + 1 - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false,
          r := qr.r.shiftConcat (args.n.getLsbD (wn' + 1 - 1)) }
      else
        { wn := wn' + 1 - 1, wr := qr.wr + 1, q := qr.q.shiftConcat true,
          r := qr.r.shiftConcat (args.n.getLsbD (wn' + 1 - 1)) - args.d }).wn =
    wn'

Tactic:
split <;> rfl

Result:
no goals

Proof state:
case h.h.hwn_lt
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ 0 < qr.wn

Tactic:
omega

Result:
no goals

Proof state:
case h.h.toLawful
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ DivModState.Lawful args qr

Tactic:
assumption

Result:
no goals

Proof state:
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ DivModState.Lawful args (divRec wn' args (divSubtractShift args qr))

Tactic:
apply ih

Result:
case h
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ DivModState.Lawful args (divSubtractShift args qr)

case hm
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ {qr : DivModState w}, DivModState.Lawful args qr → qr.wn = wn' → DivModState.Lawful args (divRec wn' args qr)
qr : DivModState w
h : DivModState.Lawful args qr
hm : qr.wn = wn' + 1
⊢ (divSubtractShift args qr).wn = wn'