internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v = x ∨ v = y → u ∉ binders
⊢ IsSub (eq_ x y) v u (eq_ (if v = x then u else x) (if v = y then u else y))
Tactic:
apply IsSub.eq_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub false_ v u false_
Tactic:
first | apply IsSub.true_ | apply IsSub.false_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub true_ v u true_
Tactic:
apply IsSub.true_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub false_ v u false_
Tactic:
apply IsSub.false_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : 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 phi
⊢ IsSub phi.not_ v u (Rec.fastReplaceFree v u phi).not_
Tactic:
apply IsSub.not_
Proof state after:
case a
v u : 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 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 a
v u : 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 phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
exact phi_ih binders h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders phi ∧ Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.iff_ psi) v u ((Rec.fastReplaceFree v u phi).iff_ (Rec.fastReplaceFree v u psi))
Tactic:
cases h1
Proof state after:
case intro
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
left✝ : Rec.fastAdmitsAux v u binders phi
right✝ : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.iff_ psi) v u ((Rec.fastReplaceFree v u phi).iff_ (Rec.fastReplaceFree v u psi))
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.iff_ psi) v u ((Rec.fastReplaceFree v u phi).iff_ (Rec.fastReplaceFree v u psi))
Tactic:
first | apply IsSub.imp_ | apply IsSub.and_ | apply IsSub.or_ | apply IsSub.iff_
Proof state after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.imp_ psi) v u ((Rec.fastReplaceFree v u phi).imp_ (Rec.fastReplaceFree v u psi))
Tactic:
apply IsSub.imp_
Proof state after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.and_ psi) v u ((Rec.fastReplaceFree v u phi).and_ (Rec.fastReplaceFree v u psi))
Tactic:
apply IsSub.and_
Proof state after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.or_ psi) v u ((Rec.fastReplaceFree v u phi).or_ (Rec.fastReplaceFree v u psi))
Tactic:
apply IsSub.or_
Proof state after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.iff_ psi) v u ((Rec.fastReplaceFree v u phi).iff_ (Rec.fastReplaceFree v u psi))
Tactic:
apply IsSub.iff_
Proof state after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
exact phi_ih binders h1_left
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)
Tactic:
exact psi_ih binders h1_right
Proof state after:
no goals
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 : v = x ∨ Rec.fastAdmitsAux v u (binders ∪ {x}) phi
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
cases h1
Proof state after:
case inl
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
h✝ : v = x
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))

case inr
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
h✝ : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
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 : v = x
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
case inl h1 =>
  split_ifs
  case pos c1 | neg c1 =>
    first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
    subst h1
    simp only [isFreeIn]
    simp
Proof state after:
no goals
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 : v = x
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
split_ifs
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 h✝ : v = x
⊢ IsSub (exists_ x phi) v u (exists_ x 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 : v = x
h✝ : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
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 : v = x
c1 : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
case pos c1 | neg c1 =>
  first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
  subst h1
  simp only [isFreeIn]
  simp
Proof state after:
no goals
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 : v = x
c1 : ¬v = x
⊢ 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 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 : v = x
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case 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 : v = x
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
subst h1
Proof state after:
case a
v u : 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
c1 : ¬v = v
⊢ ¬isFreeIn v (exists_ v phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case a
v u : 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
c1 : ¬v = v
⊢ ¬isFreeIn v (exists_ v phi)
Tactic:
simp only [isFreeIn]
Proof state after:
case a
v u : 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
c1 : ¬v = v
⊢ ¬(¬True ∧ isFreeIn v phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case a
v u : 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
c1 : ¬v = v
⊢ ¬(¬True ∧ isFreeIn v phi)
Tactic:
simp
Proof state after:
no goals
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 : v = x
c1 : ¬v = x
⊢ IsSub (forall_ x phi) v u (forall_ x phi)
Tactic:
apply IsSub.forall_not_free_in
Proof state after:
case 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 : v = x
c1 : ¬v = x
⊢ ¬isFreeIn v (forall_ x phi)
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 : v = x
c1 : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
apply IsSub.exists_not_free_in
Proof state after:
case 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 : v = x
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x phi)
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
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
split_ifs
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
h✝ : v = x
⊢ IsSub (exists_ x phi) v u (exists_ x 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
h✝ : ¬v = x
⊢ 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:
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 phi)
Tactic:
case pos c1 =>
  first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
  simp only [isFreeIn]
  tauto
Proof state after:
no goals
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 phi)
Tactic:
first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
Proof state after:
case 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
⊢ ¬isFreeIn v (exists_ x phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case 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
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
simp only [isFreeIn]
Proof state after:
case 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
⊢ ¬(¬v = x ∧ isFreeIn v phi)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case 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
⊢ ¬(¬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:
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 (forall_ x phi) v u (forall_ x phi)
Tactic:
apply IsSub.forall_not_free_in
Proof state after:
case 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
⊢ ¬isFreeIn v (forall_ x phi)
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 phi)
Tactic:
apply IsSub.exists_not_free_in
Proof state after:
case 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
⊢ ¬isFreeIn v (exists_ x phi)