-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem wn_divRec (args : DivModArgs w) (qr : DivModState w) :
    (divRec qr.wn args qr).wn = 0

Proof state:
case hm
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ (qr : DivModState w), qr.wn = wn' → (divRec wn' args qr).wn = 0
qr : DivModState w
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), qr.wn = wn' → (divRec wn' args qr).wn = 0
qr : DivModState w
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:
w : Nat
args : DivModArgs w
qr : DivModState w
⊢ (divRec qr.wn args qr).wn = 0

Tactic:
generalize hm : qr.wn = m

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

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

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

Tactic:
case zero =>
  assumption

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

Proof state:
case succ
w : Nat
args : DivModArgs w
n✝ : Nat
a✝ : ∀ (qr : DivModState w), qr.wn = n✝ → (divRec n✝ args qr).wn = 0
qr : DivModState w
hm : qr.wn = n✝ + 1
⊢ (divRec (n✝ + 1) args qr).wn = 0

Tactic:
case succ wn' ih =>
  apply ih
  simp only [divSubtractShift, hm]
  split <;> rfl

Result:
no goals

Proof state:
case hm
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ (qr : DivModState w), qr.wn = wn' → (divRec wn' args qr).wn = 0
qr : DivModState w
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:
w : Nat
args : DivModArgs w
wn' : Nat
ih : ∀ (qr : DivModState w), qr.wn = wn' → (divRec wn' args qr).wn = 0
qr : DivModState w
hm : qr.wn = wn' + 1
⊢ (divRec (wn' + 1) args qr).wn = 0

Tactic:
apply ih

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

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

Tactic:
induction m generalizing qr

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

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

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

Tactic:
assumption

Result:
no goals