Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub (FOL/NV/Sub/Var/One/Ind/Sub.lean)

State before:
F F' : Formula
v u : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders F
h2 : Rec.fastReplaceFree v u F = F'
⊢ IsSub F v u F'
Tactic:
subst h2
State after:
F : Formula
v u : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders F
⊢ IsSub F v u (Rec.fastReplaceFree v u F)

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

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (pred_var_ a✝¹ a✝)
⊢ IsSub (pred_var_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (pred_var_ a✝¹ a✝))

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (eq_ a✝¹ a✝)
⊢ IsSub (eq_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (eq_ a✝¹ a✝))

case true_
v u : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders true_
⊢ IsSub true_ v u (Rec.fastReplaceFree v u true_)

case false_
v u : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders false_
⊢ IsSub false_ v u (Rec.fastReplaceFree v u false_)

case not_
v u : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders a✝.not_
⊢ IsSub a✝.not_ v u (Rec.fastReplaceFree v u a✝.not_)

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝¹ → IsSub a✝¹ v u (Rec.fastReplaceFree v u a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (a✝¹.imp_ a✝)
⊢ IsSub (a✝¹.imp_ a✝) v u (Rec.fastReplaceFree v u (a✝¹.imp_ a✝))

case and_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝¹ → IsSub a✝¹ v u (Rec.fastReplaceFree v u a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (a✝¹.and_ a✝)
⊢ IsSub (a✝¹.and_ a✝) v u (Rec.fastReplaceFree v u (a✝¹.and_ a✝))

case or_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝¹ → IsSub a✝¹ v u (Rec.fastReplaceFree v u a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (a✝¹.or_ a✝)
⊢ IsSub (a✝¹.or_ a✝) v u (Rec.fastReplaceFree v u (a✝¹.or_ a✝))

case iff_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝¹ → IsSub a✝¹ v u (Rec.fastReplaceFree v u a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (a✝¹.iff_ a✝)
⊢ IsSub (a✝¹.iff_ a✝) v u (Rec.fastReplaceFree v u (a✝¹.iff_ a✝))

case forall_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (forall_ a✝¹ a✝)
⊢ IsSub (forall_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (forall_ a✝¹ a✝))

case exists_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (exists_ a✝¹ a✝)
⊢ IsSub (exists_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (exists_ a✝¹ a✝))

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (def_ a✝¹ a✝)
⊢ IsSub (def_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (def_ a✝¹ a✝))

State before:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (pred_const_ a✝¹ a✝)
⊢ IsSub (pred_const_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (pred_const_ a✝¹ a✝))

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (pred_var_ a✝¹ a✝)
⊢ IsSub (pred_var_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (pred_var_ a✝¹ a✝))

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (eq_ a✝¹ a✝)
⊢ IsSub (eq_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (eq_ a✝¹ a✝))

case true_
v u : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders true_
⊢ IsSub true_ v u (Rec.fastReplaceFree v u true_)

case false_
v u : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders false_
⊢ IsSub false_ v u (Rec.fastReplaceFree v u false_)

case not_
v u : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders a✝.not_
⊢ IsSub a✝.not_ v u (Rec.fastReplaceFree v u a✝.not_)

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝¹ → IsSub a✝¹ v u (Rec.fastReplaceFree v u a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (a✝¹.imp_ a✝)
⊢ IsSub (a✝¹.imp_ a✝) v u (Rec.fastReplaceFree v u (a✝¹.imp_ a✝))

case and_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝¹ → IsSub a✝¹ v u (Rec.fastReplaceFree v u a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (a✝¹.and_ a✝)
⊢ IsSub (a✝¹.and_ a✝) v u (Rec.fastReplaceFree v u (a✝¹.and_ a✝))

case or_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝¹ → IsSub a✝¹ v u (Rec.fastReplaceFree v u a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (a✝¹.or_ a✝)
⊢ IsSub (a✝¹.or_ a✝) v u (Rec.fastReplaceFree v u (a✝¹.or_ a✝))

case iff_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝¹ → IsSub a✝¹ v u (Rec.fastReplaceFree v u a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (a✝¹.iff_ a✝)
⊢ IsSub (a✝¹.iff_ a✝) v u (Rec.fastReplaceFree v u (a✝¹.iff_ a✝))

case forall_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (forall_ a✝¹ a✝)
⊢ IsSub (forall_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (forall_ a✝¹ a✝))

case exists_
v u a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (exists_ a✝¹ a✝)
⊢ IsSub (exists_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (exists_ a✝¹ a✝))

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (def_ a✝¹ a✝)
⊢ IsSub (def_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (def_ a✝¹ a✝))
Tactic:
all_goals
  simp only [Rec.fastAdmitsAux] at h1
  simp only [Rec.fastReplaceFree]
State after:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ → u ∉ binders
⊢ IsSub (pred_const_ a✝¹ a✝) v u (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 ∈ a✝ → u ∉ binders
⊢ IsSub (pred_var_ a✝¹ a✝) v u (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 = a✝¹ ∨ v = a✝ → u ∉ binders
⊢ IsSub (eq_ a✝¹ a✝) v u (eq_ (if v = a✝¹ then u else a✝¹) (if v = a✝ then u else a✝))

case true_
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub true_ v u true_

case false_
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub false_ v u false_

case not_
v u : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders a✝ → IsSub a✝ v u (Rec.fastReplaceFree v u a✝)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders a✝
⊢ IsSub a✝.not_ v u (Rec.fastReplaceFree v u a✝).not_

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

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

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

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

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

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

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

State before:
v u : VarName
X : PredName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (pred_var_ X xs) v u (pred_var_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
case pred_const_ X xs | pred_var_ X xs =>
  first | apply IsSub.pred_const_ | apply IsSub.pred_var_
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v = x ∨ v = y → u ∉ binders
⊢ IsSub (eq_ x y) v u (eq_ (if v = x then u else x) (if v = y then u else y))
Tactic:
case eq_ x y =>
  apply IsSub.eq_
State after:
no goals

State before:
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub false_ v u false_
Tactic:
case true_ | false_ =>
  first | apply IsSub.true_ | apply IsSub.false_
State after:
no goals

State before:
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders phi
⊢ IsSub phi.not_ v u (Rec.fastReplaceFree v u phi).not_
Tactic:
case not_ phi phi_ih =>
  apply IsSub.not_
  exact phi_ih binders h1
State after:
no goals

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (def_ X xs) v u (def_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
case def_ X xs =>
  apply IsSub.def_
State after:
no goals

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

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

State before:
v u : VarName
X : PredName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (pred_var_ X xs) v u (pred_var_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
first | apply IsSub.pred_const_ | apply IsSub.pred_var_
State after:
no goals

State before:
v u : VarName
X : PredName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (pred_const_ X xs) v u (pred_const_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
apply IsSub.pred_const_
State after:
no goals

State before:
v u : VarName
X : PredName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (pred_var_ X xs) v u (pred_var_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
apply IsSub.pred_var_
State after:
no goals

State before:
v u x y : VarName
binders : Finset VarName
h1 : v = x ∨ v = y → u ∉ binders
⊢ IsSub (eq_ x y) v u (eq_ (if v = x then u else x) (if v = y then u else y))
Tactic:
apply IsSub.eq_
State after:
no goals

State before:
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub false_ v u false_
Tactic:
first | apply IsSub.true_ | apply IsSub.false_
State after:
no goals

State before:
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub true_ v u true_
Tactic:
apply IsSub.true_
State after:
no goals

State before:
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub false_ v u false_
Tactic:
apply IsSub.false_
State after:
no goals

State before:
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders phi
⊢ IsSub phi.not_ v u (Rec.fastReplaceFree v u phi).not_
Tactic:
apply IsSub.not_
State after:
case a
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

State before:
case a
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
exact phi_ih binders h1
State after:
no goals

State before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders phi ∧ Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.iff_ psi) v u ((Rec.fastReplaceFree v u phi).iff_ (Rec.fastReplaceFree v u psi))
Tactic:
cases h1
State after:
case intro
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
left✝ : Rec.fastAdmitsAux v u binders phi
right✝ : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.iff_ psi) v u ((Rec.fastReplaceFree v u phi).iff_ (Rec.fastReplaceFree v u psi))

State before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.iff_ psi) v u ((Rec.fastReplaceFree v u phi).iff_ (Rec.fastReplaceFree v u psi))
Tactic:
first | apply IsSub.imp_ | apply IsSub.and_ | apply IsSub.or_ | apply IsSub.iff_
State after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)

State before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.imp_ psi) v u ((Rec.fastReplaceFree v u phi).imp_ (Rec.fastReplaceFree v u psi))
Tactic:
apply IsSub.imp_
State after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)

State before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.and_ psi) v u ((Rec.fastReplaceFree v u phi).and_ (Rec.fastReplaceFree v u psi))
Tactic:
apply IsSub.and_
State after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)

State before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.or_ psi) v u ((Rec.fastReplaceFree v u phi).or_ (Rec.fastReplaceFree v u psi))
Tactic:
apply IsSub.or_
State after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)

State before:
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub (phi.iff_ psi) v u ((Rec.fastReplaceFree v u phi).iff_ (Rec.fastReplaceFree v u psi))
Tactic:
apply IsSub.iff_
State after:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)

State before:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
exact phi_ih binders h1_left
State after:
no goals

State before:
case a
v u : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
psi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders psi → IsSub psi v u (Rec.fastReplaceFree v u psi)
binders : Finset VarName
h1_left : Rec.fastAdmitsAux v u binders phi
h1_right : Rec.fastAdmitsAux v u binders psi
⊢ IsSub psi v u (Rec.fastReplaceFree v u psi)
Tactic:
exact psi_ih binders h1_right
State after:
no goals

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x ∨ Rec.fastAdmitsAux v u (binders ∪ {x}) phi
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
cases h1
State after:
case inl
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h✝ : v = x
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))

case inr
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h✝ : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
case inl h1 =>
  split_ifs
  case pos c1 | neg c1 =>
    first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
    subst h1
    simp only [isFreeIn]
    simp
State after:
no goals

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
split_ifs
State after:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 h✝ : v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
h✝ : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
c1 : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
case pos c1 | neg c1 =>
  first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
  subst h1
  simp only [isFreeIn]
  simp
State after:
no goals

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
c1 : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
State after:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x phi)

State before:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
subst h1
State after:
case a
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
c1 : ¬v = v
⊢ ¬isFreeIn v (exists_ v phi)

State before:
case a
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
c1 : ¬v = v
⊢ ¬isFreeIn v (exists_ v phi)
Tactic:
simp only [isFreeIn]
State after:
case a
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
c1 : ¬v = v
⊢ ¬(¬True ∧ isFreeIn v phi)

State before:
case a
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
c1 : ¬v = v
⊢ ¬(¬True ∧ isFreeIn v phi)
Tactic:
simp
State after:
no goals

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
c1 : ¬v = x
⊢ IsSub (forall_ x phi) v u (forall_ x phi)
Tactic:
apply IsSub.forall_not_free_in
State after:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
c1 : ¬v = x
⊢ ¬isFreeIn v (forall_ x phi)

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
c1 : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
apply IsSub.exists_not_free_in
State after:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : v = x
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x phi)

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
split_ifs
State after:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
h✝ : v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
h✝ : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
case pos c1 =>
  first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
  simp only [isFreeIn]
  tauto
