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

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

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

State before:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v (P.and_ Q)} ((exists_ v P).and_ (exists_ v Q))
Tactic:
apply rule_C (P.and_ Q) ((exists_ v P).and_ (exists_ v Q)) v
State after:
case h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v (P.and_ Q)} (exists_ v (P.and_ Q))

case h1.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) ((exists_ v P).and_ (exists_ v Q))

case h1.h3
P Q : Formula
v : VarName
⊢ ∀ H ∈ {exists_ v (P.and_ Q)}, ¬isFreeIn v H

case h1.h4
P Q : Formula
v : VarName
⊢ ¬isFreeIn v ((exists_ v P).and_ (exists_ v Q))

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

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

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

case h1.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (exists_ v Q)

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

case h1.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (exists_ v P)

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

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

State before:
case h1.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (exists_ v P)
Tactic:
apply exists_intro P v v
State after:
case h1.h2.a.a.h1
P Q : Formula
v : VarName
⊢ fastAdmits v v P

case h1.h2.a.a.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (fastReplaceFree v v P)

State before:
case h1.h2.a.a.h1
P Q : Formula
v : VarName
⊢ fastAdmits v v P
Tactic:
apply fastAdmits_self
State after:
no goals

State before:
case h1.h2.a.a.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (fastReplaceFree v v P)
Tactic:
simp only [fastReplaceFree_self]
State after:
case h1.h2.a.a.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) P

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

case h1.h2.a.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (P.and_ Q)

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

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

State before:
case h1.h2.a.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (P.and_ Q)
Tactic:
apply IsDeduct.assume_
State after:
case h1.h2.a.a.h2.a.a
P Q : Formula
v : VarName
⊢ P.and_ Q ∈ {exists_ v (P.and_ Q)} ∪ {P.and_ Q}

State before:
case h1.h2.a.a.h2.a.a
P Q : Formula
v : VarName
⊢ P.and_ Q ∈ {exists_ v (P.and_ Q)} ∪ {P.and_ Q}
Tactic:
simp
State after:
no goals

State before:
case h1.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (exists_ v Q)
Tactic:
apply exists_intro Q v v
State after:
case h1.h2.a.h1
P Q : Formula
v : VarName
⊢ fastAdmits v v Q

case h1.h2.a.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (fastReplaceFree v v Q)

State before:
case h1.h2.a.h1
P Q : Formula
v : VarName
⊢ fastAdmits v v Q
Tactic:
apply fastAdmits_self
State after:
no goals

State before:
case h1.h2.a.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (fastReplaceFree v v Q)
Tactic:
simp only [fastReplaceFree_self]
State after:
case h1.h2.a.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) Q

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

case h1.h2.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (P.and_ Q)

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

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

State before:
case h1.h2.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (P.and_ Q)
Tactic:
apply IsDeduct.assume_
State after:
case h1.h2.a.h2.a.a
P Q : Formula
v : VarName
⊢ P.and_ Q ∈ {exists_ v (P.and_ Q)} ∪ {P.and_ Q}

State before:
case h1.h2.a.h2.a.a
P Q : Formula
v : VarName
⊢ P.and_ Q ∈ {exists_ v (P.and_ Q)} ∪ {P.and_ Q}
Tactic:
simp
State after:
no goals

State before:
case h1.h3
P Q : Formula
v : VarName
⊢ ∀ H ∈ {exists_ v (P.and_ Q)}, ¬isFreeIn v H
Tactic:
simp only [def_and_]
State after:
case h1.h3
P Q : Formula
v : VarName
⊢ ∀ H ∈ {exists_ v (P.imp_ Q.not_).not_}, ¬isFreeIn v H

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

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

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

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

State before:
case h1.h4
P Q : Formula
v : VarName
⊢ ¬isFreeIn v ((exists_ v P).and_ (exists_ v Q))
Tactic:
simp only [def_and_]
State after:
case h1.h4
P Q : Formula
v : VarName
⊢ ¬isFreeIn v ((exists_ v P).imp_ (exists_ v Q).not_).not_

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

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

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