Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_fastAdmitsAux (FOL/NV/Sub/Var/One/Rec/Admits.lean)

State before:
F : Formula
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t F
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders F)
Tactic:
induction F generalizing binders
State after:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (pred_const_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (pred_const_ a✝¹ a✝))

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (pred_var_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (pred_var_ a✝¹ a✝))

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : ¬occursIn t (eq_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (eq_ a✝¹ a✝))

case true_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t true_
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders true_)

case false_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t false_
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders false_)

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✝.not_
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders a✝.not_)

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✝¹.imp_ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (a✝¹.imp_ 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✝¹.and_ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (a✝¹.and_ 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✝¹.or_ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (a✝¹.or_ 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✝¹.iff_ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (a✝¹.iff_ 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 : ¬occursIn t (forall_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (forall_ 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 : ¬occursIn t (exists_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (exists_ a✝¹ a✝))

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

State before:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (pred_const_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (pred_const_ a✝¹ a✝))

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (pred_var_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (pred_var_ a✝¹ a✝))

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : ¬occursIn t (eq_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (eq_ a✝¹ a✝))

case true_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t true_
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders true_)

case false_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t false_
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders false_)

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✝.not_
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders a✝.not_)

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✝¹.imp_ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (a✝¹.imp_ 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✝¹.and_ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (a✝¹.and_ 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✝¹.or_ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (a✝¹.or_ 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✝¹.iff_ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (a✝¹.iff_ 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 : ¬occursIn t (forall_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (forall_ 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 : ¬occursIn t (exists_ a✝¹ a✝)
⊢ fastAdmitsAux t v binders (replaceFreeAux v t binders (exists_ a✝¹ a✝))

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:
all_goals
  simp only [occursIn] at h1
  simp only [replaceFreeAux]
  simp only [fastAdmitsAux]
State after:
case pred_const_
v t : VarName
a✝¹ : PredName
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

case pred_var_
v t : VarName
a✝¹ : PredName
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

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

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

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

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
State after:
no goals

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
State after:
no goals

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

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]
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✝))

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]
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals