Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.freeVarSet_sub_eq_freeVarSet_image
Proof 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]
Proof 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