internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
a1 : t = x ∨ t = t
c2_left : v = y
c2_right : y ∉ binders
⊢ v ∉ binders
Tactic:
subst c2_left
Proof state after:
v t x : VarName
binders : Finset VarName
c1 : ¬(v = x ∧ x ∉ binders)
a1 : t = x ∨ t = t
h1 : t ≠ x ∧ t ≠ v
c2_right : v ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t x : VarName
binders : Finset VarName
c1 : ¬(v = x ∧ x ∉ binders)
a1 : t = x ∨ t = t
h1 : t ≠ x ∧ t ≠ v
c2_right : v ∉ binders
⊢ v ∉ binders
Tactic:
exact c2_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
c2 : ¬(v = y ∧ y ∉ binders)
a1 : t = x ∨ t = y
⊢ v ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → fastAdmitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ t = a✝¹ ∨ fastAdmitsAux t v (binders ∪ {a✝¹}) (replaceFreeAux v t (binders ∪ {a✝¹}) a✝)
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFree_fastAdmits
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmits t v (replaceFree v t F)
Tactic:
simp only [replaceFree]
Proof state after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmits t v (replaceFreeAux v t ∅ F)
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFree_fastAdmits
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmits t v (replaceFreeAux v t ∅ F)
Tactic:
simp only [fastAdmits]
Proof state after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmitsAux t v ∅ (replaceFreeAux v t ∅ F)
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFree_fastAdmits
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmitsAux t v ∅ (replaceFreeAux v t ∅ F)
Tactic:
exact replaceFreeAux_fastAdmitsAux F v t ∅ h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (S ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ T ∪ {x}) phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  cases h1
  case inl h1 =>
    tauto
  case inr h1 =>
    specialize phi_ih (S ∪ {x}) h1
    right
    simp only [Finset.union_right_comm_assoc]
    exact phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
case pred_const_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : PredName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → ¬(u ∈ S ∨ u ∈ T)

case pred_var_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : PredName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → ¬(u ∈ S ∨ u ∈ T)

case eq_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : VarName
S : Finset VarName
h1 : v = a✝¹ ∨ v = a✝ → u ∉ S
⊢ v = a✝¹ ∨ v = a✝ → ¬(u ∈ S ∨ u ∈ T)

case not_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝ : Formula
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝

case imp_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

case and_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

case or_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

case iff_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝¹ → fastAdmitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), fastAdmitsAux v u S a✝ → fastAdmitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : fastAdmitsAux v u S a✝¹ ∧ fastAdmitsAux v u S a✝
⊢ fastAdmitsAux v u (S ∪ T) a✝¹ ∧ fastAdmitsAux v u (S ∪ T) a✝

