-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
    (acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
    (hacc : ∀ (idx : Nat) (hidx : idx < w),
                ⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
                  =
                (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (go aig lhs rhs (curr + 1) acc).aig,
          (go aig lhs rhs (curr + 1) acc).vec.get idx hidx,
          assign.toAIGAssignment
        ⟧
          =
        (BitVec.mulRec lexpr rexpr w).getLsbD idx

Proof state:
case hleft
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝ : curr + 1 < w
hconstant : aig.isConstant (rhs.get (curr + 1) h✝) false = true
hgo : go aig lhs rhs (curr + 1 + 1) acc = res
⊢ ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx

Tactic:
exact hleft

Result:
no goals

Proof state:
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
hgo : go aig lhs rhs (curr + 1) acc = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lexpr.mulRec rexpr w).getLsbD idx

Tactic:
unfold go at hgo

Result:
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
hgo :
  (if h : curr + 1 < w then
      if aig.isConstant (rhs.get (curr + 1) h) false = true then go aig lhs rhs (curr + 1 + 1) acc
      else
        let res := blastShiftLeftConst aig { vec := lhs, distance := curr + 1 };
        let aig_1 := res.aig;
        let shifted := res.vec;
        let_fun this := ⋯;
        let lhs_1 := lhs.cast this;
        let rhs_1 := rhs.cast this;
        let acc_1 := acc.cast this;
        let res := blastAdd aig_1 { lhs := acc_1, rhs := shifted };
        let aig_2 := res.aig;
        let added := res.vec;
        let_fun this_1 := ⋯;
        let lhs_2 := lhs_1.cast this_1;
        let rhs_2 := rhs_1.cast this_1;
        let acc_2 := acc_1.cast this_1;
        let res := RefVec.ite aig_2 { discr := rhs_2.get (curr + 1) h, lhs := added, rhs := acc_2 };
        let aig_3 := res.aig;
        let acc_3 := res.vec;
        let_fun this := ⋯;
        let lhs := lhs_2.cast this;
        let rhs := rhs_2.cast this;
        go aig_3 lhs rhs (curr + 1 + 1) acc_3
    else { aig := aig, vec := acc }) =
    res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lexpr.mulRec rexpr w).getLsbD idx

Proof state:
case isFalse
w : Nat
aig : AIG BVBit
curr : Nat
hcurr : curr + 1 ≤ w
acc lhs rhs : aig.RefVec w
lexpr rexpr : BitVec w
assign : Assignment
hleft :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝ : ¬curr + 1 < w
hgo : { aig := aig, vec := acc } = res
this : curr + 1 = w
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lexpr.mulRec rexpr w).getLsbD idx

Tactic:
subst this

Result:
case isFalse
aig : AIG BVBit
curr : Nat
assign : Assignment
idx : Nat
hcurr : curr + 1 ≤ curr + 1
acc lhs rhs : aig.RefVec (curr + 1)
lexpr rexpr : BitVec (curr + 1)
hleft :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx
hacc :
  ∀ (idx : Nat) (hidx : idx < curr + 1),
    ⟦assign.toAIGAssignment, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx
hidx : idx < curr + 1
res : RefVecEntry BVBit (curr + 1)
h✝ : ¬curr + 1 < curr + 1
hgo : { aig := aig, vec := acc } = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (lexpr.mulRec rexpr (curr + 1)).getLsbD idx