internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
by_cases c2 : isFreeIn v phi
Proof state after:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
first | apply IsSub.forall_free_in | apply IsSub.exists_free_in
Proof state after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v (exists_ x phi)

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v (exists_ x phi)

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
simp only [isFreeIn]
Proof state after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬v = x ∧ isFreeIn v phi

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬v = x ∧ isFreeIn v phi

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
constructor
Proof state after:
case pos.a.left
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬v = x

case pos.a.right
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v phi

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a.right
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v phi

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
. exact c2
Proof state after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
. have s1 : ¬ u ∈ binders ∪ {x}
  exact Rec.fastAdmitsAux_isFreeIn phi v u (binders ∪ {x}) h1 c2
  simp at s1
  tauto
Proof state after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub (forall_ x phi) v u (forall_ x (Rec.fastReplaceFree v u phi))
Tactic:
apply IsSub.forall_free_in
Proof state after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v (forall_ x phi)

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
apply IsSub.exists_free_in
Proof state after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v (exists_ x phi)

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a.left
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬v = x
Tactic:
exact c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a.right
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v phi
Tactic:
exact c2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u
Tactic:
have s1 : ¬ u ∈ binders ∪ {x}
Proof state after:
case s1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ u ∉ binders ∪ {x}

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∪ {x}
⊢ ¬x = u
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case s1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ u ∉ binders ∪ {x}

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∪ {x}
⊢ ¬x = u
Tactic:
exact Rec.fastAdmitsAux_isFreeIn phi v u (binders ∪ {x}) h1 c2
Proof state after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∪ {x}
⊢ ¬x = u
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∪ {x}
⊢ ¬x = u
Tactic:
simp at s1
Proof state after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∧ ¬u = x
⊢ ¬x = u
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∧ ¬u = x
⊢ ¬x = u
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
exact phi_ih (binders ∪ {x}) h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
have s1 : Rec.fastReplaceFree v u phi = phi
Proof state after:
case s1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
⊢ Rec.fastReplaceFree v u phi = phi

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case s1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
⊢ Rec.fastReplaceFree v u phi = phi

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
exact Rec.not_free_in_fastReplaceFree_self phi v u c2
Proof state after:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
simp only [s1]
Proof state after:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
Proof state after:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬isFreeIn v (exists_ x phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
simp only [isFreeIn]
Proof state after:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬(¬v = x ∧ isFreeIn v phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬(¬v = x ∧ isFreeIn v phi)
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (forall_ x phi) v u (forall_ x phi)
Tactic:
apply IsSub.forall_not_free_in
Proof state after:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬isFreeIn v (forall_ x phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
apply IsSub.exists_not_free_in
Proof state after:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬isFreeIn v (exists_ x phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (def_ X xs) v u (def_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
apply IsSub.def_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastAdmitsAux
Proof state before:
F : Formula
v u : VarName
binders : Finset VarName
h1 : ∃ F', IsSub F v u F'
h2 : u ∉ binders
⊢ Rec.fastAdmitsAux v u binders F
Tactic:
apply Exists.elim h1
Proof state after:
F : Formula
v u : VarName
binders : Finset VarName
h1 : ∃ F', IsSub F v u F'
h2 : u ∉ binders
⊢ ∀ (a : Formula), IsSub F v u a → Rec.fastAdmitsAux v u binders F