-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
      (input : BinaryRefVec aig w)
      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
      ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blastUdiv aig input).aig, (blastUdiv aig input).vec.get idx hidx, assign⟧
          =
        (lhs / rhs).getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
hdiscr✝ :
  ⟦assign,
      {
        aig :=
          (blastUdiv.go
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                  { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
              w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
              { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
              ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
        ref :=
          {
            gate :=
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
            hgate := ⋯ } }⟧ =
    true
hdiscr :
  ⟦assign,
      {
        aig :=
          (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
              { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig,
        ref :=
          {
            gate :=
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
            hgate := ?hstart } }⟧ =
    true
⊢ ⟦assign,
      {
        aig :=
          (blastUdiv.go
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                  { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
              w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
              { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
              ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
        ref := { gate := ((blastConst aig 0#w).vec.get idx hidx).gate, hgate := ⋯ } }⟧ =
    (lhs / rhs).getLsbD idx

case hstart
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
hdiscr :
  ⟦assign,
      {
        aig :=
          (blastUdiv.go
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                  { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
              w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
              { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
              ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
        ref :=
          {
            gate :=
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
            hgate := ⋯ } }⟧ =
    true
⊢ (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
          { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate <
    (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
            { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
              rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig.decls.size

Tactic:
rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
hdiscr✝ :
  ⟦assign,
      {
        aig :=
          (blastUdiv.go
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                  { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
              w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
              { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
              ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
        ref :=
          {
            gate :=
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
            hgate := ⋯ } }⟧ =
    true
hdiscr : (rhs == 0#w) = true
⊢ ⟦assign,
      {
        aig :=
          (blastUdiv.go
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                  { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
              w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
              { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
              ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
        ref := { gate := ((blastConst aig 0#w).vec.get idx hidx).gate, hgate := ⋯ } }⟧ =
    (lhs / rhs).getLsbD idx

case hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
hdiscr✝ :
  ⟦assign,
      {
        aig :=
          (blastUdiv.go
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                  { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
              w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
              { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
              ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
        ref :=
          {
            gate :=
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
            hgate := ⋯ } }⟧ =
    true
hdiscr :
  ⟦assign,
      {
        aig :=
          (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
              { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig,
        ref :=
          {
            gate :=
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
            hgate := ⋯ } }⟧ =
    true
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        { aig := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig,
          ref :=
            { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }.lhs.get idx
              hidx }⟧ =
      rhs.getLsbD idx

case hright
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
hdiscr✝ :
  ⟦assign,
      {
        aig :=
          (blastUdiv.go
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                  { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
              w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
              { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
              ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
              ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
        ref :=
          {
            gate :=
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
            hgate := ⋯ } }⟧ =
    true
hdiscr :
  ⟦assign,
      {
        aig :=
          (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
              { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig,
        ref :=
          {
            gate :=
              (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
            hgate := ⋯ } }⟧ =
    true
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        { aig := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig,
          ref :=
            { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }.rhs.get idx
              hidx }⟧ =
      (0#w).getLsbD idx