-- 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✝
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') = false
⊢ False

Tactic:
apply hbounds

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

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

Tactic:
apply hbounds

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

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
⊢ decl' = decl

Tactic:
match heq : decl == decl' with
| true =>
  apply Eq.symm
  simpa using heq
| false =>
  exfalso
  apply hbounds
  simp only [BEq.symm_false heq, cond_false] at hfound
  specialize ih _ hfound
  apply Array.lt_of_getElem
  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 α
hbounds : ¬idx < decls✝.size
hfound : (if (decl' == decl) = true then some decls✝.size else cache✝[decl]?) = some idx
heq : (decl == decl') = false
⊢ idx < decls✝.size

Tactic:
simp only [BEq.symm_false heq, cond_false] at hfound

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

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

Tactic:
exfalso

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

Proof state:
case mk.push_id.isFalse
α : 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
⊢ decl✝ = decl

Tactic:
next hbounds =>
exfalso
apply hbounds
specialize ih _ hfound
apply Array.lt_of_getElem
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 α
hfound : ⟨cache✝.insert decl' decls✝.size, ⋯⟩.val[decl]? = some idx
hbounds : ¬idx < decls✝.size
⊢ decl' = decl

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

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

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

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

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

Tactic:
specialize ih _ hfound

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