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

State before:
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ P
Tactic:
apply IsDeduct.mp_ (forall_ v P)
State after:
case a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ ((forall_ v P).imp_ P)

case a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ (forall_ v P)

State before:
case a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ ((forall_ v P).imp_ P)
Tactic:
apply IsDeduct.axiom_
State after:
case a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsAxiom ((forall_ v P).imp_ P)

State before:
case a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsAxiom ((forall_ v P).imp_ P)
Tactic:
apply IsAxiom.pred_2_ v v P
State after:
case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastAdmits v v P

case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastReplaceFree v v P = P

State before:
case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastAdmits v v P
Tactic:
exact fastAdmits_self P v
State after:
no goals

State before:
case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastReplaceFree v v P = P
Tactic:
exact fastReplaceFree_self P v
State after:
no goals

State before:
case a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ (forall_ v P)
Tactic:
exact h1
State after:
no goals