-- 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
⊢ ⟦assign, { aig := (blastUmod aig input).aig, ref := (blastUmod aig input).vec.get idx hidx }⟧ =
    (lhs % rhs).getLsbD idx

Tactic:
unfold blastUmod

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
⊢ ⟦assign,
      {
        aig :=
          (let res := blastConst aig 0#w;
            let aig_1 := res.aig;
            let zero := res.vec;
            let input := input.cast ⋯;
            let res_1 := aig_1.mkConstCached false;
            let aig_2 := res_1.aig;
            let falseRef := res_1.ref;
            let_fun this := ⋯;
            let zero := zero.cast this;
            let input := input.cast this;
            let res_2 := aig_2.mkConstCached true;
            let aig_3 := res_2.aig;
            let trueRef := res_2.ref;
            let_fun this_1 := ⋯;
            let falseRef := falseRef.cast this_1;
            let zero := zero.cast this_1;
            let input := input.cast this_1;
            match input with
            | { lhs := lhs, rhs := rhs } =>
              let res := BVPred.mkEq aig_3 { lhs := rhs, rhs := zero };
              let aig_4 := res.aig;
              let discr := res.ref;
              let_fun this_2 := ⋯;
              let falseRef := falseRef.cast this_2;
              let trueRef := trueRef.cast this_2;
              let zero_1 := zero.cast this_2;
              let lhs_1 := lhs.cast this_2;
              let rhs_1 := rhs.cast this_2;
              let res_3 := blastUdiv.go aig_4 w falseRef trueRef lhs_1 rhs_1 w 0 zero_1 zero_1;
              let aig_5 := res_3.aig;
              let modRes := res_3.r;
              let_fun this := ⋯;
              let discr := discr.cast this;
              let lhs := lhs_1.cast this;
              RefVec.ite aig_5 { discr := discr, lhs := lhs, rhs := modRes }).aig,
        ref :=
          (let res := blastConst aig 0#w;
                let aig_1 := res.aig;
                let zero := res.vec;
                let input := input.cast ⋯;
                let res_1 := aig_1.mkConstCached false;
                let aig_2 := res_1.aig;
                let falseRef := res_1.ref;
                let_fun this := ⋯;
                let zero := zero.cast this;
                let input := input.cast this;
                let res_2 := aig_2.mkConstCached true;
                let aig_3 := res_2.aig;
                let trueRef := res_2.ref;
                let_fun this_1 := ⋯;
                let falseRef := falseRef.cast this_1;
                let zero := zero.cast this_1;
                let input := input.cast this_1;
                match input with
                | { lhs := lhs, rhs := rhs } =>
                  let res := BVPred.mkEq aig_3 { lhs := rhs, rhs := zero };
                  let aig_4 := res.aig;
                  let discr := res.ref;
                  let_fun this_2 := ⋯;
                  let falseRef := falseRef.cast this_2;
                  let trueRef := trueRef.cast this_2;
                  let zero_1 := zero.cast this_2;
                  let lhs_1 := lhs.cast this_2;
                  let rhs_1 := rhs.cast this_2;
                  let res_3 := blastUdiv.go aig_4 w falseRef trueRef lhs_1 rhs_1 w 0 zero_1 zero_1;
                  let aig_5 := res_3.aig;
                  let modRes := res_3.r;
                  let_fun this := ⋯;
                  let discr := discr.cast this;
                  let lhs := lhs_1.cast this;
                  RefVec.ite aig_5 { discr := discr, lhs := lhs, rhs := modRes }).vec.get
            idx hidx }⟧ =
    (lhs % rhs).getLsbD idx