-- 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:
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
heq✝ : rhs.getLsbD 0 = false
heq : ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get 0 ?hidx }⟧ = false
⊢ ((input.rhs.get 0 ⋯).cast ⋯).gate < aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals

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 h : w = 0 then { aig := aig, vec := ⋯ ▸ RefVec.empty }
    else
      let_fun this := ⋯;
      let res := blastConst aig 0;
      let aig_1 := res.aig;
      let zero := res.vec;
      let_fun this_1 := ⋯;
      let input := input.cast this_1;
      match input with
      | { lhs := lhs, rhs := rhs } =>
        let res := RefVec.ite aig_1 { discr := rhs.get 0 this, lhs := lhs, rhs := zero };
        let aig_2 := res.aig;
        let acc := res.vec;
        let_fun this_2 := ⋯;
        let lhs_1 := lhs.cast this_2;
        let rhs := rhs.cast this_2;
        go aig_2 lhs_1 rhs 1 acc) =
    res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs.mulRec rhs w).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 h : w = 0 then { aig := aig, vec := ⋯ ▸ RefVec.empty }
    else
      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
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs.mulRec rhs w).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
hne : ¬w = 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
this : ∃ k, w = k.succ
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs.mulRec rhs w).getLsbD idx

Tactic:
rcases this with ⟨w, hw⟩

Result:
case intro
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✝
hne : ¬w✝ = 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
w : Nat
hw : w✝ = w.succ
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs.mulRec rhs w✝).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
⊢ (((input.cast ⋯).lhs.cast ⋯).get idx hidx).gate < aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals