internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
apply Finset.image_subset_image
Proof state after:
case s2.h
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ phi.freeVarSet \ {x} ⊆ phi.freeVarSet

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s2.h
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ phi.freeVarSet \ {x} ⊆ phi.freeVarSet

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
have s3 : x' ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
Proof state after:
case s3
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s3
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
apply Finset.not_mem_mono s2 s1
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
calc
  Finset.image (Function.updateITE σ x x') (freeVarSet phi) \ {x'}
= Finset.image (Function.updateITE σ x x') (freeVarSet phi \ {x}) \ {x'} :=
    by
    {
      apply Finset.image_sdiff_singleton phi.freeVarSet x x' (Function.updateITE σ x x')
      simp only [Function.updateITE]
      simp
    }
_ = Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) \ {x'} :=
    by simp only [Finset.image_congr_update_ite phi.freeVarSet x x' x]
_ = Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) :=
    by exact Finset.sdiff_singleton_eq_self s3
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x') (phi.freeVarSet \ {x}) \ {x'}
Tactic:
apply Finset.image_sdiff_singleton phi.freeVarSet x x' (Function.updateITE σ x x')
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Function.updateITE σ x x' x = x'
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Function.updateITE σ x x' x = x'
Tactic:
simp only [Function.updateITE]
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ (if True then x' else σ x) = x'
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ (if True then x' else σ x) = x'
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x') (phi.freeVarSet \ {x}) \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x'}
Tactic:
simp only [Finset.image_congr_update_ite phi.freeVarSet x x' x]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
exact Finset.sdiff_singleton_eq_self s3
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp at c1
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
have s1 : Finset.image (Function.updateITE σ x x) (freeVarSet phi) \ {x} = Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) \ {x}
Proof state after:
case s1
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s1
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
apply Finset.image_sdiff_singleton
Proof state after:
case s1.h1
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ Function.updateITE σ x x x = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s1.h1
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ Function.updateITE σ x x x = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp only [Function.updateITE]
Proof state after:
case s1.h1
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ (if True then x else σ x) = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case s1.h1
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ (if True then x else σ x) = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
simp only [s1]
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
clear s1
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
have s2 : x ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
Proof state after:
case s2
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s2 : x ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})