Theorem: AIG.toCNF.go_marked (LeanSAT/AIG/CNF.lean)

State before:
aig : AIG Nat
start : Nat
h : start < aig.decls.size
state : State aig
⊢ start < (go aig start h state).val.cache.marks.size
Tactic:
have := (go aig start h state).val.cache.hmarks
State after:
aig : AIG Nat
start : Nat
h : start < aig.decls.size
state : State aig
this : (go aig start h state).val.cache.marks.size = aig.decls.size
⊢ start < (go aig start h state).val.cache.marks.size

State before:
aig : AIG Nat
start : Nat
h : start < aig.decls.size
state : State aig
this : (go aig start h state).val.cache.marks.size = aig.decls.size
⊢ start < (go aig start h state).val.cache.marks.size
Tactic:
omega
State after:
no goals