-- 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:
case mk.push_cache.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✝.insert decl' decls✝.size, ⋯⟩.val[decl]? = some idx
h✝ : ¬idx < decls✝.size
⊢ decl' = decl

Tactic:
next hbounds =>
simp only [HashMap.getElem?_insert] at hfound
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:
case mk.push_cache
α : 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
⊢ (decls✝.push decl')[idx] = decl

Tactic:
rw [Array.getElem_push]

Result:
case mk.push_cache
α : 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
⊢ (if h : idx < decls✝.size then decls✝[idx] else decl') = 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 α
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:
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 α
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

Proof state:
case mk.push_cache
α : 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
⊢ (decls✝.push decl✝)[idx] = decl

Tactic:
rename_i decl'

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

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

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'
⊢ decls✝[idx] = decl

Tactic:
simp [heq] 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 α
h✝ : idx < decls✝.size
heq : decl = decl'
hfound : decls✝.size = idx
⊢ decls✝[idx] = decl

Proof state:
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

Tactic:
simpa [BEq.symm_false heq] using hfound

Result:
no goals