internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
σ : VarName → VarName
c : Char
F : Formula
⊢ (sub σ c F).freeVarSet = Finset.image σ F.freeVarSet
Tactic:
induction F generalizing σ
Proof state after:
case pred_const_
c : Char
a✝¹ : PredName
a✝ : List VarName
σ : VarName → VarName
⊢ (sub σ c (pred_const_ a✝¹ a✝)).freeVarSet = Finset.image σ (pred_const_ a✝¹ a✝).freeVarSet

case pred_var_
c : Char
a✝¹ : PredName
a✝ : List VarName
σ : VarName → VarName
⊢ (sub σ c (pred_var_ a✝¹ a✝)).freeVarSet = Finset.image σ (pred_var_ a✝¹ a✝).freeVarSet

case eq_
c : Char
a✝¹ a✝ : VarName
σ : VarName → VarName
⊢ (sub σ c (eq_ a✝¹ a✝)).freeVarSet = Finset.image σ (eq_ a✝¹ a✝).freeVarSet

case true_
c : Char
σ : VarName → VarName
⊢ (sub σ c true_).freeVarSet = Finset.image σ true_.freeVarSet

case false_
c : Char
σ : VarName → VarName
⊢ (sub σ c false_).freeVarSet = Finset.image σ false_.freeVarSet

case not_
c : Char
a✝ : Formula
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c a✝.not_).freeVarSet = Finset.image σ a✝.not_.freeVarSet

case imp_
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (σ : VarName → VarName), (sub σ c a✝¹).freeVarSet = Finset.image σ a✝¹.freeVarSet
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (a✝¹.imp_ a✝)).freeVarSet = Finset.image σ (a✝¹.imp_ a✝).freeVarSet

case and_
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (σ : VarName → VarName), (sub σ c a✝¹).freeVarSet = Finset.image σ a✝¹.freeVarSet
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (a✝¹.and_ a✝)).freeVarSet = Finset.image σ (a✝¹.and_ a✝).freeVarSet

case or_
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (σ : VarName → VarName), (sub σ c a✝¹).freeVarSet = Finset.image σ a✝¹.freeVarSet
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (a✝¹.or_ a✝)).freeVarSet = Finset.image σ (a✝¹.or_ a✝).freeVarSet

case iff_
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (σ : VarName → VarName), (sub σ c a✝¹).freeVarSet = Finset.image σ a✝¹.freeVarSet
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (a✝¹.iff_ a✝)).freeVarSet = Finset.image σ (a✝¹.iff_ a✝).freeVarSet

case forall_
c : Char
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (forall_ a✝¹ a✝)).freeVarSet = Finset.image σ (forall_ a✝¹ a✝).freeVarSet

case exists_
c : Char
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (exists_ a✝¹ a✝)).freeVarSet = Finset.image σ (exists_ a✝¹ a✝).freeVarSet

case def_
c : Char
a✝¹ : DefName
a✝ : List VarName
σ : VarName → VarName
⊢ (sub σ c (def_ a✝¹ a✝)).freeVarSet = Finset.image σ (def_ a✝¹ a✝).freeVarSet
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
⊢ (List.map σ xs).toFinset = Finset.image σ xs.toFinset
Tactic:
case pred_const_ X xs | pred_var_ X xs | eq_ x y | def_ X xs =>
  apply Finset.ext
  intro a
  simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
σ : VarName → VarName
⊢ ∅ = Finset.image σ ∅
Tactic:
case true_ | false_ =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
Tactic:
case not_ phi phi_ih =>
  exact phi_ih σ
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
⊢ (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi).freeVarSet \
      {if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x} =
    Finset.image σ (phi.freeVarSet \ {x})
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [phi_ih]
  simp only [<- Finset.image_sdiff_singleton_updateITE phi.freeVarSet x x σ]
  split_ifs
  case _ c1 =>
    obtain s1 := fresh_not_mem x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi))
    generalize (
    fresh x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi)) ) = x' at *
    have s2 : Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) ⊆ Finset.image (Function.updateITE σ x x) (freeVarSet phi)
    apply Finset.image_subset_image
    simp
    have s3 : x' ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
    apply Finset.not_mem_mono s2 s1
    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
  case _ c1 =>
    simp at c1
    have s1 : Finset.image (Function.updateITE σ x x) (freeVarSet phi) \ {x} = Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) \ {x}
    apply Finset.image_sdiff_singleton
    simp only [Function.updateITE]
    simp
    simp only [s1]
    clear s1
    have s2 : x ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
    simp only [Finset.mem_image]
    simp
    simp only [Function.updateITE]
    simp
    tauto
    simp only [Finset.sdiff_singleton_eq_self s2]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case def_
