internlm/Lean-Github huggingface dataset:
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2 : xs ∈ RegExp.languageOf α (RegExp.derivative a e) ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
cases a2
Proof state after:
case mp.intro
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
left✝ : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
right✝ : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
case _ a2_left a2_right =>
  apply Exists.elim a2_right
  intro ys a3
  clear a2_right
  cases a3
  case _ a3_left a3_right =>
    apply Exists.intro [(a :: w)]
    simp
    simp only [← ih]
    sorry
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
apply Exists.elim a2_right
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∀ (a_1 : List (List α)),
    (∀ r ∈ a_1, r ∈ RegExp.languageOf α e) ∧ xs ++ a_1.join = w →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∀ (a_1 : List (List α)),
    (∀ r ∈ a_1, r ∈ RegExp.languageOf α e) ∧ xs ++ a_1.join = w →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
intro ys a3
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α e) ∧ xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α e) ∧ xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
clear a2_right
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α e) ∧ xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α e) ∧ xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
cases a3
Proof state after:
case intro
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
left✝ : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
right✝ : xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
case _ a3_left a3_right =>
  apply Exists.intro [(a :: w)]
  simp
  simp only [← ih]
  sorry
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
apply Exists.intro [(a :: w)]
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ (∀ r ∈ [a :: w], r ∈ RegExp.languageOf α e) ∧ [a :: w].join = a :: w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ (∀ r ∈ [a :: w], r ∈ RegExp.languageOf α e) ∧ [a :: w].join = a :: w
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ a :: w ∈ RegExp.languageOf α e
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ a :: w ∈ RegExp.languageOf α e
Tactic:
simp only [← ih]
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a e)
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a e)
Tactic:
sorry
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
⊢ v ∈ a✝ → u ∉ binders

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

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

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

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

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

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

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

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
⊢ v ∈ a✝ → u ∉ binders
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u binders (def_ a✝¹ a✝)
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Tactic:
simp only [admitsAux] at h2
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ ∧ v ∉ binders → 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 : v ∉ binders
h2 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
⊢ v ∈ a✝ → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
by_cases c1 : v = x
Proof state after:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
left
Proof state after:
case pos.h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ v = x
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case pos.h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ v = x
Tactic:
exact c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
right
Proof state after:
case neg.h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ fastAdmitsAux v u (binders ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case neg.h
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
apply phi_ih
Proof state after:
case neg.h.h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ v ∉ binders ∪ {x}

case neg.h.h2
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ admitsAux v u (binders ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case neg.h.h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ v ∉ binders ∪ {x}
Tactic:
simp
Proof state after:
case neg.h.h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ v ∉ binders ∧ ¬v = x
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case neg.h.h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ v ∉ binders ∧ ¬v = x
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case neg.h.h2
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ admitsAux v u (binders ∪ {x}) phi
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
⊢ v ∈ a✝ → u ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.mem_binders_imp_admitsAux
Proof state before:
F : Formula
v u : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders F
Tactic:
induction F generalizing binders
Proof state after:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (pred_const_ a✝¹ a✝)

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (pred_var_ a✝¹ a✝)

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (eq_ a✝¹ a✝)

case true_
v u : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders true_

case false_
v u : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders false_

case not_
v u : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders a✝.not_

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (a✝¹.imp_ a✝)

case and_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (a✝¹.and_ a✝)

case or_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (a✝¹.or_ a✝)

case iff_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (a✝¹.iff_ a✝)

case forall_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (forall_ a✝¹ a✝)

case exists_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (exists_ a✝¹ a✝)

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.mem_binders_imp_admitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders phi
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u (binders ∪ {x}) phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  apply phi_ih
  simp
  left
  exact h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.mem_binders_imp_admitsAux
Proof state before:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ a✝ ∧ v ∉ binders → u ∉ binders

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

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

case not_
v u : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders a✝

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders a✝¹ ∧ admitsAux v u binders a✝

case and_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders a✝¹ ∧ admitsAux v u binders a✝

case or_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders a✝¹ ∧ admitsAux v u binders a✝

case iff_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝¹
a_ih✝ : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders a✝
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders a✝¹ ∧ admitsAux v u binders a✝

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ a✝ ∧ v ∉ binders → u ∉ binders
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.mem_binders_imp_admitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u binders (def_ a✝¹ a✝)
Tactic:
simp only [admitsAux]
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ a✝ ∧ v ∉ binders → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.mem_binders_imp_admitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders phi
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u (binders ∪ {x}) phi
Tactic:
apply phi_ih
Proof state after:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∪ {x}
Theorem: FOL.NV.Sub.Var.One.Rec.mem_binders_imp_admitsAux
Proof state before:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∪ {x}
Tactic:
simp
Proof state after:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∨ v = x