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

State before:
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ (exists_ v P)
Tactic:
apply T_17_4 P v v Δ
State after:
case h1
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ fastAdmits v v P

case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ (fastReplaceFree v v P)

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

State before:
case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ (fastReplaceFree v v P)
Tactic:
simp only [fastReplaceFree_self]
State after:
case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ P

State before:
case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ P
Tactic:
exact h1
State after:
no goals