Theorem: FOL.NV.T_19_3 (FOL/NV/Margaris/Fol.lean)

State before:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P.not_).iff_ (exists_ v P).not_)
Tactic:
simp only [def_exists_]
State after:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P.not_).iff_ (forall_ v P.not_).not_.not_)

State before:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P.not_).iff_ (forall_ v P.not_).not_.not_)
Tactic:
simp only [def_iff_]
State after:
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).and_ ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)))

State before:
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).and_ ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)))
Tactic:
simp only [def_and_]
State after:
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).imp_
        ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)).not_).not_

State before:
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).imp_
        ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)).not_).not_
Tactic:
SC
State after:
no goals