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

State before:
P : PredName
n : ℕ
F : Formula
⊢ predVarOccursIn P n F ↔ (P, n) ∈ F.predVarSet
Tactic:
induction F
State after:
case pred_const_
P : PredName
n : ℕ
a✝¹ : PredName
a✝ : List VarName
⊢ predVarOccursIn P n (pred_const_ a✝¹ a✝) ↔ (P, n) ∈ (pred_const_ a✝¹ a✝).predVarSet

case pred_var_
P : PredName
n : ℕ
a✝¹ : PredName
a✝ : List VarName
⊢ predVarOccursIn P n (pred_var_ a✝¹ a✝) ↔ (P, n) ∈ (pred_var_ a✝¹ a✝).predVarSet

case eq_
P : PredName
n : ℕ
a✝¹ a✝ : VarName
⊢ predVarOccursIn P n (eq_ a✝¹ a✝) ↔ (P, n) ∈ (eq_ a✝¹ a✝).predVarSet

case true_
P : PredName
n : ℕ
⊢ predVarOccursIn P n true_ ↔ (P, n) ∈ true_.predVarSet

case false_
P : PredName
n : ℕ
⊢ predVarOccursIn P n false_ ↔ (P, n) ∈ false_.predVarSet

case not_
P : PredName
n : ℕ
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝.not_ ↔ (P, n) ∈ a✝.not_.predVarSet

case imp_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.imp_ a✝) ↔ (P, n) ∈ (a✝¹.imp_ a✝).predVarSet

case and_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.and_ a✝) ↔ (P, n) ∈ (a✝¹.and_ a✝).predVarSet

case or_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.or_ a✝) ↔ (P, n) ∈ (a✝¹.or_ a✝).predVarSet

case iff_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.iff_ a✝) ↔ (P, n) ∈ (a✝¹.iff_ a✝).predVarSet

case forall_
P : PredName
n : ℕ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (forall_ a✝¹ a✝) ↔ (P, n) ∈ (forall_ a✝¹ a✝).predVarSet

case exists_
P : PredName
n : ℕ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (exists_ a✝¹ a✝) ↔ (P, n) ∈ (exists_ a✝¹ a✝).predVarSet

case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ predVarOccursIn P n (def_ a✝¹ a✝) ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet

State before:
case pred_const_
P : PredName
n : ℕ
a✝¹ : PredName
a✝ : List VarName
⊢ predVarOccursIn P n (pred_const_ a✝¹ a✝) ↔ (P, n) ∈ (pred_const_ a✝¹ a✝).predVarSet

case pred_var_
P : PredName
n : ℕ
a✝¹ : PredName
a✝ : List VarName
⊢ predVarOccursIn P n (pred_var_ a✝¹ a✝) ↔ (P, n) ∈ (pred_var_ a✝¹ a✝).predVarSet

case eq_
P : PredName
n : ℕ
a✝¹ a✝ : VarName
⊢ predVarOccursIn P n (eq_ a✝¹ a✝) ↔ (P, n) ∈ (eq_ a✝¹ a✝).predVarSet

case true_
P : PredName
n : ℕ
⊢ predVarOccursIn P n true_ ↔ (P, n) ∈ true_.predVarSet

case false_
P : PredName
n : ℕ
⊢ predVarOccursIn P n false_ ↔ (P, n) ∈ false_.predVarSet

case not_
P : PredName
n : ℕ
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝.not_ ↔ (P, n) ∈ a✝.not_.predVarSet

case imp_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.imp_ a✝) ↔ (P, n) ∈ (a✝¹.imp_ a✝).predVarSet

case and_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.and_ a✝) ↔ (P, n) ∈ (a✝¹.and_ a✝).predVarSet

case or_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.or_ a✝) ↔ (P, n) ∈ (a✝¹.or_ a✝).predVarSet

case iff_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.iff_ a✝) ↔ (P, n) ∈ (a✝¹.iff_ a✝).predVarSet

case forall_
P : PredName
n : ℕ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (forall_ a✝¹ a✝) ↔ (P, n) ∈ (forall_ a✝¹ a✝).predVarSet

case exists_
P : PredName
n : ℕ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (exists_ a✝¹ a✝) ↔ (P, n) ∈ (exists_ a✝¹ a✝).predVarSet

case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ predVarOccursIn P n (def_ a✝¹ a✝) ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet
Tactic:
all_goals
  simp only [predVarOccursIn]
  simp only [Formula.predVarSet]
