internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_imp_fastAdmitsAux
Proof state before:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ a✝
⊢ v ∈ a✝ → u ∉ binders

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ a✝
⊢ v ∈ a✝ → u ∉ binders

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : ¬(v = a✝¹ ∨ v = a✝)
⊢ v = a✝¹ ∨ v = a✝ → u ∉ binders

case not_
v u : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝ → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬isFreeIn v a✝
⊢ fastAdmitsAux v u binders a✝

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝¹ → fastAdmitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝ → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(isFreeIn v a✝¹ ∨ isFreeIn v a✝)
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case and_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝¹ → fastAdmitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝ → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(isFreeIn v a✝¹ ∨ isFreeIn v a✝)
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case or_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝¹ → fastAdmitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝ → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(isFreeIn v a✝¹ ∨ isFreeIn v a✝)
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case iff_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝¹ → fastAdmitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝ → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(isFreeIn v a✝¹ ∨ isFreeIn v a✝)
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case forall_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝ → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(¬v = a✝¹ ∧ isFreeIn v a✝)
⊢ v = a✝¹ ∨ fastAdmitsAux v u (binders ∪ {a✝¹}) a✝

case exists_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬isFreeIn v a✝ → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(¬v = a✝¹ ∧ isFreeIn v a✝)
⊢ v = a✝¹ ∨ fastAdmitsAux v u (binders ∪ {a✝¹}) a✝

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ a✝
⊢ v ∈ a✝ → u ∉ binders
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬isFreeIn v (def_ a✝¹ a✝)
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Tactic:
simp only [isFreeIn] at h1
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ a✝
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ a✝
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Tactic:
simp only [fastAdmitsAux]
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ a✝
⊢ v ∈ a✝ → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ a✝
⊢ v ∈ a✝ → u ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_imp_fastAdmits
Proof state before:
F : Formula
v u : VarName
h1 : ¬isFreeIn v F
⊢ fastAdmits v u F
Tactic:
simp only [fastAdmits]
Proof state after:
F : Formula
v u : VarName
h1 : ¬isFreeIn v F
⊢ fastAdmitsAux v u ∅ F
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_imp_fastAdmits
Proof state before:
F : Formula
v u : VarName
h1 : ¬isFreeIn v F
⊢ fastAdmitsAux v u ∅ F
Tactic:
exact not_isFreeIn_imp_fastAdmitsAux F v u ∅ h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ v ∈ a✝ → u ∉ binders

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ v ∈ a✝ → u ∉ binders

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ v = a✝¹ ∨ v = a✝ → u ∉ binders