c : Char
a✝¹ : DefName
a✝ : List VarName
σ : VarName → VarName
⊢ (sub σ c (def_ a✝¹ a✝)).freeVarSet = Finset.image σ (def_ a✝¹ a✝).freeVarSet
Tactic:
simp only [sub]
Proof state after:
case def_
c : Char
a✝¹ : DefName
a✝ : List VarName
σ : VarName → VarName
⊢ (def_ a✝¹ (List.map σ a✝)).freeVarSet = Finset.image σ (def_ a✝¹ a✝).freeVarSet
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case def_
c : Char
a✝¹ : DefName
a✝ : List VarName
σ : VarName → VarName
⊢ (def_ a✝¹ (List.map σ a✝)).freeVarSet = Finset.image σ (def_ a✝¹ a✝).freeVarSet
Tactic:
simp only [freeVarSet]
Proof state after:
case def_
c : Char
a✝¹ : DefName
a✝ : List VarName
σ : VarName → VarName
⊢ (List.map σ a✝).toFinset = Finset.image σ a✝.toFinset
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
⊢ (List.map σ xs).toFinset = Finset.image σ xs.toFinset
Tactic:
apply Finset.ext
Proof state after:
case a
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
⊢ ∀ (a : VarName), a ∈ (List.map σ xs).toFinset ↔ a ∈ Finset.image σ xs.toFinset
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case a
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
⊢ ∀ (a : VarName), a ∈ (List.map σ xs).toFinset ↔ a ∈ Finset.image σ xs.toFinset
Tactic:
intro a
Proof state after:
case a
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
a : VarName
⊢ a ∈ (List.map σ xs).toFinset ↔ a ∈ Finset.image σ xs.toFinset
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case a
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
a : VarName
⊢ a ∈ (List.map σ xs).toFinset ↔ a ∈ Finset.image σ xs.toFinset
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
σ : VarName → VarName
⊢ ∅ = Finset.image σ ∅
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
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
Tactic:
exact phi_ih σ
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
phi psi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
psi_ih : ∀ (σ : VarName → VarName), (sub σ c psi).freeVarSet = Finset.image σ psi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c phi).freeVarSet ∪ (sub σ c psi).freeVarSet = Finset.image σ (phi.freeVarSet ∪ psi.freeVarSet)
Tactic:
simp only [Finset.image_union]
Proof state after:
c : Char
phi psi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
psi_ih : ∀ (σ : VarName → VarName), (sub σ c psi).freeVarSet = Finset.image σ psi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c phi).freeVarSet ∪ (sub σ c psi).freeVarSet = Finset.image σ phi.freeVarSet ∪ Finset.image σ psi.freeVarSet
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
c : Char
phi psi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
psi_ih : ∀ (σ : VarName → VarName), (sub σ c psi).freeVarSet = Finset.image σ psi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c phi).freeVarSet ∪ (sub σ c psi).freeVarSet = Finset.image σ phi.freeVarSet ∪ Finset.image σ psi.freeVarSet
Tactic:
congr!
Proof state after:
case h.e'_3
c : Char
phi psi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
psi_ih : ∀ (σ : VarName → VarName), (sub σ c psi).freeVarSet = Finset.image σ psi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet

case h.e'_4
c : Char
phi psi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
psi_ih : ∀ (σ : VarName → VarName), (sub σ c psi).freeVarSet = Finset.image σ psi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c psi).freeVarSet = Finset.image σ psi.freeVarSet
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case h.e'_3
c : Char
phi psi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
psi_ih : ∀ (σ : VarName → VarName), (sub σ c psi).freeVarSet = Finset.image σ psi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
Tactic:
exact phi_ih σ
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof state before:
case h.e'_4
c : Char
phi psi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
psi_ih : ∀ (σ : VarName → VarName), (sub σ c psi).freeVarSet = Finset.image σ psi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c psi).freeVarSet = Finset.image σ psi.freeVarSet
Tactic:
exact psi_ih σ
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
⊢ (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi).freeVarSet \
      {if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x} =
    Finset.image σ (phi.freeVarSet \ {x})
Tactic:
simp only [phi_ih]
Proof state after:
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
⊢ Finset.image
        (Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then
            fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
          else x))
        phi.freeVarSet \
      {if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
        else x} =
    Finset.image σ (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
⊢ Finset.image
        (Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then
            fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
          else x))
        phi.freeVarSet \
      {if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
        else x} =
    Finset.image σ (phi.freeVarSet \ {x})
Tactic:
simp only [<- Finset.image_sdiff_singleton_updateITE phi.freeVarSet 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
⊢ Finset.image
        (Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then
            fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
          else x))
        phi.freeVarSet \
      {if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
        else 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
⊢ Finset.image
        (Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then
            fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
          else x))
        phi.freeVarSet \
      {if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
        else x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
split_ifs
Proof state after:
case pos
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
h✝ : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Finset.image (Function.updateITE σ x (fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)))
        phi.freeVarSet \
      {fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})

case neg
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
h✝ : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = 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
⊢ Finset.image (Function.updateITE σ x (fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)))
        phi.freeVarSet \
      {fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
case _ c1 =>
  obtain s1 := fresh_not_mem x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi))
  generalize (
  fresh x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi)) ) = x' at *
  have s2 : Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) ⊆ Finset.image (Function.updateITE σ x x) (freeVarSet phi)
  apply Finset.image_subset_image
  simp
  have s3 : x' ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
  apply Finset.not_mem_mono s2 s1
  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
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
case _ c1 =>
  simp at c1
  have s1 : Finset.image (Function.updateITE σ x x) (freeVarSet phi) \ {x} = Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) \ {x}
  apply Finset.image_sdiff_singleton
  simp only [Function.updateITE]
  simp
  simp only [s1]
  clear s1
  have s2 : x ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
  simp only [Finset.mem_image]
  simp
  simp only [Function.updateITE]
  simp
  tauto
  simp only [Finset.sdiff_singleton_eq_self s2]
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 (fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)))
        phi.freeVarSet \
      {fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
obtain s1 := fresh_not_mem x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi))
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
s1 :
  fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet) ∉
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Finset.image (Function.updateITE σ x (fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)))
        phi.freeVarSet \
      {fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)} =
    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
s1 :
  fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet) ∉
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Finset.image (Function.updateITE σ x (fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)))
        phi.freeVarSet \
      {fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
generalize (
fresh x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi)) ) = x' at *
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
⊢ 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
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
Tactic:
have s2 : Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) ⊆ Finset.image (Function.updateITE σ x x) (freeVarSet phi)
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 : ∃ 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})