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

State before:
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (P.iff_ Q)).imp_ ((exists_ v Q).imp_ (exists_ v P)))
Tactic:
apply deduction_theorem
State after:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v (P.iff_ Q)}) ((exists_ v Q).imp_ (exists_ v P))

State before:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v (P.iff_ Q)}) ((exists_ v Q).imp_ (exists_ v P))
Tactic:
simp
State after:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((exists_ v Q).imp_ (exists_ v P))

State before:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((exists_ v Q).imp_ (exists_ v P))
Tactic:
apply IsDeduct.mp_ (forall_ v (Q.iff_ P))
State after:
case h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((forall_ v (Q.iff_ P)).imp_ ((exists_ v Q).imp_ (exists_ v P)))

case h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (forall_ v (Q.iff_ P))

State before:
case h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((forall_ v (Q.iff_ P)).imp_ ((exists_ v Q).imp_ (exists_ v P)))
Tactic:
apply proof_imp_deduct
State after:
case h1.a.h1
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (Q.iff_ P)).imp_ ((exists_ v Q).imp_ (exists_ v P)))

State before:
case h1.a.h1
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (Q.iff_ P)).imp_ ((exists_ v Q).imp_ (exists_ v P)))
Tactic:
apply T_19_6_left Q P v
State after:
no goals

State before:
case h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (forall_ v (Q.iff_ P))
Tactic:
apply generalization
State after:
case h1.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (Q.iff_ P)

case h1.a.h2
P Q : Formula
v : VarName
⊢ ∀ H ∈ {forall_ v (P.iff_ Q)}, ¬isFreeIn v H

State before:
case h1.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (Q.iff_ P)
Tactic:
apply IsDeduct.mp_ (P.iff_ Q)
State after:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((P.iff_ Q).imp_ (Q.iff_ P))

case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (P.iff_ Q)

State before:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((P.iff_ Q).imp_ (Q.iff_ P))
Tactic:
simp only [def_iff_]
State after:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} (((P.imp_ Q).and_ (Q.imp_ P)).imp_ ((Q.imp_ P).and_ (P.imp_ Q)))

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

State before:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_}
    (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ ((Q.imp_ P).imp_ (P.imp_ Q).not_).not_)
Tactic:
SC
State after:
no goals

State before:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (P.iff_ Q)
Tactic:
apply specId v
State after:
case h1.a.h1.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (forall_ v (P.iff_ Q))

State before:
case h1.a.h1.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (forall_ v (P.iff_ Q))
Tactic:
apply IsDeduct.assume_
State after:
case h1.a.h1.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v (P.iff_ Q) ∈ {forall_ v (P.iff_ Q)}

State before:
case h1.a.h1.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v (P.iff_ Q) ∈ {forall_ v (P.iff_ Q)}
Tactic:
simp
State after:
no goals

State before:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ∀ H ∈ {forall_ v (P.iff_ Q)}, ¬isFreeIn v H
Tactic:
simp
State after:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v (P.iff_ Q))

State before:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v (P.iff_ Q))
Tactic:
simp only [isFreeIn]
State after:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ (isFreeIn v P ∨ isFreeIn v Q))

State before:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ (isFreeIn v P ∨ isFreeIn v Q))
Tactic:
simp
State after:
no goals