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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
H : Formula
a1 : H = P.imp_ (forall_ v Q)
⊢ ¬isFreeIn v H
Tactic:
subst a1
State after:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ ¬isFreeIn v (P.imp_ (forall_ v Q))

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

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

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