Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image (FOL/NV/Sub/Var/All/Rec/Fresh/Sub.lean)

State before:
σ : VarName → VarName
c : Char
F : Formula
⊢ (sub σ c F).freeVarSet = Finset.image σ F.freeVarSet
Tactic:
induction F generalizing σ
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

State before:
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
Tactic:
all_goals
  simp only [sub]
  simp only [freeVarSet]
State after:
case pred_const_
c : Char
a✝¹ : PredName
a✝ : List VarName
σ : VarName → VarName
⊢ (List.map σ a✝).toFinset = Finset.image σ a✝.toFinset

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

case eq_
c : Char
a✝¹ a✝ : VarName
σ : VarName → VarName
⊢ {σ a✝¹, σ a✝} = Finset.image σ {a✝¹, a✝}

case true_
c : Char
σ : VarName → VarName
⊢ ∅ = Finset.image σ ∅

case false_
c : Char
σ : VarName → VarName
⊢ ∅ = Finset.image σ ∅

case not_
c : Char
a✝ : Formula
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c a✝).freeVarSet = Finset.image σ a✝.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✝¹).freeVarSet ∪ (sub σ c a✝).freeVarSet = Finset.image σ (a✝¹.freeVarSet ∪ 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✝¹).freeVarSet ∪ (sub σ c a✝).freeVarSet = Finset.image σ (a✝¹.freeVarSet ∪ 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✝¹).freeVarSet ∪ (sub σ c a✝).freeVarSet = Finset.image σ (a✝¹.freeVarSet ∪ 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✝¹).freeVarSet ∪ (sub σ c a✝).freeVarSet = Finset.image σ (a✝¹.freeVarSet ∪ 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
          (Function.updateITE σ a✝¹
            (if ∃ y ∈ a✝.freeVarSet \ {a✝¹}, σ y = a✝¹ then
              fresh a✝¹ c (sub (Function.updateITE σ a✝¹ a✝¹) c a✝).freeVarSet
            else a✝¹))
          c a✝).freeVarSet \
      {if ∃ y ∈ a✝.freeVarSet \ {a✝¹}, σ y = a✝¹ then fresh a✝¹ c (sub (Function.updateITE σ a✝¹ a✝¹) c a✝).freeVarSet
        else a✝¹} =
    Finset.image σ (a✝.freeVarSet \ {a✝¹})

case exists_
c : Char
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub
          (Function.updateITE σ a✝¹
            (if ∃ y ∈ a✝.freeVarSet \ {a✝¹}, σ y = a✝¹ then
              fresh a✝¹ c (sub (Function.updateITE σ a✝¹ a✝¹) c a✝).freeVarSet
            else a✝¹))
          c a✝).freeVarSet \
      {if ∃ y ∈ a✝.freeVarSet \ {a✝¹}, σ y = a✝¹ then fresh a✝¹ c (sub (Function.updateITE σ a✝¹ a✝¹) c a✝).freeVarSet
        else a✝¹} =
    Finset.image σ (a✝.freeVarSet \ {a✝¹})

case def_
c : Char
a✝¹ : DefName
a✝ : List VarName
σ : VarName → VarName
⊢ (List.map σ a✝).toFinset = Finset.image σ a✝.toFinset

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
State after:
no goals

State before:
c : Char
σ : VarName → VarName
⊢ ∅ = Finset.image σ ∅
Tactic:
case true_ | false_ =>
  simp
State after:
no goals

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 σ
State after:
no goals

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]
State after:
no goals

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]
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

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]
State after:
case def_
c : Char
a✝¹ : DefName
a✝ : List VarName
σ : VarName → VarName
⊢ (List.map σ a✝).toFinset = Finset.image σ a✝.toFinset

State before:
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
⊢ (List.map σ xs).toFinset = Finset.image σ xs.toFinset
Tactic:
apply Finset.ext
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

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
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

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
State after:
no goals

State before:
c : Char
σ : VarName → VarName
⊢ ∅ = Finset.image σ ∅
Tactic:
simp
State after:
no goals

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 σ
State after:
no goals

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]
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

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!
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

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 σ
State after:
no goals

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 σ
State after:
no goals

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]
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})

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 σ]
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})

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
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})

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
State after:
no goals

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]
State after:
no goals

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))
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})

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 *
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})

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)
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})

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
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})

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
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})

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})
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})

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
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})

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
State after:
no goals

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')
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'

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]
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'

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
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})

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}
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})

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
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})

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]
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})

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
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})

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]
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})

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
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})

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})
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})

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 : ∀ 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})
Tactic:
simp only [Finset.mem_image]
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
⊢ ¬∃ a ∈ phi.freeVarSet \ {x}, Function.updateITE σ x x a = 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})

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 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ¬∃ a ∈ phi.freeVarSet \ {x}, Function.updateITE σ x x a = 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})
Tactic:
simp
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_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬Function.updateITE σ x x x_1 = 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})

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 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬Function.updateITE σ x x x_1 = 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})
Tactic:
simp only [Function.updateITE]
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_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬(if x_1 = x then x else σ x_1) = 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})

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 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬(if x_1 = x then x else σ x_1) = 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})
Tactic:
simp
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_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬x_1 = x ∧ ¬σ x_1 = 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})

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 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬x_1 = x ∧ ¬σ x_1 = 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})
Tactic:
tauto
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
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})

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
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})
Tactic:
simp only [Finset.sdiff_singleton_eq_self s2]
State after:
no goals