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

State before:
P Q : Formula
⊢ ((P.or_ Q).iff_ (P.not_.imp_ Q)).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
State after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.or_ Q).iff_ (P.not_.imp_ Q))

State before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.or_ Q).iff_ (P.not_.imp_ Q))
Tactic:
simp only [eval_or, eval_not, eval_imp, eval_iff]
State after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V P ∨ evalPrime V Q ↔ ¬evalPrime V P → evalPrime V Q

State before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V P ∨ evalPrime V Q ↔ ¬evalPrime V P → evalPrime V Q
Tactic:
tauto
State after:
no goals