case not_
v u : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬isBoundIn u a✝ → u ∉ binders → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬isBoundIn u a✝
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders a✝

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬isBoundIn u a✝¹ → u ∉ binders → fastAdmitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), ¬isBoundIn u a✝ → u ∉ binders → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(isBoundIn u a✝¹ ∨ isBoundIn u a✝)
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case and_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬isBoundIn u a✝¹ → u ∉ binders → fastAdmitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), ¬isBoundIn u a✝ → u ∉ binders → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(isBoundIn u a✝¹ ∨ isBoundIn u a✝)
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case or_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬isBoundIn u a✝¹ → u ∉ binders → fastAdmitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), ¬isBoundIn u a✝ → u ∉ binders → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(isBoundIn u a✝¹ ∨ isBoundIn u a✝)
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case iff_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬isBoundIn u a✝¹ → u ∉ binders → fastAdmitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), ¬isBoundIn u a✝ → u ∉ binders → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : ¬(isBoundIn u a✝¹ ∨ isBoundIn u a✝)
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ v ∈ a✝ → u ∉ binders
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬isBoundIn u (def_ a✝¹ a✝)
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Tactic:
simp only [isBoundIn] at h1
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Tactic:
simp only [fastAdmitsAux]
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ v ∈ a✝ → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : ¬(u = x ∨ isBoundIn u phi)
h2 : u ∉ binders
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
push_neg at h1
Proof state after:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1 : u ≠ x ∧ ¬isBoundIn u phi
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1 : u ≠ x ∧ ¬isBoundIn u phi
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
cases h1
Proof state after:
case intro
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
left✝ : u ≠ x
right✝ : ¬isBoundIn u phi
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1_left : u ≠ x
h1_right : ¬isBoundIn u phi
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
right
Proof state after:
case h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1_left : u ≠ x
h1_right : ¬isBoundIn u phi
⊢ fastAdmitsAux v u (binders ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
case h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1_left : u ≠ x
h1_right : ¬isBoundIn u phi
⊢ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
apply phi_ih (binders ∪ {x}) h1_right
Proof state after:
case h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1_left : u ≠ x
h1_right : ¬isBoundIn u phi
⊢ u ∉ binders ∪ {x}
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
case h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1_left : u ≠ x
h1_right : ¬isBoundIn u phi
⊢ u ∉ binders ∪ {x}
Tactic:
simp
Proof state after:
case h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1_left : u ≠ x
h1_right : ¬isBoundIn u phi
⊢ u ∉ binders ∧ ¬u = x
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
case h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1_left : u ≠ x
h1_right : ¬isBoundIn u phi
⊢ u ∉ binders ∧ ¬u = x
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ v ∈ a✝ → u ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmits
Proof state before:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ fastAdmits v u F
Tactic:
simp only [fastAdmits]
Proof state after:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ fastAdmitsAux v u ∅ F
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmits
Proof state before:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ fastAdmitsAux v u ∅ F
Tactic:
apply not_isBoundIn_imp_fastAdmitsAux F v u ∅ h1
Proof state after:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ u ∉ ∅
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_fastAdmits
Proof state before:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ u ∉ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h1 : ¬(t = x ∨ occursIn t phi)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    split_ifs
    case pos c1 =>
      simp only [fastAdmitsAux]
      subst c1
      right
      apply not_isFreeIn_imp_fastAdmitsAux
      intro contra
      apply h1_right
      apply isFreeIn_imp_occursIn
      exact contra
    case neg c1 =>
      simp only [fastAdmitsAux]
      right
      apply phi_ih (binders ∪ {x}) h1_right
      simp
      tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ t ∈ List.map (fun x => if v = x then t else x) a✝ → v ∉ binders

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ t ∈ List.map (fun x => if v = x then t else x) a✝ → v ∉ binders

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ t = a✝)
h2 : v ∉ binders
⊢ ((t = if v = a✝¹ then t else a✝¹) ∨ t = if v = a✝ then t else a✝) → v ∉ binders

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝)

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝¹) ∧ fastAdmitsAux t v binders (fastReplaceFree v t a✝)

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝¹) ∧ fastAdmitsAux t v binders (fastReplaceFree v t a✝)

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝¹) ∧ fastAdmitsAux t v binders (fastReplaceFree v t a✝)

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝¹) ∧ fastAdmitsAux t v binders (fastReplaceFree v t a✝)

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ t ∈ List.map (fun x => if v = x then t else x) a✝ → v ∉ binders
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (def_ a✝¹ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
simp only [occursIn] at h1
Proof state after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (def_ a✝¹ a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
simp only [fastReplaceFree]
Proof state after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))
Tactic:
simp only [fastAdmitsAux]
Proof state after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ t ∈ List.map (fun x => if v = x then t else x) a✝ → v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h1 : ¬(t = x ∨ occursIn t phi)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
push_neg at h1
Proof state after:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1 : t ≠ x ∧ ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1 : t ≠ x ∧ ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
cases h1
Proof state after:
case intro
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
left✝ : t ≠ x
right✝ : ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
case intro h1_left h1_right =>
  split_ifs
  case pos c1 =>
    simp only [fastAdmitsAux]
    subst c1
    right
    apply not_isFreeIn_imp_fastAdmitsAux
    intro contra
    apply h1_right
    apply isFreeIn_imp_occursIn
    exact contra
  case neg c1 =>
    simp only [fastAdmitsAux]
    right
    apply phi_ih (binders ∪ {x}) h1_right
    simp
    tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
split_ifs
Proof state after:
case pos
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
h✝ : v = x
⊢ fastAdmitsAux t v binders (exists_ x phi)

case neg
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
h✝ : ¬v = x
⊢ fastAdmitsAux t v binders (exists_ x (fastReplaceFree v t phi))
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ fastAdmitsAux t v binders (exists_ x phi)
Tactic:
case pos c1 =>
  simp only [fastAdmitsAux]
  subst c1
  right
  apply not_isFreeIn_imp_fastAdmitsAux
  intro contra
  apply h1_right
  apply isFreeIn_imp_occursIn
  exact contra
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ fastAdmitsAux t v binders (exists_ x (fastReplaceFree v t phi))
Tactic:
case neg c1 =>
  simp only [fastAdmitsAux]
  right
  apply phi_ih (binders ∪ {x}) h1_right
  simp
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ fastAdmitsAux t v binders (exists_ x phi)
Tactic:
simp only [fastAdmitsAux]
Proof state after:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ t = x ∨ fastAdmitsAux t v (binders ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ t = x ∨ fastAdmitsAux t v (binders ∪ {x}) phi
Tactic:
subst c1
Proof state after:
v t : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_right : ¬occursIn t phi
h1_left : t ≠ v
⊢ t = v ∨ fastAdmitsAux t v (binders ∪ {v}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
v t : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_right : ¬occursIn t phi
h1_left : t ≠ v
⊢ t = v ∨ fastAdmitsAux t v (binders ∪ {v}) phi
Tactic:
right
Proof state after:
case h
v t : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_right : ¬occursIn t phi
h1_left : t ≠ v
⊢ fastAdmitsAux t v (binders ∪ {v}) phi