Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree (FOL/NV/Sub/Var/One/Rec/ReplaceFree.lean)

State before:
F : Formula
v t : VarName
h1 : ¬v = t
⊢ ¬isFreeIn v (fastReplaceFree v t F)
Tactic:
induction F
State after:
case pred_const_
v t : VarName
h1 : ¬v = t
a✝¹ : PredName
a✝ : List VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (pred_const_ a✝¹ a✝))

case pred_var_
v t : VarName
h1 : ¬v = t
a✝¹ : PredName
a✝ : List VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (pred_var_ a✝¹ a✝))

case eq_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (eq_ a✝¹ a✝))

case true_
v t : VarName
h1 : ¬v = t
⊢ ¬isFreeIn v (fastReplaceFree v t true_)

case false_
v t : VarName
h1 : ¬v = t
⊢ ¬isFreeIn v (fastReplaceFree v t false_)

case not_
v t : VarName
h1 : ¬v = t
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t a✝.not_)

case imp_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.imp_ a✝))

case and_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.and_ a✝))

case or_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.or_ a✝))

case iff_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.iff_ a✝))

case forall_
v t : VarName
h1 : ¬v = t
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (forall_ a✝¹ a✝))

case exists_
v t : VarName
h1 : ¬v = t
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (exists_ a✝¹ a✝))

case def_
v t : VarName
h1 : ¬v = t
a✝¹ : DefName
a✝ : List VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (def_ a✝¹ a✝))

State before:
case pred_const_
v t : VarName
h1 : ¬v = t
a✝¹ : PredName
a✝ : List VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (pred_const_ a✝¹ a✝))

case pred_var_
v t : VarName
h1 : ¬v = t
a✝¹ : PredName
a✝ : List VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (pred_var_ a✝¹ a✝))

case eq_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (eq_ a✝¹ a✝))

case true_
v t : VarName
h1 : ¬v = t
⊢ ¬isFreeIn v (fastReplaceFree v t true_)

case false_
v t : VarName
h1 : ¬v = t
⊢ ¬isFreeIn v (fastReplaceFree v t false_)

case not_
v t : VarName
h1 : ¬v = t
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t a✝.not_)

case imp_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.imp_ a✝))

case and_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.and_ a✝))

case or_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.or_ a✝))

case iff_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.iff_ a✝))

case forall_
v t : VarName
h1 : ¬v = t
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (forall_ a✝¹ a✝))

case exists_
v t : VarName
h1 : ¬v = t
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (exists_ a✝¹ a✝))

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

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

case eq_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : VarName
⊢ ¬((v = if v = a✝¹ then t else a✝¹) ∨ v = if v = a✝ then t else a✝)

case true_
v t : VarName
h1 : ¬v = t
⊢ ¬False

case false_
v t : VarName
h1 : ¬v = t
⊢ ¬False

case not_
v t : VarName
h1 : ¬v = t
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t a✝)

case imp_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬(isFreeIn v (fastReplaceFree v t a✝¹) ∨ isFreeIn v (fastReplaceFree v t a✝))

case and_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬(isFreeIn v (fastReplaceFree v t a✝¹) ∨ isFreeIn v (fastReplaceFree v t a✝))

case or_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬(isFreeIn v (fastReplaceFree v t a✝¹) ∨ isFreeIn v (fastReplaceFree v t a✝))

case iff_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬(isFreeIn v (fastReplaceFree v t a✝¹) ∨ isFreeIn v (fastReplaceFree v t a✝))

case forall_
v t : VarName
h1 : ¬v = t
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (forall_ a✝¹ a✝))

case exists_
v t : VarName
h1 : ¬v = t
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (exists_ a✝¹ a✝))

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

