-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem denote_blastAdd (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
      (input : BinaryRefVec aig w)
      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
      ∀ (idx : Nat) (hidx : idx < w),
          ⟦(blastAdd aig input).aig, (blastAdd aig input).vec.get idx hidx, assign⟧
            =
          (lhs + rhs).getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (blastAdd.go (aig.mkConstCached false).aig (input.cast ⋯).lhs (input.cast ⋯).rhs 0 ⋯
              (aig.mkConstCached false).ref RefVec.empty).aig,
        ref :=
          (blastAdd.go (aig.mkConstCached false).aig (input.cast ⋯).lhs (input.cast ⋯).rhs 0 ⋯
                  (aig.mkConstCached false).ref RefVec.empty).vec.get
            idx hidx }⟧ =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ ^^ BitVec.carry idx lhs rhs false))

Tactic:
rw [blastAdd.go_denote_eq _ 0 (by omega) _ _ _ _ assign lhs rhs _ _]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ (⟦assign, { aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.get idx hidx }⟧ ^^
        BitVec.carry idx lhs rhs false)) =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ ^^ BitVec.carry idx lhs rhs false))

case hcin
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }⟧ =
    BitVec.carry 0 lhs rhs false

case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ 0 ≤ idx

α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.get idx hidx }⟧ = lhs.getLsbD idx

α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.get idx hidx }⟧ = rhs.getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastAdd aig input).aig, ref := (blastAdd aig input).vec.get idx hidx }⟧ =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ ^^ BitVec.carry idx lhs rhs false))

Tactic:
unfold blastAdd

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      {
        aig :=
          (let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let cin := res.ref;
            let input := input.cast ⋯;
            match input with
            | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 lhs rhs 0 ⋯ cin RefVec.empty).aig,
        ref :=
          (let res := aig.mkConstCached false;
                let aig_1 := res.aig;
                let cin := res.ref;
                let input := input.cast ⋯;
                match input with
                | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 lhs rhs 0 ⋯ cin RefVec.empty).vec.get
            idx hidx }⟧ =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ ^^ BitVec.carry idx lhs rhs false))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (blastAdd aig input).aig, ref := (blastAdd aig input).vec.get idx hidx }⟧ =
      (lhs + rhs).getLsbD idx

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastAdd aig input).aig, ref := (blastAdd aig input).vec.get idx hidx }⟧ = (lhs + rhs).getLsbD idx