-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem denote_mkConst_cached {aig : AIG α} {hit} :
    aig.cache.get? (.const b) = some hit
      →
    ⟦aig, ⟨hit.idx, hit.hbound⟩, assign⟧ = ⟦aig.mkConst b, assign⟧

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

Tactic:
have := hit.hvalid

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

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

Tactic:
simp only [denote_mkConst]

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

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

Tactic:
unfold denote denote.go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
b : Bool
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const b)
this : aig.decls[hit.idx] = Decl.const b
⊢ aig.cache.get? (Decl.const b) = some hit →
    (match elem :
        { aig := aig,
                ref :=
                  { gate := hit.idx,
                    hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
      | Decl.const b_1 => b_1
      | 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)) =
      b

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
b : Bool
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const b)
this : aig.decls[hit.idx] = Decl.const b
⊢ aig.cache.get? (Decl.const b) = some hit →
    (match elem :
        { aig := aig,
                ref :=
                  { gate := hit.idx,
                    hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
      | Decl.const b_1 => b_1
      | 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)) =
      b

Tactic:
split <;> simp_all

Result:
no goals