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

State before:
F : Formula
v u : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders F = toIsBoundAux binders (fastReplaceFree v u F)
⊢ fastAdmitsAux v u binders F
Tactic:
induction F generalizing binders
State after:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (pred_const_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (pred_const_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (pred_const_ a✝¹ a✝)

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (pred_var_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (pred_var_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (pred_var_ a✝¹ a✝)

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (eq_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (eq_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (eq_ a✝¹ a✝)

case true_
v u : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders true_ = toIsBoundAux binders (fastReplaceFree v u true_)
⊢ fastAdmitsAux v u binders true_

case false_
v u : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders false_ = toIsBoundAux binders (fastReplaceFree v u false_)
⊢ fastAdmitsAux v u binders false_

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

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

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

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

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

case forall_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (forall_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (forall_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (forall_ a✝¹ a✝)

case exists_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (exists_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (exists_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (exists_ a✝¹ a✝)

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (def_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)

State before:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (pred_const_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (pred_const_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (pred_const_ a✝¹ a✝)

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (pred_var_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (pred_var_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (pred_var_ a✝¹ a✝)

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (eq_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (eq_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (eq_ a✝¹ a✝)

case true_
v u : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders true_ = toIsBoundAux binders (fastReplaceFree v u true_)
⊢ fastAdmitsAux v u binders true_

case false_
v u : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders false_ = toIsBoundAux binders (fastReplaceFree v u false_)
⊢ fastAdmitsAux v u binders false_

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

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

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

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

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

case forall_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (forall_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (forall_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (forall_ a✝¹ a✝)

case exists_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (exists_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (exists_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (exists_ a✝¹ a✝)

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

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

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

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

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (a✝¹.imp_ a✝) = toIsBoundAux binders ((fastReplaceFree v u a✝¹).imp_ (fastReplaceFree v u 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 →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (a✝¹.and_ a✝) = toIsBoundAux binders ((fastReplaceFree v u a✝¹).and_ (fastReplaceFree v u 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 →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (a✝¹.or_ a✝) = toIsBoundAux binders ((fastReplaceFree v u a✝¹).or_ (fastReplaceFree v u 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 →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (a✝¹.iff_ a✝) = toIsBoundAux binders ((fastReplaceFree v u a✝¹).iff_ (fastReplaceFree v u a✝))
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case forall_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (forall_ a✝¹ a✝) =
    toIsBoundAux binders (if v = a✝¹ then forall_ a✝¹ a✝ else forall_ a✝¹ (fastReplaceFree v u a✝))
⊢ v = a✝¹ ∨ fastAdmitsAux v u (binders ∪ {a✝¹}) a✝

case exists_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (exists_ a✝¹ a✝) =
    toIsBoundAux binders (if v = a✝¹ then exists_ a✝¹ a✝ else exists_ a✝¹ (fastReplaceFree v u a✝))
⊢ v = a✝¹ ∨ fastAdmitsAux v u (binders ∪ {a✝¹}) a✝

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

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

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

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

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

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (a✝¹.imp_ a✝) = toIsBoundAux binders ((fastReplaceFree v u a✝¹).imp_ (fastReplaceFree v u 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 →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (a✝¹.and_ a✝) = toIsBoundAux binders ((fastReplaceFree v u a✝¹).and_ (fastReplaceFree v u 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 →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (a✝¹.or_ a✝) = toIsBoundAux binders ((fastReplaceFree v u a✝¹).or_ (fastReplaceFree v u 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 →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (a✝¹.iff_ a✝) = toIsBoundAux binders ((fastReplaceFree v u a✝¹).iff_ (fastReplaceFree v u a✝))
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case forall_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (forall_ a✝¹ a✝) =
    toIsBoundAux binders (if v = a✝¹ then forall_ a✝¹ a✝ else forall_ a✝¹ (fastReplaceFree v u a✝))
⊢ v = a✝¹ ∨ fastAdmitsAux v u (binders ∪ {a✝¹}) a✝

case exists_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (exists_ a✝¹ a✝) =
    toIsBoundAux binders (if v = a✝¹ then exists_ a✝¹ a✝ else exists_ a✝¹ (fastReplaceFree v u a✝))
⊢ v = a✝¹ ∨ fastAdmitsAux v u (binders ∪ {a✝¹}) a✝

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (def_ a✝¹ (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders
Tactic:
any_goals
  simp only [toIsBoundAux] at h2
State after:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.pred_const_ a✝¹ (List.map (fun v => decide (v ∈ binders)) a✝) =
    BoolFormula.pred_const_ a✝¹
      (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.pred_var_ a✝¹ (List.map (fun v => decide (v ∈ binders)) a✝) =
    BoolFormula.pred_var_ a✝¹ (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.eq_ (decide (a✝¹ ∈ binders)) (decide (a✝ ∈ binders)) =
    BoolFormula.eq_ (decide ((if v = a✝¹ then u else a✝¹) ∈ binders)) (decide ((if v = a✝ then u else a✝) ∈ binders))
⊢ v = a✝¹ ∨ v = a✝ → u ∉ binders

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

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  (toIsBoundAux binders a✝¹).imp_ (toIsBoundAux binders a✝) =
    (toIsBoundAux binders (fastReplaceFree v u a✝¹)).imp_ (toIsBoundAux binders (fastReplaceFree v u 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 →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  (toIsBoundAux binders a✝¹).and_ (toIsBoundAux binders a✝) =
    (toIsBoundAux binders (fastReplaceFree v u a✝¹)).and_ (toIsBoundAux binders (fastReplaceFree v u 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 →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  (toIsBoundAux binders a✝¹).or_ (toIsBoundAux binders a✝) =
    (toIsBoundAux binders (fastReplaceFree v u a✝¹)).or_ (toIsBoundAux binders (fastReplaceFree v u 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 →
      toIsBoundAux binders a✝¹ = toIsBoundAux binders (fastReplaceFree v u a✝¹) → fastAdmitsAux v u binders a✝¹
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  (toIsBoundAux binders a✝¹).iff_ (toIsBoundAux binders a✝) =
    (toIsBoundAux binders (fastReplaceFree v u a✝¹)).iff_ (toIsBoundAux binders (fastReplaceFree v u a✝))
⊢ fastAdmitsAux v u binders a✝¹ ∧ fastAdmitsAux v u binders a✝

case forall_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {a✝¹}) a✝) =
    toIsBoundAux binders (if v = a✝¹ then forall_ a✝¹ a✝ else forall_ a✝¹ (fastReplaceFree v u a✝))
⊢ v = a✝¹ ∨ fastAdmitsAux v u (binders ∪ {a✝¹}) a✝

case exists_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (binders : Finset VarName),
    v ∉ binders → toIsBoundAux binders a✝ = toIsBoundAux binders (fastReplaceFree v u a✝) → fastAdmitsAux v u binders a✝
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {a✝¹}) a✝) =
    toIsBoundAux binders (if v = a✝¹ then exists_ a✝¹ a✝ else exists_ a✝¹ (fastReplaceFree v u a✝))
⊢ v = a✝¹ ∨ fastAdmitsAux v u (binders ∪ {a✝¹}) a✝

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.def_ a✝¹ (List.map (fun v => decide (v ∈ binders)) a✝) =
    BoolFormula.def_ a✝¹ (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) xs) =
    BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) xs))
⊢ v ∈ xs → u ∉ binders
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp at h2
  simp only [List.map_eq_map_iff] at h2
  intro a1
  specialize h2 v a1
  simp at h2
  tauto
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.eq_ (decide (x ∈ binders)) (decide (y ∈ binders)) =
    BoolFormula.eq_ (decide ((if v = x then u else x) ∈ binders)) (decide ((if v = y then u else y) ∈ binders))
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
case eq_ x y =>
  simp at h2
  cases h2
  case intro h2_left h2_right =>
    intros a1
    cases a1
    case inl a1 =>
      subst a1
      simp at h2_left
      tauto
    case inr a1 =>
      subst a1
      simp at h2_right
      tauto
State after:
no goals

State before:
v u : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : (toIsBoundAux binders phi).not_ = (toIsBoundAux binders (fastReplaceFree v u phi)).not_
⊢ fastAdmitsAux v u binders phi
Tactic:
case not_ phi phi_ih =>
  simp at h2
  exact phi_ih binders h1 h2
State after:
no goals

State before:
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi) → fastAdmitsAux v u binders psi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  (toIsBoundAux binders phi).iff_ (toIsBoundAux binders psi) =
    (toIsBoundAux binders (fastReplaceFree v u phi)).iff_ (toIsBoundAux binders (fastReplaceFree v u psi))
⊢ fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp at h2
  tauto
State after:
no goals

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

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

State before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (def_ a✝¹ (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders
Tactic:
simp only [toIsBoundAux] at h2
State after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.def_ a✝¹ (List.map (fun v => decide (v ∈ binders)) a✝) =
    BoolFormula.def_ a✝¹ (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) xs) =
    BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) xs))
⊢ v ∈ xs → u ∉ binders
Tactic:
simp at h2
State after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  List.map (fun v => decide (v ∈ binders)) xs =
    List.map ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) xs
⊢ v ∈ xs → u ∉ binders

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  List.map (fun v => decide (v ∈ binders)) xs =
    List.map ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) xs
⊢ v ∈ xs → u ∉ binders
Tactic:
simp only [List.map_eq_map_iff] at h2
State after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : ∀ x ∈ xs, decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) x
⊢ v ∈ xs → u ∉ binders

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : ∀ x ∈ xs, decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) x
⊢ v ∈ xs → u ∉ binders
Tactic:
intro a1
State after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : ∀ x ∈ xs, decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) x
a1 : v ∈ xs
⊢ u ∉ binders

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : ∀ x ∈ xs, decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) x
a1 : v ∈ xs
⊢ u ∉ binders
Tactic:
specialize h2 v a1
State after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v ∈ xs
h2 : decide (v ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) v
⊢ u ∉ binders

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v ∈ xs
h2 : decide (v ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) v
⊢ u ∉ binders
Tactic:
simp at h2
State after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v ∈ xs
h2 : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v ∈ xs
h2 : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders
Tactic:
tauto
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.eq_ (decide (x ∈ binders)) (decide (y ∈ binders)) =
    BoolFormula.eq_ (decide ((if v = x then u else x) ∈ binders)) (decide ((if v = y then u else y) ∈ binders))
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
simp at h2
State after:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : (x ∈ binders ↔ (if v = x then u else x) ∈ binders) ∧ (y ∈ binders ↔ (if v = y then u else y) ∈ binders)
⊢ v = x ∨ v = y → u ∉ binders

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : (x ∈ binders ↔ (if v = x then u else x) ∈ binders) ∧ (y ∈ binders ↔ (if v = y then u else y) ∈ binders)
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
cases h2
State after:
case intro
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
left✝ : x ∈ binders ↔ (if v = x then u else x) ∈ binders
right✝ : y ∈ binders ↔ (if v = y then u else y) ∈ binders
⊢ v = x ∨ v = y → u ∉ binders

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
case intro h2_left h2_right =>
  intros a1
  cases a1
  case inl a1 =>
    subst a1
    simp at h2_left
    tauto
  case inr a1 =>
    subst a1
    simp at h2_right
    tauto
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
intros a1
State after:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = x ∨ v = y
⊢ u ∉ binders

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = x ∨ v = y
⊢ u ∉ binders
Tactic:
cases a1
State after:
case inl
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h✝ : v = x
⊢ u ∉ binders

case inr
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h✝ : v = y
⊢ u ∉ binders

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = x
⊢ u ∉ binders
Tactic:
case inl a1 =>
  subst a1
  simp at h2_left
  tauto
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = y
⊢ u ∉ binders
Tactic:
case inr a1 =>
  subst a1
  simp at h2_right
  tauto
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = x
⊢ u ∉ binders
Tactic:
subst a1
State after:
v u y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h2_left : v ∈ binders ↔ (if v = v then u else v) ∈ binders
⊢ u ∉ binders

State before:
v u y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h2_left : v ∈ binders ↔ (if v = v then u else v) ∈ binders
⊢ u ∉ binders
Tactic:
simp at h2_left
State after:
v u y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h2_left : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders

State before:
v u y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h2_left : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders
Tactic:
tauto
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = y
⊢ u ∉ binders
Tactic:
subst a1
State after:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ (if v = v then u else v) ∈ binders
⊢ u ∉ binders

State before:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ (if v = v then u else v) ∈ binders
⊢ u ∉ binders
Tactic:
simp at h2_right
State after:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders

State before:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders
Tactic:
tauto
State after:
no goals

State before:
v u : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : (toIsBoundAux binders phi).not_ = (toIsBoundAux binders (fastReplaceFree v u phi)).not_
⊢ fastAdmitsAux v u binders phi
Tactic:
simp at h2
State after:
v u : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
⊢ fastAdmitsAux v u binders phi

State before:
v u : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
⊢ fastAdmitsAux v u binders phi
Tactic:
exact phi_ih binders h1 h2
State after:
no goals

State before:
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi) → fastAdmitsAux v u binders psi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  (toIsBoundAux binders phi).iff_ (toIsBoundAux binders psi) =
    (toIsBoundAux binders (fastReplaceFree v u phi)).iff_ (toIsBoundAux binders (fastReplaceFree v u psi))
⊢ fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
Tactic:
simp at h2
State after:
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi) → fastAdmitsAux v u binders psi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) ∧
    toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi)
⊢ fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi

State before:
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi) → fastAdmitsAux v u binders psi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) ∧
    toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi)
⊢ fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
Tactic:
tauto
State after:
no goals

State before:
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v u phi))
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
split_ifs at h2
State after:
case pos
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h✝ : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi

case neg
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h✝ : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi

State before:
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
case pos c1 =>
  left
  exact c1
State after:
no goals

State before:
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
left
State after:
case h
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x

State before:
case h
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x
Tactic:
exact c1
State after:
no goals

State before:
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
right
State after:
case h
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ fastAdmitsAux v u (binders ∪ {x}) phi

State before:
case h
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
apply phi_ih
State after:
case h.h1
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v ∉ binders ∪ {x}

case h.h2
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)

State before:
case h.h1
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v ∉ binders ∪ {x}
Tactic:
simp
State after:
case h.h1
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v ∉ binders ∧ ¬v = x

State before:
case h.h1
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v ∉ binders ∧ ¬v = x
Tactic:
tauto
State after:
no goals

State before:
case h.h2
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)
Tactic:
simp only [toIsBoundAux] at h2
State after:
case h.h2
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi))
⊢ toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)

State before:
case h.h2
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi))
⊢ toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)
Tactic:
simp at h2
State after:
case h.h2
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 : toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)
⊢ toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)

State before:
case h.h2
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 : toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)
⊢ toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)
Tactic:
exact h2
State after:
no goals