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

State before:
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))
Tactic:
simp only [Similar] at h1
State after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))

State before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))
Tactic:
cases h1
State after:
case intro
P_u P_v : Formula
u v : VarName
left✝ : ¬isFreeIn v P_u
right✝ :
  ¬isFreeIn u P_v ∧
    fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))

State before:
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right :
  ¬isFreeIn u P_v ∧
    fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))
Tactic:
cases h1_right
State after:
case intro
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
left✝ : ¬isFreeIn u P_v
right✝ : fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))

State before:
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right : fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))
Tactic:
cases h1_right_right
State after:
case intro
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
left✝ : fastAdmits u v P_u
right✝ : fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))

State before:
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right : fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))
Tactic:
cases h1_right_right_right
State after:
case intro
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
left✝ : fastAdmits v u P_v
right✝ : P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))

State before:
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right : P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))
Tactic:
cases h1_right_right_right_right
State after:
case intro
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
left✝ : P_v = fastReplaceFree u v P_u
right✝ : P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))

State before:
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))
Tactic:
apply IsDeduct.mp_ ((forall_ v P_v).imp_ (forall_ u P_u))
State after:
case a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ (((forall_ v P_v).imp_ (forall_ u P_u)).imp_ ((forall_ u P_u).iff_ (forall_ v P_v)))

case a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ ((forall_ v P_v).imp_ (forall_ u P_u))

State before:
case a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ (((forall_ v P_v).imp_ (forall_ u P_u)).imp_ ((forall_ u P_u).iff_ (forall_ v P_v)))
Tactic:
apply IsDeduct.mp_ ((forall_ u P_u).imp_ (forall_ v P_v))
State after:
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅
    (((forall_ u P_u).imp_ (forall_ v P_v)).imp_
      (((forall_ v P_v).imp_ (forall_ u P_u)).imp_ ((forall_ u P_u).iff_ (forall_ v P_v))))

case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ ((forall_ u P_u).imp_ (forall_ v P_v))

State before:
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅
    (((forall_ u P_u).imp_ (forall_ v P_v)).imp_
      (((forall_ v P_v).imp_ (forall_ u P_u)).imp_ ((forall_ u P_u).iff_ (forall_ v P_v))))
Tactic:
simp only [def_iff_]
State after:
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅
    (((forall_ u P_u).imp_ (forall_ v P_v)).imp_
      (((forall_ v P_v).imp_ (forall_ u P_u)).imp_
        (((forall_ u P_u).imp_ (forall_ v P_v)).and_ ((forall_ v P_v).imp_ (forall_ u P_u)))))

State before:
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅
    (((forall_ u P_u).imp_ (forall_ v P_v)).imp_
      (((forall_ v P_v).imp_ (forall_ u P_u)).imp_
        (((forall_ u P_u).imp_ (forall_ v P_v)).and_ ((forall_ v P_v).imp_ (forall_ u P_u)))))
Tactic:
simp only [def_and_]
State after:
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅
    (((forall_ u P_u).imp_ (forall_ v P_v)).imp_
      (((forall_ v P_v).imp_ (forall_ u P_u)).imp_
        (((forall_ u P_u).imp_ (forall_ v P_v)).imp_ ((forall_ v P_v).imp_ (forall_ u P_u)).not_).not_))

State before:
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅
    (((forall_ u P_u).imp_ (forall_ v P_v)).imp_
      (((forall_ v P_v).imp_ (forall_ u P_u)).imp_
        (((forall_ u P_u).imp_ (forall_ v P_v)).imp_ ((forall_ v P_v).imp_ (forall_ u P_u)).not_).not_))
Tactic:
SC
State after:
no goals

State before:
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ ((forall_ u P_u).imp_ (forall_ v P_v))
Tactic:
apply deduction_theorem
State after:
case a.a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct (∅ ∪ {forall_ u P_u}) (forall_ v P_v)

State before:
case a.a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct (∅ ∪ {forall_ u P_u}) (forall_ v P_v)
Tactic:
simp
State after:
case a.a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ u P_u} (forall_ v P_v)

State before:
case a.a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ u P_u} (forall_ v P_v)
Tactic:
apply generalization
State after:
case a.a.h1.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ u P_u} P_v

case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ∀ H ∈ {forall_ u P_u}, ¬isFreeIn v H

State before:
case a.a.h1.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ u P_u} P_v
Tactic:
subst h1_right_right_right_right_left
State after:
case a.a.h1.h1
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ IsDeduct {forall_ u P_u} (fastReplaceFree u v P_u)

State before:
case a.a.h1.h1
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ IsDeduct {forall_ u P_u} (fastReplaceFree u v P_u)
Tactic:
apply spec
State after:
case a.a.h1.h1.h1
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ IsDeduct {forall_ u P_u} (forall_ u P_u)

