-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Basic.lean
theorem Cache.get?_bounds {decls : Array (Decl α)} {idx : Nat} (c : Cache α decls) (decl : Decl α)
    (hfound : c.val[decl]? = some idx) :
    idx < decls.size

Proof state:
case mk.push_id
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl✝ : Decl α
wf : WF decls✝ cache✝
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
ih : idx < decls✝.size
⊢ idx < (decls✝.push decl✝).size

Tactic:
simp

Result:
case mk.push_id
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl✝ : Decl α
wf : WF decls✝ cache✝
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
ih : idx < decls✝.size
⊢ idx < decls✝.size + 1

Proof state:
case mk.push_id
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl✝ : Decl α
wf : WF decls✝ cache✝
ih : ⟨cache✝, wf⟩.val[decl]? = some idx → idx < decls✝.size
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
⊢ idx < (decls✝.push decl✝).size

Tactic:
specialize ih hfound

Result:
case mk.push_id
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl✝ : Decl α
wf : WF decls✝ cache✝
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
ih : idx < decls✝.size
⊢ idx < (decls✝.push decl✝).size

Proof state:
case mk.push_id
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl✝ : Decl α
wf : WF decls✝ cache✝
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
ih : idx < decls✝.size
⊢ idx < decls✝.size + 1

Tactic:
omega

Result:
no goals

Proof state:
case mk.push_cache.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
h : ¬decl' = decl
hfound : cache✝[decl]? = some idx
ih : idx < decls✝.size
⊢ idx < (decls✝.push decl').size

Tactic:
simp

Result:
case mk.push_cache.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
h : ¬decl' = decl
hfound : cache✝[decl]? = some idx
ih : idx < decls✝.size
⊢ idx < decls✝.size + 1

Proof state:
case mk.push_cache.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
ih : ⟨cache✝, wf⟩.val[decl]? = some idx → idx < decls✝.size
h : ¬decl' = decl
hfound : cache✝[decl]? = some idx
⊢ idx < (decls✝.push decl').size

Tactic:
specialize ih hfound

Result:
case mk.push_cache.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
h : ¬decl' = decl
hfound : cache✝[decl]? = some idx
ih : idx < decls✝.size
⊢ idx < (decls✝.push decl').size

Proof state:
case mk.push_cache.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
h : ¬decl' = decl
hfound : cache✝[decl]? = some idx
ih : idx < decls✝.size
⊢ idx < decls✝.size + 1

Tactic:
omega

Result:
no goals

Proof state:
case mk.empty
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
hfound : ⟨∅, ⋯⟩.val[decl]? = some idx
⊢ idx < decls✝.size

Tactic:
simp at hfound

Result:
no goals

Proof state:
case mk.push_cache
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
ih : ⟨cache✝, wf⟩.val[decl]? = some idx → idx < decls✝.size
hfound : (if decl' = decl then some decls✝.size else cache✝[decl]?) = some idx
⊢ idx < (decls✝.push decl').size

Tactic:
split at hfound <;> rename_i h

Result:
case mk.push_cache.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
ih : ⟨cache✝, wf⟩.val[decl]? = some idx → idx < decls✝.size
h : decl' = decl
hfound : some decls✝.size = some idx
⊢ idx < (decls✝.push decl').size

case mk.push_cache.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
ih : ⟨cache✝, wf⟩.val[decl]? = some idx → idx < decls✝.size
h : ¬decl' = decl
hfound : cache✝[decl]? = some idx
⊢ idx < (decls✝.push decl').size

Proof state:
case mk.push_cache.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
hfound : some decls✝.size = some idx
ih : ⟨cache✝, wf⟩.val[decl']? = some idx → idx < decls✝.size
⊢ idx < (decls✝.push decl').size

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.push_cache
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
ih : ⟨cache✝, wf⟩.val[decl]? = some idx → idx < decls✝.size
hfound : ⟨cache✝.insert decl' decls✝.size, ⋯⟩.val[decl]? = some idx
⊢ idx < (decls✝.push decl').size

Tactic:
simp only [HashMap.getElem?_insert, beq_iff_eq] at hfound

Result:
case mk.push_cache
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
ih : ⟨cache✝, wf⟩.val[decl]? = some idx → idx < decls✝.size
hfound : (if decl' = decl then some decls✝.size else cache✝[decl]?) = some idx
⊢ idx < (decls✝.push decl').size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
c : Cache α decls
decl : Decl α
hfound : c.val[decl]? = some idx
⊢ idx < decls.size

Tactic:
rcases c with ⟨cache, hcache⟩

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
hcache : WF decls cache
hfound : ⟨cache, hcache⟩.val[decl]? = some idx
⊢ idx < decls.size