-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem denote_blast (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment)
      (input : BinaryRefVec aig w)
      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs.getLsbD idx)
      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs.getLsbD idx) :
      ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blast aig input).aig, (blast aig input).vec.get idx hidx, assign.toAIGAssignment⟧
          =
        (lhs * rhs).getLsbD idx

Proof state:
case intro.hleft
aig : AIG BVBit
assign : Assignment
idx✝ w : Nat
lhs rhs : BitVec w.succ
input : aig.BinaryRefVec w.succ
hleft :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
hidx✝ : idx✝ < w.succ
res : RefVecEntry BVBit w.succ
hne : ¬w.succ = 0
hb :
  go
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).aig
      ((input.cast ⋯).lhs.cast ⋯) ((input.cast ⋯).rhs.cast ⋯) 1
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).vec =
    res
idx : Nat
hidx : idx < w.succ
⊢ ⟦assign.toAIGAssignment,
      { aig := (blastConst aig 0).aig,
        ref := { gate := (((input.cast ⋯).lhs.cast ⋯).get idx hidx).gate, hgate := ?intro.hleft } }⟧ =
    lhs.getLsbD idx

case intro.hleft
aig : AIG BVBit
assign : Assignment
idx✝ w : Nat
lhs rhs : BitVec w.succ
input : aig.BinaryRefVec w.succ
hleft :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
hidx✝ : idx✝ < w.succ
res : RefVecEntry BVBit w.succ
hne : ¬w.succ = 0
hb :
  go
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).aig
      ((input.cast ⋯).lhs.cast ⋯) ((input.cast ⋯).rhs.cast ⋯) 1
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).vec =
    res
idx : Nat
hidx : idx < w.succ
⊢ (((input.cast ⋯).lhs.cast ⋯).get idx hidx).gate < (blastConst aig 0).aig.decls.size

Tactic:
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]

Result:
case intro.hleft
aig : AIG BVBit
assign : Assignment
idx✝ w : Nat
lhs rhs : BitVec w.succ
input : aig.BinaryRefVec w.succ
hleft :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
hidx✝ : idx✝ < w.succ
res : RefVecEntry BVBit w.succ
hne : ¬w.succ = 0
hb :
  go
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).aig
      ((input.cast ⋯).lhs.cast ⋯) ((input.cast ⋯).rhs.cast ⋯) 1
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).vec =
    res
idx : Nat
hidx : idx < w.succ
⊢ ⟦assign.toAIGAssignment,
      { aig := aig, ref := { gate := (((input.cast ⋯).lhs.cast ⋯).get idx hidx).gate, hgate := ?intro.hleft } }⟧ =
    lhs.getLsbD idx

case intro.hleft
aig : AIG BVBit
assign : Assignment
idx✝ w : Nat
lhs rhs : BitVec w.succ
input : aig.BinaryRefVec w.succ
hleft :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
hidx✝ : idx✝ < w.succ
res : RefVecEntry BVBit w.succ
hne : ¬w.succ = 0
hb :
  go
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).aig
      ((input.cast ⋯).lhs.cast ⋯) ((input.cast ⋯).rhs.cast ⋯) 1
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).vec =
    res
idx : Nat
hidx : idx < w.succ
⊢ (((input.cast ⋯).lhs.cast ⋯).get idx hidx).gate < aig.decls.size

Proof state:
case intro.hright
aig : AIG BVBit
assign : Assignment
idx w : Nat
lhs rhs : BitVec w.succ
input : aig.BinaryRefVec w.succ
hleft :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
hidx : idx < w.succ
res : RefVecEntry BVBit w.succ
hne : ¬w.succ = 0
hb :
  go
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).aig
      ((input.cast ⋯).lhs.cast ⋯) ((input.cast ⋯).rhs.cast ⋯) 1
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).vec =
    res
⊢ ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment,
        {
          aig :=
            (RefVec.ite (blastConst aig 0).aig
                { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).aig,
          ref := ((input.cast ⋯).rhs.cast ⋯).get idx hidx }⟧ =
      rhs.getLsbD idx

Tactic:
intro idx hidx

Result:
case intro.hright
aig : AIG BVBit
assign : Assignment
idx✝ w : Nat
lhs rhs : BitVec w.succ
input : aig.BinaryRefVec w.succ
hleft :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w.succ),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
hidx✝ : idx✝ < w.succ
res : RefVecEntry BVBit w.succ
hne : ¬w.succ = 0
hb :
  go
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).aig
      ((input.cast ⋯).lhs.cast ⋯) ((input.cast ⋯).rhs.cast ⋯) 1
      (RefVec.ite (blastConst aig 0).aig
          { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).vec =
    res
idx : Nat
hidx : idx < w.succ
⊢ ⟦assign.toAIGAssignment,
      {
        aig :=
          (RefVec.ite (blastConst aig 0).aig
              { discr := (input.cast ⋯).rhs.get 0 ⋯, lhs := (input.cast ⋯).lhs, rhs := (blastConst aig 0).vec }).aig,
        ref := ((input.cast ⋯).rhs.cast ⋯).get idx hidx }⟧ =
    rhs.getLsbD idx