case a.a.h1.h1.h2
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ fastAdmits u v P_u

State before:
case a.a.h1.h1.h1
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ IsDeduct {forall_ u P_u} (forall_ u P_u)
Tactic:
apply IsDeduct.assume_
State after:
case a.a.h1.h1.h1.a
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ forall_ u P_u ∈ {forall_ u P_u}

State before:
case a.a.h1.h1.h1.a
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ forall_ u P_u ∈ {forall_ u P_u}
Tactic:
simp
State after:
no goals

State before:
case a.a.h1.h1.h2
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ fastAdmits u v P_u
Tactic:
exact h1_right_right_left
State after:
no goals

State before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ∀ H ∈ {forall_ u P_u}, ¬isFreeIn v H
Tactic:
intro H a1
State after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H ∈ {forall_ u P_u}
⊢ ¬isFreeIn v H

State before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H ∈ {forall_ u P_u}
⊢ ¬isFreeIn v H
Tactic:
simp at a1
State after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H = forall_ u P_u
⊢ ¬isFreeIn v H

State before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H = forall_ u P_u
⊢ ¬isFreeIn v H
Tactic:
subst a1
State after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v (forall_ u P_u)

State before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v (forall_ u P_u)
Tactic:
simp only [isFreeIn]
State after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬(¬v = u ∧ isFreeIn v P_u)

State before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬(¬v = u ∧ isFreeIn v P_u)
Tactic:
simp
State after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬v = u → ¬isFreeIn v P_u

State before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬v = u → ¬isFreeIn v P_u
Tactic:
intro _
State after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
a✝ : ¬v = u
⊢ ¬isFreeIn v P_u

State before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
a✝ : ¬v = u
⊢ ¬isFreeIn v P_u
Tactic:
exact h1_left
State after:
no goals

State before:
case a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ ((forall_ v P_v).imp_ (forall_ u P_u))
Tactic:
apply deduction_theorem
State after:
case a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct (∅ ∪ {forall_ v P_v}) (forall_ u P_u)

State before:
case a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct (∅ ∪ {forall_ v P_v}) (forall_ u P_u)
Tactic:
simp
State after:
case a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ v P_v} (forall_ u P_u)

State before:
case a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ v P_v} (forall_ u P_u)
Tactic:
apply generalization
State after:
case a.h1.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ v P_v} P_u

case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ∀ H ∈ {forall_ v P_v}, ¬isFreeIn u H

State before:
case a.h1.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ v P_v} P_u
Tactic:
subst h1_right_right_right_right_right
State after:
case a.h1.h1
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ IsDeduct {forall_ v P_v} (fastReplaceFree v u P_v)

State before:
case a.h1.h1
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ IsDeduct {forall_ v P_v} (fastReplaceFree v u P_v)
Tactic:
apply spec
State after:
case a.h1.h1.h1
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ IsDeduct {forall_ v P_v} (forall_ v P_v)

case a.h1.h1.h2
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ fastAdmits v u P_v

State before:
case a.h1.h1.h1
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ IsDeduct {forall_ v P_v} (forall_ v P_v)
Tactic:
apply IsDeduct.assume_
State after:
case a.h1.h1.h1.a
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ forall_ v P_v ∈ {forall_ v P_v}

State before:
case a.h1.h1.h1.a
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ forall_ v P_v ∈ {forall_ v P_v}
Tactic:
simp
State after:
no goals

State before:
case a.h1.h1.h2
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ fastAdmits v u P_v
Tactic:
exact h1_right_right_right_left
State after:
no goals

State before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ∀ H ∈ {forall_ v P_v}, ¬isFreeIn u H
Tactic:
intro H a1
State after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H ∈ {forall_ v P_v}
⊢ ¬isFreeIn u H

State before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H ∈ {forall_ v P_v}
⊢ ¬isFreeIn u H
Tactic:
simp at a1
State after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H = forall_ v P_v
⊢ ¬isFreeIn u H

State before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H = forall_ v P_v
⊢ ¬isFreeIn u H
Tactic:
subst a1
State after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn u (forall_ v P_v)

State before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn u (forall_ v P_v)
Tactic:
simp only [isFreeIn]
State after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬(¬u = v ∧ isFreeIn u P_v)

State before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬(¬u = v ∧ isFreeIn u P_v)
Tactic:
simp
State after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬u = v → ¬isFreeIn u P_v

State before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬u = v → ¬isFreeIn u P_v
Tactic:
intro _
State after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
a✝ : ¬u = v
⊢ ¬isFreeIn u P_v

State before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
a✝ : ¬u = v
⊢ ¬isFreeIn u P_v
Tactic:
exact h1_right_left
State after:
no goals