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

State before:
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q).imp_ (forall_ v P)))
Tactic:
simp only [def_iff_]
State after:
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v Q).imp_ (forall_ v P)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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