-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α} :
    ⟦aig.mkAtomCached var, assign⟧ = ⟦aig.mkAtom var, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
⊢ ⟦assign, aig.mkAtomCached var⟧ = ⟦assign, aig.mkAtom var⟧

Tactic:
simp only [mkAtomCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
⊢ ⟦assign,
      match aig.cache.get? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              invariant := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }⟧ =
    ⟦assign, aig.mkAtom var⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
⊢ ⟦assign,
      match aig.cache.get? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              invariant := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }⟧ =
    ⟦assign, aig.mkAtom var⟧

Tactic:
split

Result:
case h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.get? (Decl.atom var) = some hit✝
⊢ ⟦assign,
      { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }⟧ =
    ⟦assign, aig.mkAtom var⟧

case h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.get? (Decl.atom var) = none
⊢ ⟦assign,
      {
        aig :=
          { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
            invariant := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } }⟧ =
    ⟦assign, aig.mkAtom var⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq1 : aig.cache.get? (Decl.atom var) = some hit✝
⊢ ⟦assign,
      { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }⟧ =
    ⟦assign, aig.mkAtom var⟧

Tactic:
rw [denote_mkAtom_cached heq1]

Result:
no goals

Proof state:
case h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.get? (Decl.atom var) = some hit✝
⊢ ⟦assign,
      { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }⟧ =
    ⟦assign, aig.mkAtom var⟧

Tactic:
next heq1 =>
rw [denote_mkAtom_cached heq1]

Result:
no goals

Proof state:
case h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.get? (Decl.atom var) = none
⊢ ⟦assign,
      {
        aig :=
          { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
            invariant := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } }⟧ =
    ⟦assign, aig.mkAtom var⟧

Tactic:
simp [mkAtom, denote]

Result:
no goals