-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
theorem denote_blastUmod (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),
        ⟦(blastUmod aig input).aig, (blastUmod 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 : ¬(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 :=
          (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 ⋯)).r.get
            idx hidx }⟧ =
    (lhs % rhs).getLsbD idx

Tactic:
have hzero : 0#w < rhs := by
  rw [Normalize.BitVec.zero_lt_iff_zero_neq]
  simpa using 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
hzero : 0#w < rhs
⊢ ⟦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 ⋯)).r.get
            idx hidx }⟧ =
    (lhs % rhs).getLsbD idx