-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem mkFullAdder_denote_mem_prefix (aig : AIG α) (input : FullAdderInput aig) (start : Nat)
    (hstart) :
    ⟦
      (mkFullAdder aig input).aig,
      ⟨start, Nat.lt_of_lt_of_le hstart (FullAdderOutput.hle _)⟩,
      assign
    ⟧
      =
    ⟦aig, ⟨start, hstart⟩, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦assign,
      { aig := (mkFullAdderCarry (mkFullAdderOut aig input).aig (input.cast ⋯)).aig,
        ref := { gate := start, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦assign, { aig := (mkFullAdderOut aig input).aig, ref := { gate := start, hgate := ?m.8615 } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < (mkFullAdderOut aig input).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦assign, { aig := (mkFullAdderOut aig input).aig, ref := { gate := start, hgate := ?m.8615 } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < (mkFullAdderOut aig input).aig.decls.size

Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦assign,
      {
        aig :=
          (let res := mkFullAdderOut aig input;
            let aig_1 := res.aig;
            let outRef := res.ref;
            let_fun haig1 := ⋯;
            let input_1 := input.cast haig1;
            let res_1 := mkFullAdderCarry aig_1 input_1;
            let aig_2 := res_1.aig;
            let carryRef := res_1.ref;
            let_fun haig2 := ⋯;
            let outRef := outRef.cast haig2;
            let_fun hle := ⋯;
            { aig := aig_2, out := outRef, cout := carryRef, hle := hle }).aig,
        ref := { gate := start, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦assign,
      { aig := (mkFullAdderCarry (mkFullAdderOut aig input).aig (input.cast ⋯)).aig,
        ref := { gate := start, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦assign, { aig := (mkFullAdder aig input).aig, ref := { gate := start, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

Tactic:
unfold mkFullAdder

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦assign,
      {
        aig :=
          (let res := mkFullAdderOut aig input;
            let aig_1 := res.aig;
            let outRef := res.ref;
            let_fun haig1 := ⋯;
            let input_1 := input.cast haig1;
            let res_1 := mkFullAdderCarry aig_1 input_1;
            let aig_2 := res_1.aig;
            let carryRef := res_1.ref;
            let_fun haig2 := ⋯;
            let outRef := outRef.cast haig2;
            let_fun hle := ⋯;
            { aig := aig_2, out := outRef, cout := carryRef, hle := hle }).aig,
        ref := { gate := start, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