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

Proof state:
α : 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✝
decl : Decl α
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
hbounds : ¬idx < decls✝.size
ih : decls✝[idx] = decl
⊢ idx < decls✝.size

Tactic:
apply Array.lt_of_getElem

Result:
case x
α : 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✝
decl : Decl α
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
hbounds : ¬idx < decls✝.size
ih : decls✝[idx] = decl
⊢ decls✝[idx] = ?x

case x
α : 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✝
decl : Decl α
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
hbounds : ¬idx < decls✝.size
ih : decls✝[idx] = decl
⊢ Decl α

case hidx
α : 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✝
decl : Decl α
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
hbounds : ¬idx < decls✝.size
ih : decls✝[idx] = decl
⊢ idx < decls✝.size

Proof state:
case mk.push_id.isTrue.hfound
α : 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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
h✝ : idx < decls✝.size
⊢ ⟨cache✝, wf⟩.val[decl]? = some idx

Tactic:
simp [hfound]

Result:
no goals

Proof state:
case mk.push_id.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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
h✝ : idx < decls✝.size
⊢ decls✝[idx] = decl

Tactic:
apply ih

Result:
case mk.push_id.isTrue.hfound
α : 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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
hfound : ⟨cache✝, ⋯⟩.val[decl]? = some idx
h✝ : idx < decls✝.size
⊢ ⟨cache✝, wf⟩.val[decl]? = some idx

Proof state:
α : 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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
h✝ : idx < decls✝.size
hfound : (if (decl' == decl) = true then some decls✝.size else cache✝[decl]?) = some idx
heq : (decl == decl') = true
⊢ decls✝[idx] = decl

Tactic:
simp only [beq_iff_eq] at heq

Result:
α : 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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
h✝ : idx < decls✝.size
hfound : (if (decl' == decl) = true then some decls✝.size else cache✝[decl]?) = some idx
heq : decl = decl'
⊢ decls✝[idx] = decl

Proof state:
α : 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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
hbounds : ¬idx < decls✝.size
hfound : (if (decl' == decl) = true then some decls✝.size else cache✝[decl]?) = some idx
heq : (decl == decl') = true
⊢ decl' = decl

Tactic:
apply Eq.symm

Result:
case h
α : 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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
hbounds : ¬idx < decls✝.size
hfound : (if (decl' == decl) = true then some decls✝.size else cache✝[decl]?) = some idx
heq : (decl == decl') = true
⊢ decl = decl'

Proof state:
case h
α : 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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
hbounds : ¬idx < decls✝.size
hfound : (if (decl' == decl) = true then some decls✝.size else cache✝[decl]?) = some idx
heq : (decl == decl') = true
⊢ decl = decl'

Tactic:
simpa using heq

Result:
no goals

Proof state:
case x
α : 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✝
decl : Decl α
hbounds : ¬idx < decls✝.size
heq : (decl == decl') = false
hfound : (if false = true then some decls✝.size else cache✝[decl]?) = some idx
ih : decls✝[idx] = decl
⊢ decls✝[idx] = ?x

case x
α : 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✝
decl : Decl α
hbounds : ¬idx < decls✝.size
heq : (decl == decl') = false
hfound : (if false = true then some decls✝.size else cache✝[decl]?) = some idx
ih : decls✝[idx] = decl
⊢ Decl α

case hidx
α : 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✝
decl : Decl α
hbounds : ¬idx < decls✝.size
heq : (decl == decl') = false
hfound : (if false = true then some decls✝.size else cache✝[decl]?) = some idx
ih : decls✝[idx] = decl
⊢ idx < decls✝.size

Tactic:
assumption

Result:
no goals

Proof state:
α : 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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
h✝ : idx < decls✝.size
hfound : (if (decl' == decl) = true then some decls✝.size else cache✝[decl]?) = some idx
heq : (decl == decl') = false
⊢ decls✝[idx] = decl

Tactic:
apply ih

Result:
case hfound
α : 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✝
ih : ∀ (decl : Decl α) (hfound : ⟨cache✝, wf⟩.val[decl]? = some idx), decls✝[idx] = decl
decl : Decl α
h✝ : idx < decls✝.size
hfound : (if (decl' == decl) = true then some decls✝.size else cache✝[decl]?) = some idx
heq : (decl == decl') = false
⊢ ⟨cache✝, wf⟩.val[decl]? = some idx