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

State before:
P S : Formula
⊢ IsProof ((S.imp_ P).imp_ ((S.not_.imp_ P).imp_ P))
Tactic:
simp only [IsProof]
State after:
P S : Formula
⊢ IsDeduct ∅ ((S.imp_ P).imp_ ((S.not_.imp_ P).imp_ P))

State before:
P S : Formula
⊢ IsDeduct ∅ ((S.imp_ P).imp_ ((S.not_.imp_ P).imp_ P))
Tactic:
apply deduction_theorem
State after:
case h1
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) ((S.not_.imp_ P).imp_ P)

State before:
case h1
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) ((S.not_.imp_ P).imp_ P)
Tactic:
apply IsDeduct.mp_ (P.not_.imp_ (S.not_.imp_ P).not_)
State after:
case h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))

case h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) (P.not_.imp_ (S.not_.imp_ P).not_)

State before:
case h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))
Tactic:
apply IsDeduct.axiom_
State after:
case h1.a.a
P S : Formula
⊢ IsAxiom ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))

State before:
case h1.a.a
P S : Formula
⊢ IsAxiom ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))
Tactic:
apply IsAxiom.prop_3_
State after:
no goals

State before:
case h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) (P.not_.imp_ (S.not_.imp_ P).not_)
Tactic:
apply deduction_theorem
State after:
case h1.a.h1
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.not_.imp_ P).not_

State before:
case h1.a.h1
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.not_.imp_ P).not_
Tactic:
apply IsDeduct.mp_ P.not_
State after:
case h1.a.h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (P.not_.imp_ (S.not_.imp_ P).not_)

case h1.a.h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) P.not_

State before:
case h1.a.h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (P.not_.imp_ (S.not_.imp_ P).not_)
Tactic:
apply IsDeduct.mp_ S.not_
State after:
case h1.a.h1.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.not_.imp_ (P.not_.imp_ (S.not_.imp_ P).not_))

case h1.a.h1.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) S.not_

State before:
case h1.a.h1.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.not_.imp_ (P.not_.imp_ (S.not_.imp_ P).not_))
Tactic:
apply proof_imp_deduct
State after:
case h1.a.h1.a.a.h1
P S : Formula
⊢ IsProof (S.not_.imp_ (P.not_.imp_ (S.not_.imp_ P).not_))

State before:
case h1.a.h1.a.a.h1
P S : Formula
⊢ IsProof (S.not_.imp_ (P.not_.imp_ (S.not_.imp_ P).not_))
Tactic:
apply T_14_8
State after:
no goals

State before:
case h1.a.h1.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) S.not_
Tactic:
apply IsDeduct.mp_ P.not_
State after:
case h1.a.h1.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (P.not_.imp_ S.not_)

case h1.a.h1.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) P.not_

State before:
case h1.a.h1.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (P.not_.imp_ S.not_)
Tactic:
apply IsDeduct.mp_ (S.imp_ P)
State after:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) ((S.imp_ P).imp_ (P.not_.imp_ S.not_))

case h1.a.h1.a.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.imp_ P)

State before:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) ((S.imp_ P).imp_ (P.not_.imp_ S.not_))
Tactic:
apply proof_imp_deduct
State after:
case h1.a.h1.a.a.a.a.h1
P S : Formula
⊢ IsProof ((S.imp_ P).imp_ (P.not_.imp_ S.not_))

State before:
case h1.a.h1.a.a.a.a.h1
P S : Formula
⊢ IsProof ((S.imp_ P).imp_ (P.not_.imp_ S.not_))
Tactic:
apply T_14_7
State after:
no goals

State before:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.imp_ P)
Tactic:
apply IsDeduct.assume_
State after:
case h1.a.h1.a.a.a.a.a
P S : Formula
⊢ S.imp_ P ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}

State before:
case h1.a.h1.a.a.a.a.a
P S : Formula
⊢ S.imp_ P ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}
Tactic:
simp
State after:
no goals

State before:
case h1.a.h1.a.a.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) P.not_
Tactic:
apply IsDeduct.assume_
State after:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ P.not_ ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}

State before:
case h1.a.h1.a.a.a.a
P S : Formula
⊢ P.not_ ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}
Tactic:
simp
State after:
no goals

State before:
case h1.a.h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) P.not_
Tactic:
apply IsDeduct.assume_
State after:
case h1.a.h1.a.a
P S : Formula
⊢ P.not_ ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}

State before:
case h1.a.h1.a.a
P S : Formula
⊢ P.not_ ∈ ∅ ∪ {S.imp_ P} ∪ {P.not_}
Tactic:
simp
State after:
no goals