Theorem: LN.occursIn_iff_mem_varSet (FOL/LN/Binders.lean)

State before:
v : Var
F : Formula
⊢ occursIn v F ↔ v ∈ F.varSet
Tactic:
induction F
State after:
case pred_
v : Var
a✝¹ : String
a✝ : List Var
⊢ occursIn v (pred_ a✝¹ a✝) ↔ v ∈ (pred_ a✝¹ a✝).varSet

case not_
v : Var
a✝ : Formula
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v a✝.not_ ↔ v ∈ a✝.not_.varSet

case imp_
v : Var
a✝¹ a✝ : Formula
a_ih✝¹ : occursIn v a✝¹ ↔ v ∈ a✝¹.varSet
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (a✝¹.imp_ a✝) ↔ v ∈ (a✝¹.imp_ a✝).varSet

case forall_
v : Var
a✝¹ : String
a✝ : Formula
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (forall_ a✝¹ a✝) ↔ v ∈ (forall_ a✝¹ a✝).varSet

State before:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ↔ v ∈ (pred_ X vs).varSet
Tactic:
case pred_ X vs =>
  simp only [occursIn]
  simp only [varSet]
  simp
State after:
no goals

State before:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi.not_ ↔ v ∈ phi.not_.varSet
Tactic:
case not_ phi phi_ih =>
  simp only [occursIn]
  simp only [varSet]
  exact phi_ih
State after:
no goals

State before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v (phi.imp_ psi) ↔ v ∈ (phi.imp_ psi).varSet
Tactic:
case imp_ phi psi phi_ih psi_ih =>
  simp only [occursIn]
  simp only [varSet]
  simp
  congr!
State after:
no goals

State before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v (forall_ a✝ phi) ↔ v ∈ (forall_ a✝ phi).varSet
Tactic:
case forall_ _ phi phi_ih =>
  simp only [occursIn]
  simp only [varSet]
  exact phi_ih
State after:
no goals

State before:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ↔ v ∈ (pred_ X vs).varSet
Tactic:
simp only [occursIn]
State after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ↔ v ∈ (pred_ X vs).varSet

State before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ↔ v ∈ (pred_ X vs).varSet
Tactic:
simp only [varSet]
State after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ↔ v ∈ vs.toFinset

State before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ↔ v ∈ vs.toFinset
Tactic:
simp
State after:
no goals

State before:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi.not_ ↔ v ∈ phi.not_.varSet
Tactic:
simp only [occursIn]
State after:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.not_.varSet

State before:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.not_.varSet
Tactic:
simp only [varSet]
State after:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet

State before:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet
Tactic:
exact phi_ih
State after:
no goals

State before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v (phi.imp_ psi) ↔ v ∈ (phi.imp_ psi).varSet
Tactic:
simp only [occursIn]
State after:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ (phi.imp_ psi).varSet

State before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ (phi.imp_ psi).varSet
Tactic:
simp only [varSet]
State after:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∪ psi.varSet

State before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∪ psi.varSet
Tactic:
simp
State after:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∨ v ∈ psi.varSet

State before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∨ v ∈ psi.varSet
Tactic:
congr!
State after:
no goals

State before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v (forall_ a✝ phi) ↔ v ∈ (forall_ a✝ phi).varSet
Tactic:
simp only [occursIn]
State after:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ (forall_ a✝ phi).varSet

State before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ (forall_ a✝ phi).varSet
Tactic:
simp only [varSet]
State after:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet

State before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet
Tactic:
exact phi_ih
State after:
no goals