internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_admitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → admitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1_left : u ≠ x
h1_right : ¬isBoundIn u phi
⊢ admitsAux v u (binders ∪ {x}) phi
Tactic:
case intro h1_left h1_right =>
  apply phi_ih (binders ∪ {x}) h1_right
  simp
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_admitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → admitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1_left : u ≠ x
h1_right : ¬isBoundIn u phi
⊢ admitsAux v u (binders ∪ {x}) phi
Tactic:
apply phi_ih (binders ∪ {x}) h1_right
Proof state after:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → admitsAux 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_admitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → admitsAux 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:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → admitsAux 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_admitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → admitsAux 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_admitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ v ∈ a✝ ∧ v ∉ binders → u ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_admits
Proof state before:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ admits v u F
Tactic:
simp only [admits]
Proof state after:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ admitsAux v u ∅ F
Theorem: FOL.NV.Sub.Var.One.Rec.not_isBoundIn_imp_admits
Proof state before:
F : Formula
v u : VarName
h1 : ¬isBoundIn u F
⊢ admitsAux v u ∅ F
Tactic:
apply not_isBoundIn_imp_admitsAux 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_admits
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.replaceFreeAux_admitsAux
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 ∧ t ∉ binders → v ∉ binders
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  intro x a1 a2 a3
  by_cases c1 : v = x ∧ x ∉ binders
  case pos =>
    cases c1
    case intro c1_left c1_right =>
      subst c1_left
      exact c1_right
  case neg =>
    simp at c1
    specialize a2 c1
    subst a2
    contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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) ∧ t ∉ binders → v ∉ binders
Tactic:
case eq_ x y =>
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    intro 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_admitsAux
Proof state before:
case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝)

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

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

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

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

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ admitsAux 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✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ admitsAux 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_admitsAux
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (def_ a✝¹ a✝)
⊢ admitsAux 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✝
⊢ admitsAux t v binders (replaceFreeAux v t binders (def_ a✝¹ a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ admitsAux 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✝
⊢ admitsAux 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_admitsAux
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ admitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝))
Tactic:
simp only [admitsAux]
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✝ ∧ t ∉ binders → v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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 ∧ t ∉ binders → 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) → t ∉ binders → v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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) → t ∉ binders → v ∉ binders
Tactic:
intro x a1 a2 a3
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
a3 : t ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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
a3 : t ∉ binders
⊢ 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
a3 : t ∉ binders
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
a3 : t ∉ binders
c1 : ¬(v = x ∧ x ∉ binders)
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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
a3 : t ∉ binders
c1 : v = x ∧ x ∉ binders
⊢ v ∉ binders
Tactic:
case pos =>
  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_admitsAux
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
a3 : t ∉ binders
c1 : ¬(v = x ∧ x ∉ binders)
⊢ v ∉ binders
Tactic:
case neg =>
  simp at c1
  specialize a2 c1
  subst a2
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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
a3 : t ∉ binders
c1 : v = x ∧ x ∉ binders
⊢ v ∉ binders
Tactic:
cases c1
Proof state after:
case 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
a3 : t ∉ binders
left✝ : v = x
right✝ : x ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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
a3 : t ∉ binders
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_admitsAux
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
a3 : t ∉ binders
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
a3 : t ∉ binders
a1 : v ∈ xs
a2 : (v = v → v ∈ binders) → v = t
c1_right : v ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
a3 : t ∉ binders
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_admitsAux
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
a3 : t ∉ binders
c1 : ¬(v = x ∧ x ∉ binders)
⊢ v ∉ binders
Tactic:
simp at c1
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
a3 : t ∉ binders
c1 : v = x → x ∈ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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
a3 : t ∉ binders
c1 : v = x → x ∈ binders
⊢ v ∉ binders
Tactic:
specialize a2 c1
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a3 : t ∉ binders
c1 : v = x → x ∈ binders
a2 : x = t
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a3 : t ∉ binders
c1 : v = x → x ∈ binders
a2 : x = t
⊢ v ∉ binders
Tactic:
subst a2
Proof state after:
v : VarName
X : DefName
xs : List VarName
binders : Finset VarName
x : VarName
a1 : x ∈ xs
c1 : v = x → x ∈ binders
h1 : x ∉ xs
a3 : x ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
Proof state before:
v : VarName
X : DefName
xs : List VarName
binders : Finset VarName
x : VarName
a1 : x ∈ xs
c1 : v = x → x ∈ binders
h1 : x ∉ xs
a3 : x ∉ binders
⊢ v ∉ binders
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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) ∧ t ∉ binders → 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) ∧ t ∉ binders → v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
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) ∧ t ∉ binders → v ∉ binders
Tactic:
cases h1
Proof state after:
case intro
v t x y : VarName
binders : Finset VarName
left✝ : t ≠ x
right✝ : t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
Proof state before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
Tactic:
case intro h1_left h1_right =>
  intro 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_admitsAux
Proof state before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
Tactic:
intro a1
Proof state after:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
a1 : ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
Proof state before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
a1 : ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
split_ifs at a1
Proof state after:
case pos
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
h✝¹ : v = x ∧ x ∉ binders
h✝ : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
⊢ v ∉ binders

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

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

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