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

Tactic:
omega

Result:
no goals

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

Tactic:
simp at hfound

Result:
no goals

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

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

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

Tactic:
rw [Array.getElem_push]

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

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

Tactic:
split

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

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

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 α
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

Tactic:
assumption

Result:
no goals

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

Tactic:
split

Result:
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

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

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

Tactic:
match heq : decl == decl' with
| true =>
  simp only [beq_iff_eq] at heq
  simp [heq] at hfound
  omega
| false =>
  apply ih
  simpa [BEq.symm_false heq] using hfound

Result:
no goals