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

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

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

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

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

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

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

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

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

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

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

case h1.h1.h2.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (fastReplaceFree v v Q)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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