-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem denote_blastMul (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),
        ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
          =
        (lhs * rhs).getLsbD idx

Proof state:
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
hb :
  (if RefVec.countKnown aig input.lhs < RefVec.countKnown aig input.rhs then blastMul.blast aig input
    else blastMul.blast aig { lhs := input.rhs, rhs := input.lhs }) =
    res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx

Tactic:
split at hb

Result:
case isTrue
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝ : RefVec.countKnown aig input.lhs < RefVec.countKnown aig input.rhs
hb : blastMul.blast aig input = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx

case isFalse
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝ : ¬RefVec.countKnown aig input.lhs < RefVec.countKnown aig input.rhs
hb : blastMul.blast aig { lhs := input.rhs, rhs := input.lhs } = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx

Proof state:
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := (blastMul aig input).aig, ref := (blastMul aig input).vec.get idx hidx }⟧ =
      (lhs * rhs).getLsbD idx

Tactic:
intro idx hidx

Result:
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign.toAIGAssignment, { aig := (blastMul aig input).aig, ref := (blastMul aig input).vec.get idx hidx }⟧ =
    (lhs * rhs).getLsbD idx

Proof state:
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
hb :
  (if RefVec.countKnown aig input.lhs < RefVec.countKnown aig input.rhs then blastMul.blast aig input
    else
      match input with
      | { lhs := lhs, rhs := rhs } => blastMul.blast aig { lhs := rhs, rhs := lhs }) =
    res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx

Tactic:
dsimp only at hb

Result:
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
hb :
  (if RefVec.countKnown aig input.lhs < RefVec.countKnown aig input.rhs then blastMul.blast aig input
    else blastMul.blast aig { lhs := input.rhs, rhs := input.lhs }) =
    res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx

Proof state:
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
hb : blastMul aig input = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx

Tactic:
unfold blastMul at hb

Result:
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
hb :
  (if RefVec.countKnown aig input.lhs < RefVec.countKnown aig input.rhs then blastMul.blast aig input
    else
      match input with
      | { lhs := lhs, rhs := rhs } => blastMul.blast aig { lhs := rhs, rhs := lhs }) =
    res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx

Proof state:
case isFalse
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝ : ¬RefVec.countKnown aig input.lhs < RefVec.countKnown aig input.rhs
hb : blastMul.blast aig { lhs := input.rhs, rhs := input.lhs } = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx

Tactic:
rw [BitVec.mul_comm, ← hb, blastMul.denote_blast] <;> assumption

Result:
no goals