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

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
⊢ aig.decls.size ≤ (aig.mkAtomCached var).aig.decls.size
Tactic:
dsimp [mkAtomCached]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
⊢ aig.decls.size ≤
    (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.decls.size

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
⊢ aig.decls.size ≤
    (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.decls.size
Tactic:
split
State after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.find? (Decl.atom var) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            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.decls.size

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.find? (Decl.atom var) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            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.decls.size
Tactic:
. simp
State after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            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.decls.size

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            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.decls.size
Tactic:
. simp_arith
State after:
no goals

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.find? (Decl.atom var) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size
Tactic:
simp
State after:
no goals

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ aig.decls.size ≤
    {
            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.decls.size
Tactic:
simp_arith
State after:
no goals