-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem udiv_eq_of_mul_add_toNat {d n q r : BitVec w} (hd : 0 < d)
    (hrd : r < d)
    (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) :
    n / d = q

Proof state:
case a.hz
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat
⊢ 0 < d.toNat

Tactic:
exact hd

Result:
no goals

Proof state:
case a.hy
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat
⊢ r.toNat < d.toNat

Tactic:
exact hrd

Result:
no goals

Proof state:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ (n / d).toNat = q.toNat

Tactic:
rw [toNat_udiv]

Result:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ n.toNat / d.toNat = q.toNat

Proof state:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat
⊢ n.toNat / d.toNat = q.toNat

Tactic:
rw [Nat.div_add_eq_left_of_lt] at hdqnr

Result:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat / d.toNat = n.toNat / d.toNat
⊢ n.toNat / d.toNat = q.toNat

case a.hx
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat
⊢ d.toNat ∣ d.toNat * q.toNat

case a.hy
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat
⊢ r.toNat < d.toNat

case a.hz
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat
⊢ 0 < d.toNat

Proof state:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat / d.toNat = n.toNat / d.toNat
⊢ d.toNat * q.toNat / d.toNat = q.toNat

Tactic:
exact mul_div_right q.toNat hd

Result:
no goals

Proof state:
case a.hx
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat
⊢ d.toNat ∣ d.toNat * q.toNat

Tactic:
exact Nat.dvd_mul_right d.toNat q.toNat

Result:
no goals

Proof state:
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat

Tactic:
simp [hdqnr]

Result:
no goals

Proof state:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ n.toNat / d.toNat = q.toNat

Tactic:
replace hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat := by
  simp [hdqnr]

Result:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat
⊢ n.toNat / d.toNat = q.toNat

Proof state:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat / d.toNat = n.toNat / d.toNat
⊢ n.toNat / d.toNat = q.toNat

Tactic:
rw [← hdqnr]

Result:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat / d.toNat = n.toNat / d.toNat
⊢ d.toNat * q.toNat / d.toNat = q.toNat

Proof state:
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ n / d = q

Tactic:
apply BitVec.eq_of_toNat_eq

Result:
case a
w : Nat
d n q r : BitVec w
hd : 0 < d
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ (n / d).toNat = q.toNat