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

Tactic:
unfold blastUdiv

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 divRes := res_3.q;
              let_fun this := ⋯;
              let zero_2 := zero_1.cast this;
              let discr := discr.cast this;
              RefVec.ite aig_5 { discr := discr, lhs := zero_2, rhs := divRes }).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 divRes := res_3.q;
                  let_fun this := ⋯;
                  let zero_2 := zero_1.cast this;
                  let discr := discr.cast this;
                  RefVec.ite aig_5 { discr := discr, lhs := zero_2, rhs := divRes }).vec.get
            idx hidx }⟧ =
    (lhs / rhs).getLsbD idx

Proof state:
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
hdix : idx < w
⊢ ({ lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs, rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }.rhs.get idx
        hdix).gate <
    (blastConst aig 0#w).aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals