Theorem: AIG.RelabelNat.State.ofAIG.Inv1 (LeanSAT/AIG/RelabelNat.lean)

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ ∃ n, State.Inv1 n (ofAIG aig)
Tactic:
exists (ofAIGAux aig).max
State after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIG aig)

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIG aig)
Tactic:
dsimp [ofAIG]
State after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIGAux aig).map

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIGAux aig).map
Tactic:
exact (ofAIGAux aig).inv1
State after:
no goals