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

State before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
⊢ (go aig start h1 state).val.sat (cnfSatAssignment aig assign1)
Tactic:
have := (go aig start h1 state).val.inv assign1
State after:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
this : (go aig start h1 state).val.cnf.sat (cnfSatAssignment aig assign1)
⊢ (go aig start h1 state).val.sat (cnfSatAssignment aig assign1)

State before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
this : (go aig start h1 state).val.cnf.sat (cnfSatAssignment aig assign1)
⊢ (go aig start h1 state).val.sat (cnfSatAssignment aig assign1)
Tactic:
simp [this]
State after:
no goals