State after:
case pred_const_
P : PredName
n : ℕ
a✝¹ : PredName
a✝ : List VarName
⊢ False ↔ (P, n) ∈ ∅

case pred_var_
P : PredName
n : ℕ
a✝¹ : PredName
a✝ : List VarName
⊢ P = a✝¹ ∧ n = a✝.length ↔ (P, n) ∈ {(a✝¹, a✝.length)}

case eq_
P : PredName
n : ℕ
a✝¹ a✝ : VarName
⊢ False ↔ (P, n) ∈ ∅

case true_
P : PredName
n : ℕ
⊢ False ↔ (P, n) ∈ ∅

case false_
P : PredName
n : ℕ
⊢ False ↔ (P, n) ∈ ∅

case not_
P : PredName
n : ℕ
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet

case imp_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝¹ ∨ predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝¹.predVarSet ∪ a✝.predVarSet

case and_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝¹ ∨ predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝¹.predVarSet ∪ a✝.predVarSet

case or_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝¹ ∨ predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝¹.predVarSet ∪ a✝.predVarSet

case iff_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝¹ ∨ predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝¹.predVarSet ∪ a✝.predVarSet

case forall_
P : PredName
n : ℕ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet

case exists_
P : PredName
n : ℕ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet

case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ (P, n) ∈ ∅

State before:
P : PredName
n : ℕ
X : DefName
xs : List VarName
⊢ False ↔ (P, n) ∈ ∅
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
State after:
no goals

State before:
P : PredName
n : ℕ
x y : VarName
⊢ False ↔ (P, n) ∈ ∅
Tactic:
case eq_ x y =>
  simp
State after:
no goals

State before:
P : PredName
n : ℕ
⊢ False ↔ (P, n) ∈ ∅
Tactic:
case true_ | false_ =>
  tauto
State after:
no goals

State before:
P : PredName
n : ℕ
phi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
⊢ predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
Tactic:
case not_ phi phi_ih =>
  tauto
State after:
no goals

State before:
P : PredName
n : ℕ
phi psi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
psi_ih : predVarOccursIn P n psi ↔ (P, n) ∈ psi.predVarSet
⊢ predVarOccursIn P n phi ∨ predVarOccursIn P n psi ↔ (P, n) ∈ phi.predVarSet ∪ psi.predVarSet
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:
P : PredName
n : ℕ
x : VarName
phi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
⊢ predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  tauto
State after:
no goals

State before:
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ predVarOccursIn P n (def_ a✝¹ a✝) ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet
Tactic:
simp only [predVarOccursIn]
State after:
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet

State before:
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet
Tactic:
simp only [Formula.predVarSet]
State after:
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ (P, n) ∈ ∅

State before:
P : PredName
n : ℕ
X : DefName
xs : List VarName
⊢ False ↔ (P, n) ∈ ∅
Tactic:
simp
State after:
no goals

State before:
P : PredName
n : ℕ
x y : VarName
⊢ False ↔ (P, n) ∈ ∅
Tactic:
simp
State after:
no goals

State before:
P : PredName
n : ℕ
⊢ False ↔ (P, n) ∈ ∅
Tactic:
tauto
State after:
no goals

State before:
P : PredName
n : ℕ
phi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
⊢ predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
Tactic:
tauto
State after:
no goals

State before:
P : PredName
n : ℕ
phi psi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
psi_ih : predVarOccursIn P n psi ↔ (P, n) ∈ psi.predVarSet
⊢ predVarOccursIn P n phi ∨ predVarOccursIn P n psi ↔ (P, n) ∈ phi.predVarSet ∪ psi.predVarSet
Tactic:
simp
State after:
P : PredName
n : ℕ
phi psi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
psi_ih : predVarOccursIn P n psi ↔ (P, n) ∈ psi.predVarSet
⊢ predVarOccursIn P n phi ∨ predVarOccursIn P n psi ↔ (P, n) ∈ phi.predVarSet ∨ (P, n) ∈ psi.predVarSet

State before:
P : PredName
n : ℕ
phi psi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
psi_ih : predVarOccursIn P n psi ↔ (P, n) ∈ psi.predVarSet
⊢ predVarOccursIn P n phi ∨ predVarOccursIn P n psi ↔ (P, n) ∈ phi.predVarSet ∨ (P, n) ∈ psi.predVarSet
Tactic:
tauto
State after:
no goals

State before:
P : PredName
n : ℕ
x : VarName
phi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
⊢ predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
Tactic:
tauto
State after:
no goals