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

State before:
P : Formula
v t : VarName
h1 : fastAdmits v t P
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))
Tactic:
simp only [fastAdmits] at h1
State after:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))

State before:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))
Tactic:
simp only [def_exists_]
State after:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsProof ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_)

State before:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsProof ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_)
Tactic:
simp only [IsProof]
State after:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅ ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_)

State before:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅ ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_)
Tactic:
apply IsDeduct.mp_ ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)
State after:
case a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅
    (((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_).imp_ ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_))

case a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅ ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)

State before:
case a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅
    (((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_).imp_ ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_))
Tactic:
SC
State after:
no goals

State before:
case a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅ ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)
Tactic:
apply IsDeduct.axiom_
State after:
case a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsAxiom ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)

State before:
case a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsAxiom ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)
Tactic:
apply IsAxiom.pred_2_ v t
State after:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmits v t P.not_

case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastReplaceFree v t P.not_ = (fastReplaceFree v t P).not_

State before:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmits v t P.not_
Tactic:
simp only [fastAdmits]
State after:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmitsAux v t ∅ P.not_

State before:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmitsAux v t ∅ P.not_
Tactic:
simp only [fastAdmitsAux]
State after:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmitsAux v t ∅ P

State before:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmitsAux v t ∅ P
Tactic:
exact h1
State after:
no goals

State before:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastReplaceFree v t P.not_ = (fastReplaceFree v t P).not_
Tactic:
rfl
State after:
no goals