Theorem: AIG.RelabelNat.State.ofAIG_find_some (LeanSAT/AIG/RelabelNat.lean)

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ ∀ (a : α), a ∈ aig → ∃ n, (ofAIG aig).find? a = some n
Tactic:
intro a ha
State after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : a ∈ aig
⊢ ∃ n, (ofAIG aig).find? a = some n

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : a ∈ aig
⊢ ∃ n, (ofAIG aig).find? a = some n
Tactic:
simp only [mem_def] at ha
State after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
⊢ ∃ n, (ofAIG aig).find? a = some n

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
⊢ ∃ n, (ofAIG aig).find? a = some n
Tactic:
rcases Array.get_of_mem ha with ⟨⟨i, isLt⟩, hi⟩
State after:
case intro.mk
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ∃ n, (ofAIG aig).find? a = some n

State before:
case intro.mk
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ∃ n, (ofAIG aig).find? a = some n
Tactic:
apply Inv2.property
State after:
case intro.mk.a
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.decls[?intro.mk.idx] = Decl.atom a

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

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

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

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

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

State before:
case intro.mk.a
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.decls[?intro.mk.idx] = Decl.atom a

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

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

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

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

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.idx < ?intro.mk.upper
Tactic:
. assumption
State after:
case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

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

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < ?intro.mk.upper

State before:
case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

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

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < ?intro.mk.upper
Tactic:
. exact aig.decls.size
State after:
case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 aig.decls aig.decls.size (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size

State before:
case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 aig.decls aig.decls.size (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size
Tactic:
. apply ofAIG.Inv2
State after:
case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size

State before:
case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size
Tactic:
. omega
State after:
no goals

State before:
case intro.mk.a
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.decls[?intro.mk.idx] = Decl.atom a
Tactic:
assumption
State after:
no goals

State before:
case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat
Tactic:
exact aig.decls.size
State after:
no goals

State before:
case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 aig.decls aig.decls.size (ofAIG aig)
Tactic:
apply ofAIG.Inv2
State after:
no goals

State before:
case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < aig.decls.size
Tactic:
omega
State after:
no goals