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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (forall_ u (forall_ v P))
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