internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.C_18_3
Proof state before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (forall_ hd (List.foldr forall_ (U.iff_ V) tl))
Tactic:
apply generalization
Proof state after:
case h1
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)

case h2
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ ∀ H ∈ ∅, ¬isFreeIn hd H
Theorem: FOL.NV.C_18_3
Proof state before:
case h1
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
Tactic:
exact ih
Proof state after:
no goals
Theorem: FOL.NV.C_18_3
Proof state before:
case h2
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ ∀ H ∈ ∅, ¬isFreeIn hd H
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.C_18_4
Proof state before:
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ P_V
Tactic:
apply IsDeduct.mp_ P_U
Proof state after:
case a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (P_U.imp_ P_V)

case a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ P_U
Theorem: FOL.NV.C_18_4
Proof state before:
case a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (P_U.imp_ P_V)
Tactic:
apply IsDeduct.mp_ (P_U.iff_ P_V)
Proof state after:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ ((P_U.iff_ P_V).imp_ (P_U.imp_ P_V))

case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (P_U.iff_ P_V)
Theorem: FOL.NV.C_18_4
Proof state before:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ ((P_U.iff_ P_V).imp_ (P_U.imp_ P_V))
Tactic:
simp only [def_iff_]
Proof state after:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (((P_U.imp_ P_V).and_ (P_V.imp_ P_U)).imp_ (P_U.imp_ P_V))
Theorem: FOL.NV.C_18_4
Proof state before:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (((P_U.imp_ P_V).and_ (P_V.imp_ P_U)).imp_ (P_U.imp_ P_V))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (((P_U.imp_ P_V).imp_ (P_V.imp_ P_U).not_).not_.imp_ (P_U.imp_ P_V))
Theorem: FOL.NV.C_18_4
Proof state before:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (((P_U.imp_ P_V).imp_ (P_V.imp_ P_U).not_).not_.imp_ (P_U.imp_ P_V))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.C_18_4
Proof state before:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (P_U.iff_ P_V)
Tactic:
apply proof_imp_deduct
Proof state after:
case a.a.h1
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsProof (P_U.iff_ P_V)
Theorem: FOL.NV.C_18_4
Proof state before:
case a.a.h1
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsProof (P_U.iff_ P_V)
Tactic:
exact C_18_3 U V P_U P_V h1 h2
Proof state after:
no goals
Theorem: FOL.NV.C_18_4
Proof state before:
case a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ P_U
Tactic:
exact h3
Proof state after:
no goals
Theorem: FOL.NV.T_18_5
Proof state before:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P).iff_ (exists_ v P.not_).not_)
Tactic:
simp only [def_exists_]
Proof state after:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P).iff_ (forall_ v P.not_.not_).not_.not_)
Theorem: FOL.NV.T_18_5
Proof state before:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P).iff_ (forall_ v P.not_.not_).not_.not_)
Tactic:
apply C_18_4 P P.not_.not_ ((forall_ v P).iff_ (forall_ v P).not_.not_)
Proof state after:
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).iff_ (forall_ v P).not_.not_)
    ((forall_ v P).iff_ (forall_ v P.not_.not_).not_.not_)

case h2
P : Formula
v : VarName
⊢ IsProof (P.iff_ P.not_.not_)

case h3
P : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v P).iff_ (forall_ v P).not_.not_)
Theorem: FOL.NV.T_18_5
Proof state before:
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).iff_ (forall_ v P).not_.not_)
    ((forall_ v P).iff_ (forall_ v P.not_.not_).not_.not_)
Tactic:
simp only [def_iff_]
Proof state after:
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).and_ ((forall_ v P).not_.not_.imp_ (forall_ v P)))
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).and_ ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)))
Theorem: FOL.NV.T_18_5
Proof state before:
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).and_ ((forall_ v P).not_.not_.imp_ (forall_ v P)))
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).and_ ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)))
Tactic:
simp only [def_and_]
Proof state after:
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_).not_
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).imp_
        ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_).not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_).not_
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).imp_
        ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_).not_
Tactic:
apply IsReplOfFormulaInFormula.not_
Proof state after:
case h1.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_)
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).imp_
      ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_)
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_)
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).imp_
      ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_)
Tactic:
apply IsReplOfFormulaInFormula.imp_
Proof state after:
case h1.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).imp_ (forall_ v P).not_.not_)
    ((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_)

case h1.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_
    ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).imp_ (forall_ v P).not_.not_)
    ((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_)
Tactic:
apply IsReplOfFormulaInFormula.imp_
Proof state after:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P)

