-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦(go aig expr).val.aig, (go aig expr).val.vec.get idx hidx, assign.toAIGAssignment⟧
          =
        (expr.eval assign).getLsbD idx

Proof state:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment,
        { aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref := { lhs := (go aig lhs).1.vec.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.vec }.lhs.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx

Tactic:
intros

Result:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { lhs := (go aig lhs).1.vec.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.vec }.lhs.get idx✝ hidx✝ }⟧ =
    (eval assign lhs).getLsbD idx✝

Proof state:
case bin.umod.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.vec.cast ⋯).get idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals

Proof state:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦assign.toAIGAssignment, { aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).vec.get idx hidx }⟧ &&
      (eval assign rhs).getLsbD idx) =
    ((eval assign lhs).getLsbD idx && (eval assign rhs).getLsbD idx)

Tactic:
rw [← go_val_eq_bitblast]

Result:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ &&
      (eval assign rhs).getLsbD idx) =
    ((eval assign lhs).getLsbD idx && (eval assign rhs).getLsbD idx)

Proof state:
case shiftLeft.hright
w : Nat
assign : Assignment
m✝ n✝ : Nat
lhs : BVExpr m✝
rhs : BVExpr n✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < m✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < n✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < m✝
idx✝ : Nat
hidx✝ : idx✝ < { n := n✝, target := (go aig lhs).1.vec.cast ⋯, distance := (go (go aig lhs).1.aig rhs).1.vec }.n
⊢ ⟦assign.toAIGAssignment,
      { aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { n := n✝, target := (go aig lhs).1.vec.cast ⋯, distance := (go (go aig lhs).1.aig rhs).1.vec }.distance.get
            idx✝ hidx✝ }⟧ =
    (eval assign rhs).getLsbD idx✝

Tactic:
rw [← rih]

Result:
no goals

Proof state:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦assign.toAIGAssignment,
        { aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).vec.get idx hidx).cast ⋯ }⟧ ||
      (eval assign rhs).getLsbD idx) =
    ((eval assign lhs).getLsbD idx || (eval assign rhs).getLsbD idx)

Tactic:
rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)]

Result:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦assign.toAIGAssignment, { aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).vec.get idx hidx }⟧ ||
      (eval assign rhs).getLsbD idx) =
    ((eval assign lhs).getLsbD idx || (eval assign rhs).getLsbD idx)