Theorem: FOL.NV.prop_complete (FOL/NV/Margaris/Prop.lean)

State before:
P : Formula
h1 : P.IsTautoPrime
⊢ IsProof P
Tactic:
simp only [IsProof]
State after:
P : Formula
h1 : P.IsTautoPrime
⊢ IsDeduct ∅ P

State before:
P : Formula
h1 : P.IsTautoPrime
⊢ IsDeduct ∅ P
Tactic:
apply propCompleteAux P P.primeSet
State after:
case h1
P : Formula
h1 : P.IsTautoPrime
⊢ P.primeSet ⊆ P.primeSet

case h2
P : Formula
h1 : P.IsTautoPrime
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P

State before:
case h1
P : Formula
h1 : P.IsTautoPrime
⊢ P.primeSet ⊆ P.primeSet
Tactic:
rfl
State after:
no goals

State before:
case h2
P : Formula
h1 : P.IsTautoPrime
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P
Tactic:
intro V
State after:
case h2
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P

State before:
case h2
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ IsDeduct (↑(Finset.image (evalPrimeFfToNot V) P.primeSet)) P
Tactic:
apply L_15_7 P P P.primeSet V (P.primeSet.image (evalPrimeFfToNot V))
State after:
case h2.h1
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ ↑P.primeSet ⊆ ↑P.primeSet

case h2.h2
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ ↑(Finset.image (evalPrimeFfToNot V) P.primeSet) = evalPrimeFfToNot V '' ↑P.primeSet

case h2.h3
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P

State before:
case h2.h1
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ ↑P.primeSet ⊆ ↑P.primeSet
Tactic:
rfl
State after:
no goals

State before:
case h2.h2
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ ↑(Finset.image (evalPrimeFfToNot V) P.primeSet) = evalPrimeFfToNot V '' ↑P.primeSet
Tactic:
simp only [Finset.coe_image]
State after:
no goals

State before:
case h2.h3
P : Formula
h1 : P.IsTautoPrime
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P
Tactic:
simp only [Formula.IsTautoPrime] at h1
State after:
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P

State before:
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = evalPrimeFfToNot V P
Tactic:
simp only [evalPrimeFfToNot]
State after:
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = if evalPrime V P then P else P.not_

State before:
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = if evalPrime V P then P else P.not_
Tactic:
specialize h1 V
State after:
case h2.h3
P : Formula
V : VarBoolAssignment
h1 : evalPrime V P
⊢ P = if evalPrime V P then P else P.not_

State before:
case h2.h3
P : Formula
V : VarBoolAssignment
h1 : evalPrime V P
⊢ P = if evalPrime V P then P else P.not_
Tactic:
simp only [if_pos h1]
State after:
no goals