internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
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
Tactic:
apply not_isFreeIn_imp_fastAdmitsAux
Proof state after:
case h.h1
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
⊢ ¬isFreeIn t phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case h.h1
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
⊢ ¬isFreeIn t phi
Tactic:
intro contra
Proof state after:
case h.h1
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
contra : isFreeIn t phi
⊢ False
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case h.h1
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
contra : isFreeIn t phi
⊢ False
Tactic:
apply h1_right
Proof state after:
case h.h1
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
contra : isFreeIn t phi
⊢ occursIn t phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case h.h1
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
contra : isFreeIn t phi
⊢ occursIn t phi
Tactic:
apply isFreeIn_imp_occursIn
Proof state after:
case h.h1.h1
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
contra : isFreeIn t phi
⊢ isFreeIn t phi
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case h.h1.h1
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
contra : isFreeIn t phi
⊢ isFreeIn t phi
Tactic:
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:
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}) (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
⊢ t = x ∨ fastAdmitsAux t v (binders ∪ {x}) (fastReplaceFree v t phi)
Tactic:
right
Proof state after:
case h
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 ∪ {x}) (fastReplaceFree v t phi)
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case h
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 ∪ {x}) (fastReplaceFree v t phi)
Tactic:
apply phi_ih (binders ∪ {x}) h1_right
Proof state after:
case h
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
⊢ v ∉ binders ∪ {x}
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case h
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
⊢ v ∉ binders ∪ {x}
Tactic:
simp
Proof state after:
case h
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
⊢ v ∉ binders ∧ ¬v = x
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_aux_fastAdmitsAux
Proof state before:
case h
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
⊢ v ∉ binders ∧ ¬v = x
Tactic:
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 : t ∉ a✝
h2 : v ∉ binders
⊢ t ∈ List.map (fun x => if v = x then t else x) a✝ → v ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_fastAdmits
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmits t v (fastReplaceFree v t F)
Tactic:
simp only [fastAdmits]
Proof state after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmitsAux t v ∅ (fastReplaceFree v t F)
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_fastAdmits
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmitsAux t v ∅ (fastReplaceFree v t F)
Tactic:
apply fastReplaceFree_aux_fastAdmitsAux F v t ∅ h1
Proof state after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ v ∉ ∅
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_fastAdmits
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ v ∉ ∅
Tactic:
simp
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)
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) → v ∉ binders
Tactic:
case eq_ x y =>
  push_neg at h1
  intros a1
  split_ifs at a1
  case _ c1 c2 =>
    cases c1
    case intro c1_left c1_right =>
      subst c1_left
      exact c1_right
  case _ c1 c2 =>
    cases c1
    case intro c1_left c1_right =>
      subst c1_left
      exact c1_right
  case _ c1 c2 =>
    cases c2
    case intro c2_left c2_right =>
      subst c2_left
      exact c2_right
  case _ c1 c2 =>
    tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → fastAdmitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders a✝)

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

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

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

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

case forall_
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✝)

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:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (def_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (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✝
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (def_ a✝¹ a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (def_ a✝¹ a✝))
Tactic:
simp only [replaceFreeAux]
Proof state after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ fastAdmitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ fastAdmitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders 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✝
⊢ t ∈ List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝ → v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
⊢ t ∈ List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs → v ∉ binders
Tactic:
simp
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
⊢ ∀ x ∈ xs, ((v = x → x ∈ binders) → x = t) → v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
⊢ ∀ x ∈ xs, ((v = x → x ∈ binders) → x = t) → v ∉ binders
Tactic:
intro x a1 a2
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
⊢ v ∉ binders
Tactic:
by_cases c1 : v = x ∧ x ∉ binders
Proof state after:
case pos
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
c1 : v = x ∧ x ∉ binders
⊢ v ∉ binders

case neg
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
c1 : ¬(v = x ∧ x ∉ binders)
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case pos
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
c1 : v = x ∧ x ∉ binders
⊢ v ∉ binders
Tactic:
cases c1
Proof state after:
case pos.intro
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
left✝ : v = x
right✝ : x ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
case _ c1_left c1_right =>
  subst c1_left
  exact c1_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
subst c1_left
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
a1 : v ∈ xs
a2 : (v = v → v ∈ binders) → v = t
c1_right : v ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
a1 : v ∈ xs
a2 : (v = v → v ∈ binders) → v = t
c1_right : v ∉ binders
⊢ v ∉ binders
Tactic:
exact c1_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case neg
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
c1 : ¬(v = x ∧ x ∉ binders)
⊢ v ∉ binders
Tactic:
push_neg at c1
Proof state after:
case neg
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
c1 : v = x → x ∈ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case neg
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
c1 : v = x → x ∈ binders
⊢ v ∉ binders
Tactic:
specialize a2 c1
Proof state after:
case neg
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : v = x → x ∈ binders
a2 : x = t
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case neg
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : v = x → x ∈ binders
a2 : x = t
⊢ v ∉ binders
Tactic:
subst a2
Proof state after:
case neg
v : VarName
X : DefName
xs : List VarName
binders : Finset VarName
x : VarName
a1 : x ∈ xs
c1 : v = x → x ∈ binders
h1 : x ∉ xs
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
case neg
v : VarName
X : DefName
xs : List VarName
binders : Finset VarName
x : VarName
a1 : x ∈ xs
c1 : v = x → x ∈ binders
h1 : x ∉ xs
⊢ v ∉ binders
Tactic:
contradiction
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)
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) → v ∉ binders
Tactic:
push_neg at h1
Proof state after:
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) → v ∉ binders
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
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) → v ∉ binders
Tactic:
intros a1
Proof state after:
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
a1 : (t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y
⊢ v ∉ binders
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
a1 : (t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y
⊢ v ∉ binders
Tactic:
split_ifs at a1
Proof state after:
case pos
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
h✝¹ : v = x ∧ x ∉ binders
h✝ : v = y ∧ y ∉ binders
a1 : t = t ∨ t = t
⊢ v ∉ binders

case neg
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
h✝¹ : v = x ∧ x ∉ binders
h✝ : ¬(v = y ∧ y ∉ binders)
a1 : t = t ∨ t = y
⊢ v ∉ binders

case pos
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
h✝¹ : ¬(v = x ∧ x ∉ binders)
h✝ : v = y ∧ y ∉ binders
a1 : t = x ∨ t = t
⊢ v ∉ binders

case neg
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
h✝¹ : ¬(v = x ∧ x ∉ binders)
h✝ : ¬(v = y ∧ y ∉ binders)
a1 : t = x ∨ t = y
⊢ v ∉ binders
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 = t ∨ t = t
⊢ v ∉ binders
Tactic:
case _ c1 c2 =>
  cases c1
  case intro c1_left c1_right =>
    subst c1_left
    exact c1_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 = t ∨ t = y
⊢ v ∉ binders
Tactic:
case _ c1 c2 =>
  cases c1
  case intro c1_left c1_right =>
    subst c1_left
    exact c1_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 = t
⊢ v ∉ binders
Tactic:
case _ c1 c2 =>
  cases c2
  case intro c2_left c2_right =>
    subst c2_left
    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:
case _ c1 c2 =>
  tauto
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 = t ∨ t = t
⊢ v ∉ binders
Tactic:
cases c1
Proof state after:
case intro
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c2 : v = y ∧ y ∉ binders
a1 : t = t ∨ t = t
left✝ : v = x
right✝ : x ∉ binders
⊢ v ∉ binders
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
c2 : v = y ∧ y ∉ binders
a1 : t = t ∨ t = t
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
case intro c1_left c1_right =>
  subst c1_left
  exact c1_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
c2 : v = y ∧ y ∉ binders
a1 : t = t ∨ t = t
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
subst c1_left
Proof state after:
v t y : VarName
binders : Finset VarName
c2 : v = y ∧ y ∉ binders
a1 : t = t ∨ t = t
h1 : t ≠ v ∧ t ≠ y
c1_right : v ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t y : VarName
binders : Finset VarName
c2 : v = y ∧ y ∉ binders
a1 : t = t ∨ t = t
h1 : t ≠ v ∧ t ≠ y
c1_right : v ∉ binders
⊢ v ∉ binders
Tactic:
exact c1_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 = t ∨ t = y
⊢ v ∉ binders
Tactic:
cases c1
Proof state after:
case intro
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c2 : ¬(v = y ∧ y ∉ binders)
a1 : t = t ∨ t = y
left✝ : v = x
right✝ : x ∉ binders
⊢ v ∉ binders
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
c2 : ¬(v = y ∧ y ∉ binders)
a1 : t = t ∨ t = y
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
case intro c1_left c1_right =>
  subst c1_left
  exact c1_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
c2 : ¬(v = y ∧ y ∉ binders)
a1 : t = t ∨ t = y
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
subst c1_left
Proof state after:
v t y : VarName
binders : Finset VarName
c2 : ¬(v = y ∧ y ∉ binders)
a1 : t = t ∨ t = y
h1 : t ≠ v ∧ t ≠ y
c1_right : v ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux
Proof state before:
v t y : VarName
binders : Finset VarName
c2 : ¬(v = y ∧ y ∉ binders)
a1 : t = t ∨ t = y
h1 : t ≠ v ∧ t ≠ y
c1_right : v ∉ binders
⊢ v ∉ binders
Tactic:
exact c1_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 = t
⊢ v ∉ binders
Tactic:
cases c2
Proof state after:
case intro
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
a1 : t = x ∨ t = t
left✝ : v = y
right✝ : y ∉ binders
⊢ v ∉ binders
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:
case intro c2_left c2_right =>
  subst c2_left
  exact c2_right
Proof state after:
no goals