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

State before:
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ Q
Tactic:
refine' rule_C (fastReplaceFree v t P) Q t Δ _ h2 h5 _
State after:
case refine'_1
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (exists_ t (fastReplaceFree v t P))

case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬isFreeIn t Q

State before:
case refine'_1
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (exists_ t (fastReplaceFree v t P))
Tactic:
simp only [def_exists_] at h1
State after:
case refine'_1
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ (exists_ t (fastReplaceFree v t P))

State before:
case refine'_1
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ (exists_ t (fastReplaceFree v t P))
Tactic:
simp only [def_exists_]
State after:
case refine'_1
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ (forall_ t (fastReplaceFree v t P).not_).not_

State before:
case refine'_1
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ (forall_ t (fastReplaceFree v t P).not_).not_
Tactic:
apply IsDeduct.mp_ (forall_ v P.not_).not_
State after:
case refine'_1.a
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ ((forall_ v P.not_).not_.imp_ (forall_ t (fastReplaceFree v t P).not_).not_)

case refine'_1.a
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ (forall_ v P.not_).not_

State before:
case refine'_1.a
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ ((forall_ v P.not_).not_.imp_ (forall_ t (fastReplaceFree v t P).not_).not_)
Tactic:
apply IsDeduct.mp_ ((forall_ t (fastReplaceFree v t P.not_)).imp_ (forall_ v P.not_))
State after:
case refine'_1.a.a
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ
    (((forall_ t (fastReplaceFree v t P.not_)).imp_ (forall_ v P.not_)).imp_
      ((forall_ v P.not_).not_.imp_ (forall_ t (fastReplaceFree v t P).not_).not_))

case refine'_1.a.a
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ ((forall_ t (fastReplaceFree v t P.not_)).imp_ (forall_ v P.not_))

State before:
case refine'_1.a.a
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ
    (((forall_ t (fastReplaceFree v t P.not_)).imp_ (forall_ v P.not_)).imp_
      ((forall_ v P.not_).not_.imp_ (forall_ t (fastReplaceFree v t P).not_).not_))
Tactic:
SC
State after:
no goals

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

State before:
case refine'_1.a.a.h1
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct (Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}) (forall_ v P.not_)
Tactic:
apply univIntro P.not_ v t _ h3
State after:
case refine'_1.a.a.h1.h2
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct (Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}) (fastReplaceFree v t P.not_)

case refine'_1.a.a.h1.h3
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ∀ H ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}, ¬isFreeIn t H

State before:
case refine'_1.a.a.h1.h2
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct (Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}) (fastReplaceFree v t P.not_)
Tactic:
apply specId t
State after:
case refine'_1.a.a.h1.h2.h1
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct (Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}) (forall_ t (fastReplaceFree v t P.not_))

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

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

State before:
case refine'_1.a.a.h1.h3
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ∀ H ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}, ¬isFreeIn t H
Tactic:
intro H a1
State after:
case refine'_1.a.a.h1.h3
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
a1 : H ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}
⊢ ¬isFreeIn t H

State before:
case refine'_1.a.a.h1.h3
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
a1 : H ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}
⊢ ¬isFreeIn t H
Tactic:
simp at a1
State after:
case refine'_1.a.a.h1.h3
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
a1 : H = forall_ t (fastReplaceFree v t P.not_) ∨ H ∈ Δ
⊢ ¬isFreeIn t H

State before:
case refine'_1.a.a.h1.h3
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
a1 : H = forall_ t (fastReplaceFree v t P.not_) ∨ H ∈ Δ
⊢ ¬isFreeIn t H
Tactic:
cases a1
State after:
case refine'_1.a.a.h1.h3.inl
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
h✝ : H = forall_ t (fastReplaceFree v t P.not_)
⊢ ¬isFreeIn t H

case refine'_1.a.a.h1.h3.inr
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
h✝ : H ∈ Δ
⊢ ¬isFreeIn t H

State before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
c1 : H = forall_ t (fastReplaceFree v t P.not_)
⊢ ¬isFreeIn t H
Tactic:
case _ c1 =>
  subst c1
  simp only [isFreeIn]
  simp
State after:
no goals

State before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
c1 : H ∈ Δ
⊢ ¬isFreeIn t H
Tactic:
case _ c1 =>
  exact h5 H c1
State after:
no goals

State before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
c1 : H = forall_ t (fastReplaceFree v t P.not_)
⊢ ¬isFreeIn t H
Tactic:
subst c1
State after:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ¬isFreeIn t (forall_ t (fastReplaceFree v t P.not_))

State before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ¬isFreeIn t (forall_ t (fastReplaceFree v t P.not_))
Tactic:
simp only [isFreeIn]
State after:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ¬(¬True ∧ isFreeIn t (fastReplaceFree v t P))

State before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ¬(¬True ∧ isFreeIn t (fastReplaceFree v t P))
Tactic:
simp
State after:
no goals

State before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
c1 : H ∈ Δ
⊢ ¬isFreeIn t H
Tactic:
exact h5 H c1
State after:
no goals

State before:
case refine'_1.a
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ (forall_ v P.not_).not_
Tactic:
exact h1
State after:
no goals

State before:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬isFreeIn t Q
Tactic:
intro contra
State after:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ False

State before:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ False
Tactic:
apply h4
State after:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ occursIn t Q

State before:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ occursIn t Q
Tactic:
apply isFreeIn_imp_occursIn
State after:
case refine'_2.h1
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ isFreeIn t Q

State before:
case refine'_2.h1
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ isFreeIn t Q
Tactic:
exact contra
State after:
no goals