-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem denote_mkGate_cached {aig : AIG α} {input} {hit} :
    aig.cache.get? (.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
      →
    ⟦⟨aig, hit.idx, hit.hbound⟩, assign⟧
      =
    ⟦aig.mkGate input, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ ⟦assign, { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }⟧ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Tactic:
conv =>
  lhs
  unfold denote denote.go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := hit.idx,
                  hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ ⟦assign, { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }⟧ = ⟦assign, aig.mkGate input⟧

Tactic:
simp only [denote_mkGate]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ ⟦assign, { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }⟧ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := hit.idx,
                  hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Tactic:
split <;> simp_all[denote]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
⊢ ⟦assign, { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }⟧ = ⟦assign, aig.mkGate input⟧

Tactic:
have := hit.hvalid

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ ⟦assign, { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }⟧ = ⟦assign, aig.mkGate input⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
⊢ aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit →
    ⟦assign, { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }⟧ = ⟦assign, aig.mkGate input⟧

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
⊢ ⟦assign, { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }⟧ = ⟦assign, aig.mkGate input⟧