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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬occursIn t a✝ → fastReplaceFree t v (fastReplaceFree v t a✝) = a✝
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ fastReplaceFree t v (if v = a✝¹ then forall_ a✝¹ a✝ else forall_ a✝¹ (fastReplaceFree v t a✝)) = forall_ a✝¹ a✝

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬occursIn t a✝ → fastReplaceFree t v (fastReplaceFree v t a✝) = a✝
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ fastReplaceFree t v (if v = a✝¹ then exists_ a✝¹ a✝ else exists_ a✝¹ (fastReplaceFree v t a✝)) = exists_ a✝¹ a✝

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

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

State before:
v t : VarName
phi psi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
psi_ih : ¬occursIn t psi → fastReplaceFree t v (fastReplaceFree v t psi) = psi
h1 : ¬(occursIn t phi ∨ occursIn t psi)
⊢ (fastReplaceFree t v (fastReplaceFree v t phi)).iff_ (fastReplaceFree t v (fastReplaceFree v t psi)) = phi.iff_ 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 =>
    congr! <;> tauto
State after:
no goals

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : ¬(t = x ∨ occursIn t phi)
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    split_ifs
    case pos c1 =>
      simp only [fastReplaceFree]
      simp only [if_neg h1_left]
      congr!
      apply not_free_in_fastReplaceFree_self
      contrapose! h1_right
      exact isFreeIn_imp_occursIn t phi h1_right
    case neg c1 =>
      simp only [fastReplaceFree]
      simp only [if_neg h1_left]
      congr!
      exact phi_ih h1_right
State after:
no goals

State before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : ¬occursIn t (def_ a✝¹ a✝)
⊢ fastReplaceFree t v (fastReplaceFree v t (def_ a✝¹ a✝)) = def_ a✝¹ a✝
Tactic:
simp only [occursIn] at h1
State after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : t ∉ a✝
⊢ fastReplaceFree t v (fastReplaceFree v t (def_ a✝¹ a✝)) = def_ a✝¹ a✝

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

State before:
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ def_ X (List.map (fun x => if t = x then v else x) (List.map (fun x => if v = x then t else x) xs)) = def_ X xs
Tactic:
congr!
State after:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ List.map (fun x => if t = x then v else x) (List.map (fun x => if v = x then t else x) xs) = xs

State before:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ List.map (fun x => if t = x then v else x) (List.map (fun x => if v = x then t else x) xs) = xs
Tactic:
simp
State after:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ List.map ((fun x => if t = x then v else x) ∘ fun x => if v = x then t else x) xs = xs

State before:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ List.map ((fun x => if t = x then v else x) ∘ fun x => if v = x then t else x) xs = xs
Tactic:
simp only [List.map_eq_self_iff]
State after:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ ∀ x ∈ xs, ((fun x => if t = x then v else x) ∘ fun x => if v = x then t else x) x = x

State before:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ ∀ x ∈ xs, ((fun x => if t = x then v else x) ∘ fun x => if v = x then t else x) x = x
Tactic:
simp
State after:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ ∀ x ∈ xs, (if t = if v = x then t else x then v else if v = x then t else x) = x

State before:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ ∀ x ∈ xs, (if t = if v = x then t else x then v else if v = x then t else x) = x
Tactic:
intro x a1
State after:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
⊢ (if t = if v = x then t else x then v else if v = x then t else x) = x

State before:
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
⊢ (if t = if v = x then t else x then v else if v = x then t else x) = x
Tactic:
by_cases c1 : v = x
State after:
case pos
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : v = x
⊢ (if t = if v = x then t else x then v else if v = x then t else x) = x

case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
⊢ (if t = if v = x then t else x then v else if v = x then t else x) = x

State before:
case pos
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : v = x
⊢ (if t = if v = x then t else x then v else if v = x then t else x) = x
Tactic:
simp only [if_pos c1]
State after:
case pos
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : v = x
⊢ (if True then v else t) = x

State before:
case pos
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : v = x
⊢ (if True then v else t) = x
Tactic:
simp
State after:
case pos
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : v = x
⊢ v = x

State before:
case pos
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : v = x
⊢ v = x
Tactic:
exact c1
State after:
no goals

State before:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
⊢ (if t = if v = x then t else x then v else if v = x then t else x) = x
Tactic:
simp only [if_neg c1]
State after:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
⊢ (if t = x then v else x) = x

State before:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
⊢ (if t = x then v else x) = x
Tactic:
simp
State after:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
⊢ t = x → v = x

State before:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
⊢ t = x → v = x
Tactic:
intro a2
State after:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
a2 : t = x
⊢ v = x

State before:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
a2 : t = x
⊢ v = x
Tactic:
subst a2
State after:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
a1 : t ∈ xs
c1 : ¬v = t
⊢ v = t

State before:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
a1 : t ∈ xs
c1 : ¬v = t
⊢ v = t
Tactic:
contradiction
State after:
no goals

State before:
v t x y : VarName
h1 : ¬(t = x ∨ t = y)
⊢ eq_ (if t = if v = x then t else x then v else if v = x then t else x)
      (if t = if v = y then t else y then v else if v = y then t else y) =
    eq_ x y
Tactic:
congr!
State after:
case h.e'_1
v t x y : VarName
h1 : ¬(t = x ∨ t = y)
⊢ (if t = if v = x then t else x then v else if v = x then t else x) = x

