-- 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
⊢ (if
        ⟦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 then
      ⟦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 := ⋯ } }⟧
    else
      ⟦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 :=
            (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 ⋯)).q.get
              idx hidx }⟧) =
    (lhs / rhs).getLsbD idx

Tactic:
split

Result:
case isTrue
α : 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
h✝ :
  ⟦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
⊢ ⟦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 isFalse
α : 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
h✝ :
  ¬⟦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
⊢ ⟦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 :=
          (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 ⋯)).q.get
            idx hidx }⟧ =
    (lhs / rhs).getLsbD idx