State after:
no goals

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
State after:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ ¬isFreeIn v (exists_ x phi)

State before:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
simp only [isFreeIn]
State after:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ ¬(¬v = x ∧ isFreeIn v phi)

State before:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ ¬(¬v = x ∧ isFreeIn v phi)
Tactic:
tauto
State after:
no goals

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ IsSub (forall_ x phi) v u (forall_ x phi)
Tactic:
apply IsSub.forall_not_free_in
State after:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ ¬isFreeIn v (forall_ x phi)

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
apply IsSub.exists_not_free_in
State after:
case a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ ¬isFreeIn v (exists_ x phi)

State before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
by_cases c2 : isFreeIn v phi
State after:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))

State before:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
first | apply IsSub.forall_free_in | apply IsSub.exists_free_in
State after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v (exists_ x phi)

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

State before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v (exists_ x phi)

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
simp only [isFreeIn]
State after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬v = x ∧ isFreeIn v phi

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

State before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬v = x ∧ isFreeIn v phi

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
constructor
State after:
case pos.a.left
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬v = x

case pos.a.right
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v phi

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

State before:
case pos.a.right
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v phi

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
. exact c2
State after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

State before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
. have s1 : ¬ u ∈ binders ∪ {x}
  exact Rec.fastAdmitsAux_isFreeIn phi v u (binders ∪ {x}) h1 c2
  simp at s1
  tauto
