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

State before:
F : Formula
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t F
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t 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✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (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✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (pred_var_ a✝¹ a✝))

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

case true_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t true_
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t true_)

case false_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t false_
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t false_)

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝.not_
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝.not_)

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.imp_ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (a✝¹.imp_ a✝))

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.and_ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (a✝¹.and_ a✝))

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.or_ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (a✝¹.or_ a✝))

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.iff_ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (a✝¹.iff_ a✝))

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (forall_ a✝¹ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (forall_ a✝¹ a✝))

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (exists_ a✝¹ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (exists_ a✝¹ a✝))

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (def_ a✝¹ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (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✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (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✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (pred_var_ a✝¹ a✝))

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

case true_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t true_
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t true_)

case false_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t false_
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t false_)

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝.not_
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝.not_)

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.imp_ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (a✝¹.imp_ a✝))

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.and_ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (a✝¹.and_ a✝))

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.or_ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (a✝¹.or_ a✝))

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.iff_ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (a✝¹.iff_ a✝))

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (forall_ a✝¹ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (forall_ a✝¹ a✝))

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t (exists_ a✝¹ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (exists_ a✝¹ a✝))

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (def_ a✝¹ a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
all_goals
  simp only [occursIn] at h1
  simp only [fastReplaceFree]
State after:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (pred_const_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (pred_var_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))

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

case true_
v t : VarName
binders : Finset VarName
h1 : ¬False
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders true_

case false_
v t : VarName
binders : Finset VarName
h1 : ¬False
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders false_

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝).not_

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

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

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

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

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = a✝¹ then forall_ a✝¹ a✝ else forall_ a✝¹ (fastReplaceFree v t a✝))

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = a✝¹ then exists_ a✝¹ a✝ else exists_ a✝¹ (fastReplaceFree v t a✝))

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))

State before:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (pred_const_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (pred_var_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))

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

case true_
v t : VarName
binders : Finset VarName
h1 : ¬False
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders true_

case false_
v t : VarName
binders : Finset VarName
h1 : ¬False
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders false_

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝).not_

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

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

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

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

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = a✝¹ then forall_ a✝¹ a✝ else forall_ a✝¹ (fastReplaceFree v t a✝))

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = a✝¹ then exists_ a✝¹ a✝ else exists_ a✝¹ (fastReplaceFree v t a✝))

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))
Tactic:
any_goals
  simp only [fastAdmitsAux]
State after:
case pred_const_
v t : VarName
a✝¹ : PredName
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

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

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

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝)

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

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

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

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

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = a✝¹ then forall_ a✝¹ a✝ else forall_ a✝¹ (fastReplaceFree v t a✝))

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = a✝¹ then exists_ a✝¹ a✝ else exists_ a✝¹ (fastReplaceFree v t a✝))

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

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
h1 : ¬(t = x ∨ occursIn t phi)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    split_ifs
    case pos c1 =>
      simp only [fastAdmitsAux]
      subst c1
      right
      apply not_isFreeIn_imp_fastAdmitsAux
      intro contra
      apply h1_right
      apply isFreeIn_imp_occursIn
      exact contra
    case neg c1 =>
      simp only [fastAdmitsAux]
      right
      apply phi_ih (binders ∪ {x}) h1_right
      simp
      tauto
State after:
no goals

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

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

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

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t a✝)

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

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

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

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

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:
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✝)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (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✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (def_ a✝¹ a✝))

State before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
simp only [fastReplaceFree]
State after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))

State before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x 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✝
h2 : v ∉ binders
⊢ t ∈ List.map (fun x => if v = x then t else x) a✝ → v ∉ binders

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
h1 : ¬(t = x ∨ occursIn t phi)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
push_neg at h1
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 : t ≠ x ∧ ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))

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 : t ≠ x ∧ ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
cases h1
State after:
case intro
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
left✝ : t ≠ x
right✝ : ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))

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
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
case intro h1_left h1_right =>
  split_ifs
  case pos c1 =>
    simp only [fastAdmitsAux]
    subst c1
    right
    apply not_isFreeIn_imp_fastAdmitsAux
    intro contra
    apply h1_right
    apply isFreeIn_imp_occursIn
    exact contra
  case neg c1 =>
    simp only [fastAdmitsAux]
    right
    apply phi_ih (binders ∪ {x}) h1_right
    simp
    tauto
State after:
no goals

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
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
split_ifs
State after:
case pos
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
h✝ : v = x
⊢ fastAdmitsAux t v binders (exists_ x phi)

case neg
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
h✝ : ¬v = x
⊢ fastAdmitsAux t v binders (exists_ x (fastReplaceFree v t phi))

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 phi)
Tactic:
case pos c1 =>
  simp only [fastAdmitsAux]
  subst c1
  right
  apply not_isFreeIn_imp_fastAdmitsAux
  intro contra
  apply h1_right
  apply isFreeIn_imp_occursIn
  exact contra
State after:
no goals

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:
case neg c1 =>
  simp only [fastAdmitsAux]
  right
  apply phi_ih (binders ∪ {x}) h1_right
  simp
  tauto
State after:
no goals

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 phi)
Tactic:
simp only [fastAdmitsAux]
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}) phi

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}) phi
Tactic:
subst c1
State after:
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
⊢ t = v ∨ fastAdmitsAux t v (binders ∪ {v}) phi

State before:
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
⊢ t = v ∨ fastAdmitsAux t v (binders ∪ {v}) phi
Tactic:
right
State after:
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

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

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

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

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

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

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

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

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

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

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

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