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

State before:
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ v P)
Tactic:
rw [← fastReplaceFree_inverse P v t h1]
State after:
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))

State before:
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
Tactic:
apply IsDeduct.mp_ (forall_ t (fastReplaceFree v t P))
State after:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))

case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ t (fastReplaceFree v t P))

State before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))
Tactic:
apply proof_imp_deduct
State after:
case a.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsProof ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))

State before:
case a.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsProof ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))
Tactic:
apply deduction_theorem
State after:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct (∅ ∪ {forall_ t (fastReplaceFree v t P)}) (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))

State before:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct (∅ ∪ {forall_ t (fastReplaceFree v t P)}) (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
Tactic:
simp
State after:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))

State before:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
Tactic:
apply generalization
State after:
case a.h1.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (fastReplaceFree t v (fastReplaceFree v t P))

case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ∀ H ∈ {forall_ t (fastReplaceFree v t P)}, ¬isFreeIn v H

State before:
case a.h1.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (fastReplaceFree t v (fastReplaceFree v t P))
Tactic:
apply spec
State after:
case a.h1.h1.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (forall_ t (fastReplaceFree v t P))

case a.h1.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ fastAdmits t v (fastReplaceFree v t P)

State before:
case a.h1.h1.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct {forall_ t (fastReplaceFree v t P)} (forall_ t (fastReplaceFree v t P))
Tactic:
apply IsDeduct.assume_
State after:
case a.h1.h1.h1.h1.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ forall_ t (fastReplaceFree v t P) ∈ {forall_ t (fastReplaceFree v t P)}

State before:
case a.h1.h1.h1.h1.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ forall_ t (fastReplaceFree v t P) ∈ {forall_ t (fastReplaceFree v t P)}
Tactic:
simp
State after:
no goals

State before:
case a.h1.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ fastAdmits t v (fastReplaceFree v t P)
Tactic:
apply fastReplaceFree_fastAdmits
State after:
case a.h1.h1.h1.h2.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬occursIn t P

State before:
case a.h1.h1.h1.h2.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬occursIn t P
Tactic:
exact h1
State after:
no goals

State before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ∀ H ∈ {forall_ t (fastReplaceFree v t P)}, ¬isFreeIn v H
Tactic:
simp
State after:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬isFreeIn v (forall_ t (fastReplaceFree v t P))

State before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬isFreeIn v (forall_ t (fastReplaceFree v t P))
Tactic:
simp only [isFreeIn]
State after:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬(¬v = t ∧ isFreeIn v (fastReplaceFree v t P))

State before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬(¬v = t ∧ isFreeIn v (fastReplaceFree v t P))
Tactic:
simp
State after:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬v = t → ¬isFreeIn v (fastReplaceFree v t P)

State before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬v = t → ¬isFreeIn v (fastReplaceFree v t P)
Tactic:
intro a1 contra
State after:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
a1 : ¬v = t
contra : isFreeIn v (fastReplaceFree v t P)
⊢ False

State before:
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
a1 : ¬v = t
contra : isFreeIn v (fastReplaceFree v t P)
⊢ False
Tactic:
exact not_isFreeIn_fastReplaceFree P v t a1 contra
State after:
no goals

State before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ t (fastReplaceFree v t P))
Tactic:
exact generalization (fastReplaceFree v t P) t Δ h2 h3
State after:
no goals