internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.not_free_in_fastReplaceFree_self
Proof state before:
v t x : VarName
phi : Formula
phi_ih : ¬isFreeIn v phi → fastReplaceFree v t phi = phi
h1 : ¬(¬v = x ∧ isFreeIn v phi)
⊢ ¬v = x → fastReplaceFree v t phi = phi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastReplaceFree t v (fastReplaceFree v t F) = F
Tactic:
induction F
Proof 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✝
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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✝
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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]
Proof 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✝
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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!
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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]
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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]
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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]
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
a1 : t ∈ xs
c1 : ¬v = t
⊢ v = t
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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!
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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!
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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]
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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]
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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!
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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]
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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]
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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!
Proof 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
Theorem: FOL.NV.Sub.Var.One.Rec.fastReplaceFree_inverse
Proof 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
Proof state after:
no goals