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

State before:
F : Formula
v u : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : fastAdmitsAux v u binders F
⊢ toIsBoundAux binders F = toIsBoundAux binders (fastReplaceFree v u 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 : fastAdmitsAux v u binders (pred_const_ a✝¹ a✝)
⊢ toIsBoundAux binders (pred_const_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (pred_const_ a✝¹ a✝))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ → u ∉ binders
⊢ 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✝))

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = a✝¹ ∨ v = a✝ → u ∉ binders
⊢ 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))

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

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

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

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

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

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

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

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ → u ∉ binders
⊢ 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✝))

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
⊢ 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))
Tactic:
case eq_ x y =>
  simp
  constructor
  case left | right =>
    split_ifs
    case pos c1 =>
      subst c1
      tauto
    case neg c1 =>
      rfl
State after:
no goals

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

State before:
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      fastAdmitsAux v u binders phi → toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      fastAdmitsAux v u binders psi → toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi)
binders : Finset VarName
h1 : v ∉ binders
h2 : fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
⊢ (toIsBoundAux binders phi).iff_ (toIsBoundAux binders psi) =
    (toIsBoundAux binders (fastReplaceFree v u phi)).iff_ (toIsBoundAux binders (fastReplaceFree v u 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
  tauto
State after:
no goals

State before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : fastAdmitsAux v u binders (def_ a✝¹ a✝)
⊢ toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (def_ a✝¹ a✝))
Tactic:
simp only [fastAdmitsAux] at h2
State after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ → u ∉ binders
⊢ toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (def_ a✝¹ a✝))

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

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

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
⊢ 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))
Tactic:
simp
State after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
⊢ 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

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

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

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

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
x : VarName
a1 : x ∈ xs
⊢ x ∈ binders ↔ (if v = x then u else x) ∈ binders
Tactic:
by_cases c1 : v = x
State after:
case pos
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
x : VarName
a1 : x ∈ xs
c1 : v = x
⊢ x ∈ binders ↔ (if v = x then u else x) ∈ binders

case neg
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
⊢ x ∈ binders ↔ (if v = x then u else x) ∈ binders

State before:
case pos
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
x : VarName
a1 : x ∈ xs
c1 : v = x
⊢ x ∈ binders ↔ (if v = x then u else x) ∈ binders
Tactic:
subst c1
State after:
case pos
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
a1 : v ∈ xs
⊢ v ∈ binders ↔ (if v = v then u else v) ∈ binders

State before:
case pos
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
a1 : v ∈ xs
⊢ v ∈ binders ↔ (if v = v then u else v) ∈ binders
Tactic:
simp
State after:
case pos
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
a1 : v ∈ xs
⊢ v ∈ binders ↔ u ∈ binders

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

State before:
case neg
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
⊢ x ∈ binders ↔ (if v = x then u else x) ∈ binders
Tactic:
simp only [if_neg c1]
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
⊢ 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))
Tactic:
simp
State after:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
⊢ (x ∈ binders ↔ (if v = x then u else x) ∈ binders) ∧ (y ∈ binders ↔ (if v = y then u else y) ∈ binders)

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

case right
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
⊢ y ∈ binders ↔ (if v = y then u else y) ∈ binders

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
⊢ y ∈ binders ↔ (if v = y then u else y) ∈ binders
Tactic:
case left | right =>
  split_ifs
  case pos c1 =>
    subst c1
    tauto
  case neg c1 =>
    rfl
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
⊢ y ∈ binders ↔ (if v = y then u else y) ∈ binders
Tactic:
split_ifs
State after:
case pos
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
h✝ : v = y
⊢ y ∈ binders ↔ u ∈ binders

case neg
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
h✝ : ¬v = y
⊢ y ∈ binders ↔ y ∈ binders

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
c1 : v = y
⊢ y ∈ binders ↔ u ∈ binders
Tactic:
case pos c1 =>
  subst c1
  tauto
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
c1 : ¬v = y
⊢ y ∈ binders ↔ y ∈ binders
Tactic:
case neg c1 =>
  rfl
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
c1 : v = y
⊢ y ∈ binders ↔ u ∈ binders
Tactic:
subst c1
State after:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = v → u ∉ binders
⊢ v ∈ binders ↔ u ∈ binders

State before:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = v → u ∉ binders
⊢ v ∈ binders ↔ u ∈ binders
Tactic:
tauto
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
c1 : ¬v = y
⊢ y ∈ binders ↔ y ∈ binders
Tactic:
rfl
State after:
no goals

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

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

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

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

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

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

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

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

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

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

case h2
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      fastAdmitsAux v u binders phi → toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ fastAdmitsAux v u (binders ∪ {x}) phi

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

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

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