-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool}:
    (⟦aig, ⟨start, h1⟩, projectLeftAssign assign⟧ = false)
      →
    CNF.eval assign (([(.inr ⟨start, h1⟩, true)] :: (go aig start h1 (.empty aig)).val.cnf)) = false

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Tactic:
match heval1:(go aig start h1 (State.empty aig)).val.cnf.eval assign with
| true =>
  have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval
  specialize heval2 assign heval1 start h1 go_marks
  simp only [h, projectRightAssign_property, Bool.false_eq] at heval2
  simp [heval2]
| false =>
  simp [heval1]

Result:
no goals

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
⊢ ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false →
    CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Tactic:
intro h

Result:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 :
  ∀ (assign : aig.CNFVar → Bool),
    CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true →
      ∀ (idx : Nat) (hbound : idx < aig.decls.size),
        (go aig start h1 (State.empty aig)).val.cache.marks[idx] = true →
          ⟦projectLeftAssign assign, { aig := aig, ref := { gate := idx, hgate := hbound } }⟧ =
            projectRightAssign assign idx hbound
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Tactic:
specialize heval2 assign heval1 start h1 go_marks

Result:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 :
  ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = projectRightAssign assign start h1
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = false
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Tactic:
simp [heval1]

Result:
no goals

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Tactic:
have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval

Result:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 :
  ∀ (assign : aig.CNFVar → Bool),
    CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true →
      ∀ (idx : Nat) (hbound : idx < aig.decls.size),
        (go aig start h1 (State.empty aig)).val.cache.marks[idx] = true →
          ⟦projectLeftAssign assign, { aig := aig, ref := { gate := idx, hgate := hbound } }⟧ =
            projectRightAssign assign idx hbound
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 :
  ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = projectRightAssign assign start h1
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Tactic:
simp only [h, projectRightAssign_property, Bool.false_eq] at heval2

Result:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 : assign (Sum.inr ⟨start, h1⟩) = false
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 : assign (Sum.inr ⟨start, h1⟩) = false
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

Tactic:
simp [heval2]

Result:
no goals