case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → ¬(u ∈ S ∨ u ∈ T)
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : fastAdmitsAux v u S (def_ a✝¹ a✝)
⊢ fastAdmitsAux v u (S ∪ T) (def_ a✝¹ a✝)
Tactic:
simp only [fastAdmitsAux] at h1
Proof state after:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ fastAdmitsAux v u (S ∪ T) (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ fastAdmitsAux v u (S ∪ T) (def_ a✝¹ a✝)
Tactic:
simp only [fastAdmitsAux]
Proof state after:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → u ∉ S ∪ T
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (S ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ T ∪ {x}) phi
Tactic:
simp
Proof state after:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (S ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (S ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Tactic:
cases h1
Proof state after:
case inl
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h✝ : v = x
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi

case inr
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h✝ : fastAdmitsAux v u (S ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : v = x
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Tactic:
case inl h1 =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Tactic:
case inr h1 =>
  specialize phi_ih (S ∪ {x}) h1
  right
  simp only [Finset.union_right_comm_assoc]
  exact phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : v = x
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Tactic:
specialize phi_ih (S ∪ {x}) h1
Proof state after:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ {x}) phi
phi_ih : fastAdmitsAux v u (S ∪ {x} ∪ T) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ {x}) phi
phi_ih : fastAdmitsAux v u (S ∪ {x} ∪ T) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Tactic:
right
Proof state after:
case h
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ {x}) phi
phi_ih : fastAdmitsAux v u (S ∪ {x} ∪ T) phi
⊢ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
case h
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ {x}) phi
phi_ih : fastAdmitsAux v u (S ∪ {x} ∪ T) phi
⊢ fastAdmitsAux v u (S ∪ (T ∪ {x})) phi
Tactic:
simp only [Finset.union_right_comm_assoc]
Proof state after:
case h
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ {x}) phi
phi_ih : fastAdmitsAux v u (S ∪ {x} ∪ T) phi
⊢ fastAdmitsAux v u (S ∪ {x} ∪ T) phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
case h
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ {x}) phi
phi_ih : fastAdmitsAux v u (S ∪ {x} ∪ T) phi
⊢ fastAdmitsAux v u (S ∪ {x} ∪ T) phi
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → u ∉ S ∪ T
Tactic:
simp only [Finset.mem_union]
Proof state after:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → ¬(u ∈ S ∨ u ∈ T)
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_add_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → ¬(u ∈ S ∨ u ∈ T)
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs → u ∉ S ∪ T
⊢ v ∈ xs → u ∉ S
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp at h1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
x y : VarName
S : Finset VarName
h1 : v = x ∨ v = y → u ∉ S ∪ T
⊢ v = x ∨ v = y → u ∉ S
Tactic:
case eq_ x y =>
  simp at h1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) phi → fastAdmitsAux v u S phi
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ T) phi
⊢ fastAdmitsAux v u S phi
Tactic:
case not_ phi phi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
phi psi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) phi → fastAdmitsAux v u S phi
psi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) psi → fastAdmitsAux v u S psi
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ T) phi ∧ fastAdmitsAux v u (S ∪ T) psi
⊢ fastAdmitsAux v u S phi ∧ fastAdmitsAux v u S psi
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) phi → fastAdmitsAux v u S phi
S : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (S ∪ T ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ {x}) phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [Finset.union_right_comm S T {x}] at h1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ T) (def_ a✝¹ a✝)
⊢ fastAdmitsAux v u S (def_ a✝¹ a✝)
Tactic:
simp only [fastAdmitsAux] at h1
Proof state after:
case def_
v u : VarName
T : Finset VarName
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S ∪ T
⊢ fastAdmitsAux v u S (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S ∪ T
⊢ fastAdmitsAux v u S (def_ a✝¹ a✝)
Tactic:
simp only [fastAdmitsAux]
Proof state after:
case def_
v u : VarName
T : Finset VarName
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S ∪ T
⊢ v ∈ a✝ → u ∉ S
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs → u ∉ S ∪ T
⊢ v ∈ xs → u ∉ S
Tactic:
simp at h1
Proof state after:
v u : VarName
T : Finset VarName
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs → u ∉ S ∧ u ∉ T
⊢ v ∈ xs → u ∉ S
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs → u ∉ S ∧ u ∉ T
⊢ v ∈ xs → u ∉ S
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
x y : VarName
S : Finset VarName
h1 : v = x ∨ v = y → u ∉ S ∪ T
⊢ v = x ∨ v = y → u ∉ S
Tactic:
simp at h1
Proof state after:
v u : VarName
T : Finset VarName
x y : VarName
S : Finset VarName
h1 : v = x ∨ v = y → u ∉ S ∧ u ∉ T
⊢ v = x ∨ v = y → u ∉ S
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
x y : VarName
S : Finset VarName
h1 : v = x ∨ v = y → u ∉ S ∧ u ∉ T
⊢ v = x ∨ v = y → u ∉ S
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) phi → fastAdmitsAux v u S phi
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ T) phi
⊢ fastAdmitsAux v u S phi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
phi psi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) phi → fastAdmitsAux v u S phi
psi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) psi → fastAdmitsAux v u S psi
S : Finset VarName
h1 : fastAdmitsAux v u (S ∪ T) phi ∧ fastAdmitsAux v u (S ∪ T) psi
⊢ fastAdmitsAux v u S phi ∧ fastAdmitsAux v u S psi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) phi → fastAdmitsAux v u S phi
S : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (S ∪ T ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ {x}) phi
Tactic:
simp only [Finset.union_right_comm S T {x}] at h1
Proof state after:
v u : VarName
T : Finset VarName
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) phi → fastAdmitsAux v u S phi
S : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (S ∪ {x} ∪ T) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u (S ∪ T) phi → fastAdmitsAux v u S phi
S : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (S ∪ {x} ∪ T) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ {x}) phi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_isFreeIn
Proof state before:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ → u ∉ binders
h2 : v ∈ a✝
⊢ u ∉ binders

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

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

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

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

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

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

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

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ → u ∉ binders
h2 : v ∈ a✝
⊢ u ∉ binders
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_isFreeIn
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : fastAdmitsAux v u binders (def_ a✝¹ a✝)
h2 : isFreeIn v (def_ a✝¹ a✝)
⊢ u ∉ binders
Tactic:
simp only [fastAdmitsAux] at h1
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ → u ∉ binders
h2 : isFreeIn v (def_ a✝¹ a✝)
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_isFreeIn
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ → u ∉ binders
h2 : isFreeIn v (def_ a✝¹ a✝)
⊢ u ∉ binders
Tactic:
simp only [isFreeIn] at h2
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ → u ∉ binders
h2 : v ∈ a✝
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_isFreeIn
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
h2 : ¬v = x ∧ isFreeIn v phi
⊢ u ∉ binders
Tactic:
cases h2
Proof state after:
case intro
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
left✝ : ¬v = x
right✝ : isFreeIn v phi
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_isFreeIn
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ u ∉ binders
Tactic:
cases h1
Proof state after:
case inl
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h2_left : ¬v = x
h2_right : isFreeIn v phi
h✝ : v = x
⊢ u ∉ binders

case inr
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h2_left : ¬v = x
h2_right : isFreeIn v phi
h✝ : fastAdmitsAux v u (binders ∪ {x}) phi
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_isFreeIn
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h2_left : ¬v = x
h2_right : isFreeIn v phi
h1 : v = x
⊢ u ∉ binders
Tactic:
case inl h1 =>
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_isFreeIn
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h2_left : ¬v = x
h2_right : isFreeIn v phi
h1 : v = x
⊢ u ∉ binders
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastAdmitsAux_isFreeIn
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h2_left : ¬v = x
h2_right : isFreeIn v phi
h1 : fastAdmitsAux v u (binders ∪ {x}) phi
⊢ u ∉ binders
Tactic:
apply phi_ih
Proof state after:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h2_left : ¬v = x
h2_right : isFreeIn v phi
h1 : fastAdmitsAux v u (binders ∪ {x}) phi
⊢ fastAdmitsAux v u binders phi

case h2
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h2_left : ¬v = x
h2_right : isFreeIn v phi
h1 : fastAdmitsAux v u (binders ∪ {x}) phi
⊢ isFreeIn v phi