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

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

State before:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P).iff_ (forall_ v P.not_.not_).not_.not_)
Tactic:
apply C_18_4 P P.not_.not_ ((forall_ v P).iff_ (forall_ v P).not_.not_)
State after:
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).iff_ (forall_ v P).not_.not_)
    ((forall_ v P).iff_ (forall_ v P.not_.not_).not_.not_)

case h2
P : Formula
v : VarName
⊢ IsProof (P.iff_ P.not_.not_)

case h3
P : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v P).iff_ (forall_ v P).not_.not_)

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

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

State before:
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_).not_
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).imp_
        ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_).not_
Tactic:
apply IsReplOfFormulaInFormula.not_
State after:
case h1.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_)
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).imp_
      ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_)

State before:
case h1.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_)
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).imp_
      ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_)
Tactic:
apply IsReplOfFormulaInFormula.imp_
State after:
case h1.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).imp_ (forall_ v P).not_.not_)
    ((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_)

case h1.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_
    ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_

State before:
case h1.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).imp_ (forall_ v P).not_.not_)
    ((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_)
Tactic:
apply IsReplOfFormulaInFormula.imp_
State after:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P)

case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_.not_ (forall_ v P.not_.not_).not_.not_

State before:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P)
Tactic:
apply IsReplOfFormulaInFormula.same_
State after:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ forall_ v P = forall_ v P

State before:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ forall_ v P = forall_ v P
Tactic:
rfl
State after:
no goals

State before:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_.not_ (forall_ v P.not_.not_).not_.not_
Tactic:
apply IsReplOfFormulaInFormula.not_
State after:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_ (forall_ v P.not_.not_).not_

State before:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_ (forall_ v P.not_.not_).not_
Tactic:
apply IsReplOfFormulaInFormula.not_
State after:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P.not_.not_)

State before:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P.not_.not_)
Tactic:
apply IsReplOfFormulaInFormula.forall_
State after:
case h1.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ P P.not_.not_

State before:
case h1.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ P P.not_.not_
Tactic:
apply IsReplOfFormulaInFormula.diff_
State after:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P = P

case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P.not_.not_ = P.not_.not_

State before:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P = P
Tactic:
rfl
State after:
no goals

State before:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P.not_.not_ = P.not_.not_
Tactic:
rfl
State after:
no goals

State before:
case h1.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_
    ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_
Tactic:
apply IsReplOfFormulaInFormula.not_
State after:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).not_.not_.imp_ (forall_ v P))
    ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P))

State before:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).not_.not_.imp_ (forall_ v P))
    ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P))
Tactic:
apply IsReplOfFormulaInFormula.imp_
State after:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_.not_ (forall_ v P.not_.not_).not_.not_

case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P)

State before:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_.not_ (forall_ v P.not_.not_).not_.not_
Tactic:
apply IsReplOfFormulaInFormula.not_
State after:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_ (forall_ v P.not_.not_).not_

State before:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_ (forall_ v P.not_.not_).not_
Tactic:
apply IsReplOfFormulaInFormula.not_
State after:
case h1.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P.not_.not_)

State before:
case h1.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P.not_.not_)
Tactic:
apply IsReplOfFormulaInFormula.forall_
State after:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ P P.not_.not_

State before:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ P P.not_.not_
Tactic:
apply IsReplOfFormulaInFormula.diff_
State after:
case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P = P

case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P.not_.not_ = P.not_.not_

State before:
case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P = P
Tactic:
rfl
State after:
no goals

State before:
case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P.not_.not_ = P.not_.not_
Tactic:
rfl
State after:
no goals

State before:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P)
Tactic:
apply IsReplOfFormulaInFormula.same_
State after:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ forall_ v P = forall_ v P

State before:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ forall_ v P = forall_ v P
Tactic:
rfl
State after:
no goals

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

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

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

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

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

State before:
case h3
P : Formula
v : VarName
⊢ IsDeduct ∅ (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_).not_
Tactic:
SC
State after:
no goals