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

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

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