case h.e'_2
v t x y : VarName
h1 : ¬(t = x ∨ t = y)
⊢ (if t = if v = y then t else y then v else if v = y then t else y) = y

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

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

State before:
v t : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : ¬occursIn t phi
⊢ (fastReplaceFree t v (fastReplaceFree v t phi)).not_ = phi.not_
Tactic:
congr!
State after:
case h.e'_1
v t : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : ¬occursIn t phi
⊢ fastReplaceFree t v (fastReplaceFree v t phi) = phi

State before:
case h.e'_1
v t : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : ¬occursIn t phi
⊢ fastReplaceFree t v (fastReplaceFree v t phi) = phi
Tactic:
exact phi_ih h1
State after:
no goals

State before:
v t : VarName
phi psi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
psi_ih : ¬occursIn t psi → fastReplaceFree t v (fastReplaceFree v t psi) = psi
h1 : ¬(occursIn t phi ∨ occursIn t psi)
⊢ (fastReplaceFree t v (fastReplaceFree v t phi)).iff_ (fastReplaceFree t v (fastReplaceFree v t psi)) = phi.iff_ psi
Tactic:
congr! <;> tauto
State after:
no goals

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : ¬(t = x ∨ occursIn t phi)
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi
Tactic:
push_neg at h1
State after:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : t ≠ x ∧ ¬occursIn t phi
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : t ≠ x ∧ ¬occursIn t phi
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi
Tactic:
cases h1
State after:
case intro
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
left✝ : t ≠ x
right✝ : ¬occursIn t phi
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi
Tactic:
case intro h1_left h1_right =>
  split_ifs
  case pos c1 =>
    simp only [fastReplaceFree]
    simp only [if_neg h1_left]
    congr!
    apply not_free_in_fastReplaceFree_self
    contrapose! h1_right
    exact isFreeIn_imp_occursIn t phi h1_right
  case neg c1 =>
    simp only [fastReplaceFree]
    simp only [if_neg h1_left]
    congr!
    exact phi_ih h1_right
State after:
no goals

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi
Tactic:
split_ifs
State after:
case pos
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
h✝ : v = x
⊢ fastReplaceFree t v (exists_ x phi) = exists_ x phi

case neg
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
h✝ : ¬v = x
⊢ fastReplaceFree t v (exists_ x (fastReplaceFree v t phi)) = exists_ x phi

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ fastReplaceFree t v (exists_ x phi) = exists_ x phi
Tactic:
case pos c1 =>
  simp only [fastReplaceFree]
  simp only [if_neg h1_left]
  congr!
  apply not_free_in_fastReplaceFree_self
  contrapose! h1_right
  exact isFreeIn_imp_occursIn t phi h1_right
State after:
no goals

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ fastReplaceFree t v (exists_ x (fastReplaceFree v t phi)) = exists_ x phi
Tactic:
case neg c1 =>
  simp only [fastReplaceFree]
  simp only [if_neg h1_left]
  congr!
  exact phi_ih h1_right
State after:
no goals

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ fastReplaceFree t v (exists_ x phi) = exists_ x phi
Tactic:
simp only [fastReplaceFree]
State after:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ (if t = x then exists_ x phi else exists_ x (fastReplaceFree t v phi)) = exists_ x phi

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ (if t = x then exists_ x phi else exists_ x (fastReplaceFree t v phi)) = exists_ x phi
Tactic:
simp only [if_neg h1_left]
State after:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ exists_ x (fastReplaceFree t v phi) = exists_ x phi

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ exists_ x (fastReplaceFree t v phi) = exists_ x phi
Tactic:
congr!
State after:
case h.e'_2
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ fastReplaceFree t v phi = phi

State before:
case h.e'_2
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ fastReplaceFree t v phi = phi
Tactic:
apply not_free_in_fastReplaceFree_self
State after:
case h.e'_2.h1
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ ¬isFreeIn t phi

State before:
case h.e'_2.h1
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : v = x
⊢ ¬isFreeIn t phi
Tactic:
contrapose! h1_right
State after:
case h.e'_2.h1
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
c1 : v = x
h1_right : isFreeIn t phi
⊢ occursIn t phi

State before:
case h.e'_2.h1
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
c1 : v = x
h1_right : isFreeIn t phi
⊢ occursIn t phi
Tactic:
exact isFreeIn_imp_occursIn t phi h1_right
State after:
no goals

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ fastReplaceFree t v (exists_ x (fastReplaceFree v t phi)) = exists_ x phi
Tactic:
simp only [fastReplaceFree]
State after:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ (if t = x then exists_ x (fastReplaceFree v t phi) else exists_ x (fastReplaceFree t v (fastReplaceFree v t phi))) =
    exists_ x phi

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ (if t = x then exists_ x (fastReplaceFree v t phi) else exists_ x (fastReplaceFree t v (fastReplaceFree v t phi))) =
    exists_ x phi
Tactic:
simp only [if_neg h1_left]
State after:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ exists_ x (fastReplaceFree t v (fastReplaceFree v t phi)) = exists_ x phi

State before:
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ exists_ x (fastReplaceFree t v (fastReplaceFree v t phi)) = exists_ x phi
Tactic:
congr!
State after:
case h.e'_2
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ fastReplaceFree t v (fastReplaceFree v t phi) = phi

State before:
case h.e'_2
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ fastReplaceFree t v (fastReplaceFree v t phi) = phi
Tactic:
exact phi_ih h1_right
State after:
no goals