-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem ofAIG_find_some {aig : AIG α} : ∀ a ∈ aig, ∃ n, (ofAIG aig)[a]? = some n

Proof state:
case intro.intro.hidx
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ i < aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
⊢ ∃ n, (ofAIG aig)[a]? = some n

Tactic:
rcases Array.getElem_of_mem ha with ⟨i, isLt, hi⟩

Result:
case intro.intro
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ ∃ n, (ofAIG aig)[a]? = some n

Proof state:
case intro.intro.heq
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ ?intro.intro.decls[?intro.intro.idx] = Decl.atom a

Tactic:
assumption

Result:
no goals

Proof state:
case intro.intro.hinv
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ Inv2 aig.decls aig.decls.size (ofAIG aig)

Tactic:
apply ofAIG.Inv2

Result:
no goals

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : a ∈ aig
⊢ ∃ n, (ofAIG aig)[a]? = some n

Tactic:
simp only [mem_def] at ha

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
⊢ ∃ n, (ofAIG aig)[a]? = some n

Proof state:
case intro.intro.upper
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ Nat

Tactic:
exact aig.decls.size

Result:
no goals

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
⊢ ∀ (a : α), a ∈ aig → ∃ n, (ofAIG aig)[a]? = some n

Tactic:
intro a ha

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : a ∈ aig
⊢ ∃ n, (ofAIG aig)[a]? = some n

Proof state:
case intro.intro
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ ∃ n, (ofAIG aig)[a]? = some n

Tactic:
apply Inv2.property

Result:
case intro.intro.heq
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ ?intro.intro.decls[?intro.intro.idx] = Decl.atom a

case intro.intro.decls
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ Array (Decl α)

case intro.intro.idx
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ Nat

case intro.intro.upper
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ Nat

case intro.intro.hidx
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ ?intro.intro.idx < ?intro.intro.upper

case intro.intro.hinv
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[i] = Decl.atom a
⊢ Inv2 ?intro.intro.decls ?intro.intro.upper (ofAIG aig)