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

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

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
aig : AIG α
a : α
ha : (ofAIG aig).find? a = some n
a' : α
ha' : (ofAIG aig).find? a' = some n
⊢ a = a'
Tactic:
rcases ofAIG.Inv1 aig with ⟨n, hn⟩
State after:
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
n✝ : Nat
aig : AIG α
a : α
ha : (ofAIG aig).find? a = some n✝
a' : α
ha' : (ofAIG aig).find? a' = some n✝
n : Nat
hn : Inv1 n (ofAIG aig)
⊢ a = a'

State before:
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
n✝ : Nat
aig : AIG α
a : α
ha : (ofAIG aig).find? a = some n✝
a' : α
ha' : (ofAIG aig).find? a' = some n✝
n : Nat
hn : Inv1 n (ofAIG aig)
⊢ a = a'
Tactic:
apply Inv1.property <;> assumption
State after:
no goals