case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_.not_ (forall_ v P.not_.not_).not_.not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P)
Tactic:
apply IsReplOfFormulaInFormula.same_
Proof state after:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ forall_ v P = forall_ v P
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ forall_ v P = forall_ v P
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_.not_ (forall_ v P.not_.not_).not_.not_
Tactic:
apply IsReplOfFormulaInFormula.not_
Proof state after:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_ (forall_ v P.not_.not_).not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_ (forall_ v P.not_.not_).not_
Tactic:
apply IsReplOfFormulaInFormula.not_
Proof state after:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P.not_.not_)
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P.not_.not_)
Tactic:
apply IsReplOfFormulaInFormula.forall_
Proof state after:
case h1.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ P P.not_.not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ P P.not_.not_
Tactic:
apply IsReplOfFormulaInFormula.diff_
Proof state after:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P = P

case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P.not_.not_ = P.not_.not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P = P
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P.not_.not_ = P.not_.not_
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_
    ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)).not_
Tactic:
apply IsReplOfFormulaInFormula.not_
Proof state after:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).not_.not_.imp_ (forall_ v P))
    ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P))
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).not_.not_.imp_ (forall_ v P))
    ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P))
Tactic:
apply IsReplOfFormulaInFormula.imp_
Proof state after:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_.not_ (forall_ v P.not_.not_).not_.not_

case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P)
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_.not_ (forall_ v P.not_.not_).not_.not_
Tactic:
apply IsReplOfFormulaInFormula.not_
Proof state after:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_ (forall_ v P.not_.not_).not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_ (forall_ v P.not_.not_).not_
Tactic:
apply IsReplOfFormulaInFormula.not_
Proof state after:
case h1.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P.not_.not_)
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P.not_.not_)
Tactic:
apply IsReplOfFormulaInFormula.forall_
Proof state after:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ P P.not_.not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ P P.not_.not_
Tactic:
apply IsReplOfFormulaInFormula.diff_
Proof state after:
case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P = P

case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P.not_.not_ = P.not_.not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P = P
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P.not_.not_ = P.not_.not_
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P)
Tactic:
apply IsReplOfFormulaInFormula.same_
Proof state after:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ forall_ v P = forall_ v P
Theorem: FOL.NV.T_18_5
Proof state before:
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ forall_ v P = forall_ v P
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_18_5
Proof state before:
case h2
P : Formula
v : VarName
⊢ IsProof (P.iff_ P.not_.not_)
Tactic:
simp only [def_iff_]
Proof state after:
case h2
P : Formula
v : VarName
⊢ IsProof ((P.imp_ P.not_.not_).and_ (P.not_.not_.imp_ P))
Theorem: FOL.NV.T_18_5
Proof state before:
case h2
P : Formula
v : VarName
⊢ IsProof ((P.imp_ P.not_.not_).and_ (P.not_.not_.imp_ P))
Tactic:
simp only [def_and_]
Proof state after:
case h2
P : Formula
v : VarName
⊢ IsProof ((P.imp_ P.not_.not_).imp_ (P.not_.not_.imp_ P).not_).not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h2
P : Formula
v : VarName
⊢ IsProof ((P.imp_ P.not_.not_).imp_ (P.not_.not_.imp_ P).not_).not_
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_18_5
Proof state before:
case h3
P : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v P).iff_ (forall_ v P).not_.not_)
Tactic:
simp only [def_iff_]
Proof state after:
case h3
P : Formula
v : VarName
⊢ IsDeduct ∅ (((forall_ v P).imp_ (forall_ v P).not_.not_).and_ ((forall_ v P).not_.not_.imp_ (forall_ v P)))
Theorem: FOL.NV.T_18_5
Proof state before:
case h3
P : Formula
v : VarName
⊢ IsDeduct ∅ (((forall_ v P).imp_ (forall_ v P).not_.not_).and_ ((forall_ v P).not_.not_.imp_ (forall_ v P)))
Tactic:
simp only [def_and_]
Proof state after:
case h3
P : Formula
v : VarName
⊢ IsDeduct ∅ (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_).not_
Theorem: FOL.NV.T_18_5
Proof state before:
case h3
P : Formula
v : VarName
⊢ IsDeduct ∅ (((forall_ v P).imp_ (forall_ v P).not_.not_).imp_ ((forall_ v P).not_.not_.imp_ (forall_ v P)).not_).not_
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_18_6
Proof 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
Proof 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))
Theorem: FOL.NV.T_18_6
Proof 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
Proof 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))
Theorem: FOL.NV.T_18_6
Proof 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
Proof 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))
Theorem: FOL.NV.T_18_6
Proof 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
Proof 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))
Theorem: FOL.NV.T_18_6
Proof 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
Proof 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))
Theorem: FOL.NV.T_18_6
Proof 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
Proof 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))
Theorem: FOL.NV.T_18_6
Proof 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))
Proof 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))
Theorem: FOL.NV.T_18_6
Proof 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))
Proof 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))
Theorem: FOL.NV.T_18_6
Proof 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_]
Proof 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)))))
Theorem: FOL.NV.T_18_6
Proof 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_]
Proof 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_))