State before:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ v ∉ List.map (fun x => if v = x then t else x) xs
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  intro x
  split_ifs <;> tauto
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
x y : VarName
⊢ ¬((v = if v = x then t else x) ∨ v = if v = y then t else y)
Tactic:
case eq_ x y =>
  split_ifs <;> tauto
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
⊢ ¬False
Tactic:
case true_ | false_ =>
  simp
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (fastReplaceFree v t phi)
Tactic:
case not_ phi phi_ih =>
  exact phi_ih
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
phi psi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
psi_ih : ¬isFreeIn v (fastReplaceFree v t psi)
⊢ ¬(isFreeIn v (fastReplaceFree v t phi) ∨ isFreeIn v (fastReplaceFree v t 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 =>
  tauto
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (fastReplaceFree v t (exists_ x phi))
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [fastReplaceFree]
  split_ifs
  case pos c1 =>
    simp only [isFreeIn]
    simp
    intro a1
    contradiction
  case neg c1 =>
    simp only [isFreeIn]
    simp
    intro _
    exact phi_ih
State after:
no goals

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

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

State before:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ v ∉ List.map (fun x => if v = x then t else x) xs
Tactic:
simp
State after:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ ∀ x ∈ xs, ¬(if v = x then t else x) = v

State before:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ ∀ x ∈ xs, ¬(if v = x then t else x) = v
Tactic:
intro x
State after:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
x : VarName
⊢ x ∈ xs → ¬(if v = x then t else x) = v

State before:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
x : VarName
⊢ x ∈ xs → ¬(if v = x then t else x) = v
Tactic:
split_ifs <;> tauto
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
x y : VarName
⊢ ¬((v = if v = x then t else x) ∨ v = if v = y then t else y)
Tactic:
split_ifs <;> tauto
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
⊢ ¬False
Tactic:
simp
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (fastReplaceFree v t phi)
Tactic:
exact phi_ih
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
phi psi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
psi_ih : ¬isFreeIn v (fastReplaceFree v t psi)
⊢ ¬(isFreeIn v (fastReplaceFree v t phi) ∨ isFreeIn v (fastReplaceFree v t psi))
Tactic:
tauto
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (fastReplaceFree v t (exists_ x phi))
Tactic:
simp only [fastReplaceFree]
State after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
split_ifs
State after:
case pos
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
h✝ : v = x
⊢ ¬isFreeIn v (exists_ x phi)

case neg
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
h✝ : ¬v = x
⊢ ¬isFreeIn v (exists_ x (fastReplaceFree v t phi))

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
case pos c1 =>
  simp only [isFreeIn]
  simp
  intro a1
  contradiction
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x (fastReplaceFree v t phi))
Tactic:
case neg c1 =>
  simp only [isFreeIn]
  simp
  intro _
  exact phi_ih
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
simp only [isFreeIn]
State after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬(¬v = x ∧ isFreeIn v phi)

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬(¬v = x ∧ isFreeIn v phi)
Tactic:
simp
State after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬v = x → ¬isFreeIn v phi

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬v = x → ¬isFreeIn v phi
Tactic:
intro a1
State after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
a1 : ¬v = x
⊢ ¬isFreeIn v phi

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
a1 : ¬v = x
⊢ ¬isFreeIn v phi
Tactic:
contradiction
State after:
no goals

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x (fastReplaceFree v t phi))
Tactic:
simp only [isFreeIn]
State after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬(¬v = x ∧ isFreeIn v (fastReplaceFree v t phi))

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬(¬v = x ∧ isFreeIn v (fastReplaceFree v t phi))
Tactic:
simp
State after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬v = x → ¬isFreeIn v (fastReplaceFree v t phi)

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬v = x → ¬isFreeIn v (fastReplaceFree v t phi)
Tactic:
intro _
State after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 a✝ : ¬v = x
⊢ ¬isFreeIn v (fastReplaceFree v t phi)

State before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 a✝ : ¬v = x
⊢ ¬isFreeIn v (fastReplaceFree v t phi)
Tactic:
exact phi_ih
State after:
no goals