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

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

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

State before:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((exists_ v P).imp_ Q)
Tactic:
simp only [def_exists_]
State after:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((forall_ v P.not_).not_.imp_ Q)

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

case h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (Q.not_.imp_ (forall_ v Q.not_))

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

case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((forall_ v Q.not_).imp_ (forall_ v P.not_))

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

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

case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (forall_ v (Q.not_.imp_ P.not_))

State before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((forall_ v (Q.not_.imp_ P.not_)).imp_ ((forall_ v Q.not_).imp_ (forall_ v P.not_)))
Tactic:
apply IsDeduct.axiom_
State after:
case h1.a.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsAxiom ((forall_ v (Q.not_.imp_ P.not_)).imp_ ((forall_ v Q.not_).imp_ (forall_ v P.not_)))

State before:
case h1.a.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsAxiom ((forall_ v (Q.not_.imp_ P.not_)).imp_ ((forall_ v Q.not_).imp_ (forall_ v P.not_)))
Tactic:
apply IsAxiom.pred_1_
State after:
no goals

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

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

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

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

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

State before:
case h1.a.a.a.h1.a.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsProof ((P.imp_ Q).imp_ (Q.not_.imp_ P.not_))
Tactic:
apply T_14_7
State after:
no goals

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

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

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

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

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

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

State before:
case h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (Q.not_.imp_ (forall_ v Q.not_))
Tactic:
apply IsDeduct.axiom_
State after:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsAxiom (Q.not_.imp_ (forall_ v Q.not_))

State before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsAxiom (Q.not_.imp_ (forall_ v Q.not_))
Tactic:
apply IsAxiom.pred_3_
State after:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v Q.not_

State before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v Q.not_
Tactic:
simp only [isFreeIn]
State after:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v Q

State before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v Q
Tactic:
exact h1
State after:
no goals