State after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

State before:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub (forall_ x phi) v u (forall_ x (Rec.fastReplaceFree v u phi))
Tactic:
apply IsSub.forall_free_in
State after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v (forall_ x phi)

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

State before:
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
apply IsSub.exists_free_in
State after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v (exists_ x phi)

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)

State before:
case pos.a.left
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬v = x
Tactic:
exact c1
State after:
no goals

State before:
case pos.a.right
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ isFreeIn v phi
Tactic:
exact c2
State after:
no goals

State before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u
Tactic:
have s1 : ¬ u ∈ binders ∪ {x}
State after:
case s1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ u ∉ binders ∪ {x}

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∪ {x}
⊢ ¬x = u

State before:
case s1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ u ∉ binders ∪ {x}

case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∪ {x}
⊢ ¬x = u
Tactic:
exact Rec.fastAdmitsAux_isFreeIn phi v u (binders ∪ {x}) h1 c2
State after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∪ {x}
⊢ ¬x = u

State before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∪ {x}
⊢ ¬x = u
Tactic:
simp at s1
State after:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∧ ¬u = x
⊢ ¬x = u

State before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
s1 : u ∉ binders ∧ ¬u = x
⊢ ¬x = u
Tactic:
tauto
State after:
no goals

State before:
case pos.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
Tactic:
exact phi_ih (binders ∪ {x}) h1
State after:
no goals

