Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet (FOL/NV/Binders.lean)

State before:
v : VarName
F : Formula
⊢ isFreeIn v F ↔ v ∈ F.freeVarSet
Tactic:
induction F
State after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isFreeIn v (pred_const_ a✝¹ a✝) ↔ v ∈ (pred_const_ a✝¹ a✝).freeVarSet

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isFreeIn v (pred_var_ a✝¹ a✝) ↔ v ∈ (pred_var_ a✝¹ a✝).freeVarSet

case eq_
v a✝¹ a✝ : VarName
⊢ isFreeIn v (eq_ a✝¹ a✝) ↔ v ∈ (eq_ a✝¹ a✝).freeVarSet

case true_
v : VarName
⊢ isFreeIn v true_ ↔ v ∈ true_.freeVarSet

case false_
v : VarName
⊢ isFreeIn v false_ ↔ v ∈ false_.freeVarSet

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v a✝.not_ ↔ v ∈ a✝.not_.freeVarSet

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.imp_ a✝) ↔ v ∈ (a✝¹.imp_ a✝).freeVarSet

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.and_ a✝) ↔ v ∈ (a✝¹.and_ a✝).freeVarSet

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.or_ a✝) ↔ v ∈ (a✝¹.or_ a✝).freeVarSet

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.iff_ a✝) ↔ v ∈ (a✝¹.iff_ a✝).freeVarSet

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (forall_ a✝¹ a✝) ↔ v ∈ (forall_ a✝¹ a✝).freeVarSet

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (exists_ a✝¹ a✝) ↔ v ∈ (exists_ a✝¹ a✝).freeVarSet

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isFreeIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).freeVarSet

State before:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isFreeIn v (pred_const_ a✝¹ a✝) ↔ v ∈ (pred_const_ a✝¹ a✝).freeVarSet

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isFreeIn v (pred_var_ a✝¹ a✝) ↔ v ∈ (pred_var_ a✝¹ a✝).freeVarSet

case eq_
v a✝¹ a✝ : VarName
⊢ isFreeIn v (eq_ a✝¹ a✝) ↔ v ∈ (eq_ a✝¹ a✝).freeVarSet

case true_
v : VarName
⊢ isFreeIn v true_ ↔ v ∈ true_.freeVarSet

case false_
v : VarName
⊢ isFreeIn v false_ ↔ v ∈ false_.freeVarSet

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v a✝.not_ ↔ v ∈ a✝.not_.freeVarSet

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.imp_ a✝) ↔ v ∈ (a✝¹.imp_ a✝).freeVarSet

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.and_ a✝) ↔ v ∈ (a✝¹.and_ a✝).freeVarSet

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.or_ a✝) ↔ v ∈ (a✝¹.or_ a✝).freeVarSet

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.iff_ a✝) ↔ v ∈ (a✝¹.iff_ a✝).freeVarSet

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (forall_ a✝¹ a✝) ↔ v ∈ (forall_ a✝¹ a✝).freeVarSet

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (exists_ a✝¹ a✝) ↔ v ∈ (exists_ a✝¹ a✝).freeVarSet

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isFreeIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).freeVarSet
Tactic:
all_goals
  simp only [isFreeIn]
  simp only [Formula.freeVarSet]
State after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ a✝.toFinset

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ a✝.toFinset

case eq_
v a✝¹ a✝ : VarName
⊢ v = a✝¹ ∨ v = a✝ ↔ v ∈ {a✝¹, a✝}

case true_
v : VarName
⊢ False ↔ v ∈ ∅

case false_
v : VarName
⊢ False ↔ v ∈ ∅

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v a✝¹ ∨ isFreeIn v a✝ ↔ v ∈ a✝¹.freeVarSet ∪ a✝.freeVarSet

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v a✝¹ ∨ isFreeIn v a✝ ↔ v ∈ a✝¹.freeVarSet ∪ a✝.freeVarSet

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v a✝¹ ∨ isFreeIn v a✝ ↔ v ∈ a✝¹.freeVarSet ∪ a✝.freeVarSet

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v a✝¹ ∨ isFreeIn v a✝ ↔ v ∈ a✝¹.freeVarSet ∪ a✝.freeVarSet

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ ¬v = a✝¹ ∧ isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet \ {a✝¹}

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ ¬v = a✝¹ ∧ isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet \ {a✝¹}

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ a✝.toFinset

State before:
v : VarName
X : DefName
xs : List VarName
⊢ v ∈ xs ↔ v ∈ xs.toFinset
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
State after:
no goals

State before:
v x y : VarName
⊢ v = x ∨ v = y ↔ v ∈ {x, y}
Tactic:
case eq_ x y =>
  simp
State after:
no goals

State before:
v : VarName
⊢ False ↔ v ∈ ∅
Tactic:
case true_ | false_ =>
  tauto
State after:
no goals

State before:
v : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ isFreeIn v phi ↔ v ∈ phi.freeVarSet
Tactic:
case not_ phi phi_ih =>
  tauto
State after:
no goals

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
psi_ih : isFreeIn v psi ↔ v ∈ psi.freeVarSet
⊢ isFreeIn v phi ∨ isFreeIn v psi ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp
  tauto
State after:
no goals

State before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ ¬v = x ∧ isFreeIn v phi ↔ v ∈ phi.freeVarSet \ {x}
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  tauto
State after:
no goals

State before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isFreeIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).freeVarSet
Tactic:
simp only [isFreeIn]
State after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ (def_ a✝¹ a✝).freeVarSet

State before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ (def_ a✝¹ a✝).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
State after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ a✝.toFinset

State before:
v : VarName
X : DefName
xs : List VarName
⊢ v ∈ xs ↔ v ∈ xs.toFinset
Tactic:
simp
State after:
no goals

State before:
v x y : VarName
⊢ v = x ∨ v = y ↔ v ∈ {x, y}
Tactic:
simp
State after:
no goals

State before:
v : VarName
⊢ False ↔ v ∈ ∅
Tactic:
tauto
State after:
no goals

State before:
v : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ isFreeIn v phi ↔ v ∈ phi.freeVarSet
Tactic:
tauto
State after:
no goals

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
psi_ih : isFreeIn v psi ↔ v ∈ psi.freeVarSet
⊢ isFreeIn v phi ∨ isFreeIn v psi ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet
Tactic:
simp
State after:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
psi_ih : isFreeIn v psi ↔ v ∈ psi.freeVarSet
⊢ isFreeIn v phi ∨ isFreeIn v psi ↔ v ∈ phi.freeVarSet ∨ v ∈ psi.freeVarSet

State before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
psi_ih : isFreeIn v psi ↔ v ∈ psi.freeVarSet
⊢ isFreeIn v phi ∨ isFreeIn v psi ↔ v ∈ phi.freeVarSet ∨ v ∈ psi.freeVarSet
Tactic:
tauto
State after:
no goals

State before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ ¬v = x ∧ isFreeIn v phi ↔ v ∈ phi.freeVarSet \ {x}
Tactic:
simp
State after:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ ¬v = x ∧ isFreeIn v phi ↔ v ∈ phi.freeVarSet ∧ ¬v = x

State before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ ¬v = x ∧ isFreeIn v phi ↔ v ∈ phi.freeVarSet ∧ ¬v = x
Tactic:
tauto
State after:
no goals