-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkConstCached_le_size (aig : AIG α) (val : Bool) :
    aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size

Proof state:
case h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.get? (Decl.const val) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size

Tactic:
simp

Result:
no goals

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

Tactic:
simp_arith

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
⊢ aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size

Tactic:
dsimp only [mkConstCached]

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

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

Tactic:
split

Result:
case h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.get? (Decl.const val) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size

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