State before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
have s1 : Rec.fastReplaceFree v u phi = phi
State after:
case s1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
⊢ Rec.fastReplaceFree v u phi = phi

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))

State before:
case s1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
⊢ Rec.fastReplaceFree v u phi = phi

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
exact Rec.not_free_in_fastReplaceFree_self phi v u c2
State after:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))

State before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x (Rec.fastReplaceFree v u phi))
Tactic:
simp only [s1]
State after:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x phi)

State before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
first | apply IsSub.forall_not_free_in | apply IsSub.exists_not_free_in
State after:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬isFreeIn v (exists_ x phi)

State before:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
simp only [isFreeIn]
State after:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬(¬v = x ∧ isFreeIn v phi)

State before:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬(¬v = x ∧ isFreeIn v phi)
Tactic:
tauto
State after:
no goals

State before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (forall_ x phi) v u (forall_ x phi)
Tactic:
apply IsSub.forall_not_free_in
State after:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬isFreeIn v (forall_ x phi)

State before:
case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
Tactic:
apply IsSub.exists_not_free_in
State after:
case neg.a
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
c2 : ¬isFreeIn v phi
s1 : Rec.fastReplaceFree v u phi = phi
⊢ ¬isFreeIn v (exists_ x phi)

State before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (def_ X xs) v u (def_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
apply IsSub.def_
State after:
no goals