Theorem: AIG.mkAtomCached_hit_aig (LeanSAT/AIG/CachedLemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hit : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.find? (Decl.atom var) = some hit
⊢ (aig.mkAtomCached var).aig = aig
Tactic:
simp only [mkAtomCached]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hit : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.find? (Decl.atom var) = some hit
⊢ (match aig.cache.find? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }).aig =
    aig

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hit : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.find? (Decl.atom var) = some hit
⊢ (match aig.cache.find? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }).aig =
    aig
Tactic:
split <;> simp_all
State after:
no goals