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

State before:
P : Formula
u v : VarName
⊢ IsProof ((exists_ u (forall_ v P)).imp_ (forall_ v (exists_ u P)))
Tactic:
apply deduction_theorem
State after:
case h1
P : Formula
u v : VarName
⊢ IsDeduct (∅ ∪ {exists_ u (forall_ v P)}) (forall_ v (exists_ u P))

State before:
case h1
P : Formula
u v : VarName
⊢ IsDeduct (∅ ∪ {exists_ u (forall_ v P)}) (forall_ v (exists_ u P))
Tactic:
simp
State after:
case h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (forall_ v (exists_ u P))

State before:
case h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (forall_ v (exists_ u P))
Tactic:
apply generalization
State after:
case h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (exists_ u P)

case h1.h2
P : Formula
u v : VarName
⊢ ∀ H ∈ {exists_ u (forall_ v P)}, ¬isFreeIn v H

State before:
case h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (exists_ u P)
Tactic:
apply rule_C (forall_ v P) (exists_ u P) u {exists_ u (forall_ v P)}
State after:
case h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (exists_ u (forall_ v P))

case h1.h1.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (exists_ u P)

case h1.h1.h3
P : Formula
u v : VarName
⊢ ∀ H ∈ {exists_ u (forall_ v P)}, ¬isFreeIn u H

case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬isFreeIn u (exists_ u P)

State before:
case h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (exists_ u (forall_ v P))
Tactic:
apply IsDeduct.assume_
State after:
case h1.h1.h1.a
P : Formula
u v : VarName
⊢ exists_ u (forall_ v P) ∈ {exists_ u (forall_ v P)}

State before:
case h1.h1.h1.a
P : Formula
u v : VarName
⊢ exists_ u (forall_ v P) ∈ {exists_ u (forall_ v P)}
Tactic:
simp
State after:
no goals

State before:
case h1.h1.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (exists_ u P)
Tactic:
apply exists_intro P u u
State after:
case h1.h1.h2.h1
P : Formula
u v : VarName
⊢ fastAdmits u u P

case h1.h1.h2.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (fastReplaceFree u u P)

State before:
case h1.h1.h2.h1
P : Formula
u v : VarName
⊢ fastAdmits u u P
Tactic:
apply fastAdmits_self
State after:
no goals

State before:
case h1.h1.h2.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (fastReplaceFree u u P)
Tactic:
simp only [fastReplaceFree_self]
State after:
case h1.h1.h2.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) P

State before:
case h1.h1.h2.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) P
Tactic:
apply specId v
State after:
case h1.h1.h2.h2.h1
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (forall_ v P)

State before:
case h1.h1.h2.h2.h1
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (forall_ v P)
Tactic:
apply IsDeduct.assume_
State after:
case h1.h1.h2.h2.h1.a
P : Formula
u v : VarName
⊢ forall_ v P ∈ {exists_ u (forall_ v P)} ∪ {forall_ v P}

State before:
case h1.h1.h2.h2.h1.a
P : Formula
u v : VarName
⊢ forall_ v P ∈ {exists_ u (forall_ v P)} ∪ {forall_ v P}
Tactic:
simp
State after:
no goals

State before:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ∀ H ∈ {exists_ u (forall_ v P)}, ¬isFreeIn u H
Tactic:
simp
State after:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬isFreeIn u (exists_ u (forall_ v P))

State before:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬isFreeIn u (exists_ u (forall_ v P))
Tactic:
simp only [def_exists_]
State after:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u (forall_ v P).not_).not_

State before:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u (forall_ v P).not_).not_
Tactic:
simp only [isFreeIn]
State after:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬(¬True ∧ ¬u = v ∧ isFreeIn u P)

State before:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬(¬True ∧ ¬u = v ∧ isFreeIn u P)
Tactic:
simp
State after:
no goals

State before:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬isFreeIn u (exists_ u P)
Tactic:
simp only [def_exists_]
State after:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u P.not_).not_

State before:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u P.not_).not_
Tactic:
simp only [isFreeIn]
State after:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬(¬True ∧ isFreeIn u P)

State before:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬(¬True ∧ isFreeIn u P)
Tactic:
simp
State after:
no goals

State before:
case h1.h2
P : Formula
u v : VarName
⊢ ∀ H ∈ {exists_ u (forall_ v P)}, ¬isFreeIn v H
Tactic:
simp
State after:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (exists_ u (forall_ v P))

State before:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (exists_ u (forall_ v P))
Tactic:
simp only [def_exists_]
State after:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (forall_ u (forall_ v P).not_).not_

State before:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (forall_ u (forall_ v P).not_).not_
Tactic:
simp only [isFreeIn]
State after:
case h1.h2
P : Formula
u v : VarName
⊢ ¬(¬v = u ∧ ¬True ∧ isFreeIn v P)

State before:
case h1.h2
P : Formula
u v : VarName
⊢ ¬(¬v = u ∧ ¬True ∧ isFreeIn v P)
Tactic:
simp
State after:
no goals