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

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv2 aig.decls aig.decls.size (ofAIG aig)
Tactic:
have := (ofAIGAux aig).inv2
State after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
this : State.Inv2 aig.decls aig.decls.size (ofAIGAux aig).map
⊢ State.Inv2 aig.decls aig.decls.size (ofAIG aig)

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
this : State.Inv2 aig.decls aig.decls.size (ofAIGAux aig).map
⊢ State.Inv2 aig.decls aig.decls.size (ofAIG aig)
Tactic:
simp [ofAIG, this]
State after:
no goals