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

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

case not_
v : Var
a✝ : Formula
a_ih✝ : occursIn v a✝ ∧ v.isFree ↔ v ∈ a✝.freeVarSet
⊢ occursIn v a✝.not_ ∧ v.isFree ↔ v ∈ a✝.not_.freeVarSet

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

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

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

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

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

State before:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isFree ↔ v ∈ (pred_ X vs).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
State after:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isFree ↔ v ∈ vs.toFinset.biUnion Var.freeVarSet

State before:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isFree ↔ v ∈ vs.toFinset.biUnion Var.freeVarSet
Tactic:
simp only [occursIn]
State after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree ↔ v ∈ vs.toFinset.biUnion Var.freeVarSet

State before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree ↔ v ∈ vs.toFinset.biUnion Var.freeVarSet
Tactic:
simp
State after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree ↔ ∃ a ∈ vs, v ∈ a.freeVarSet

State before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree ↔ ∃ a ∈ vs, v ∈ a.freeVarSet
Tactic:
constructor
State after:
case mp
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree → ∃ a ∈ vs, v ∈ a.freeVarSet

case mpr
v : Var
X : String
vs : List Var
⊢ (∃ a ∈ vs, v ∈ a.freeVarSet) → v ∈ vs ∧ v.isFree

State before:
case mp
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree → ∃ a ∈ vs, v ∈ a.freeVarSet
Tactic:
intro a1
State after:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isFree
⊢ ∃ a ∈ vs, v ∈ a.freeVarSet

State before:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isFree
⊢ ∃ a ∈ vs, v ∈ a.freeVarSet
Tactic:
apply Exists.intro v
State after:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isFree
⊢ v ∈ vs ∧ v ∈ v.freeVarSet

State before:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isFree
⊢ v ∈ vs ∧ v ∈ v.freeVarSet
Tactic:
cases v
State after:
case mp.free_
X : String
vs : List Var
a✝ : String
a1 : free_ a✝ ∈ vs ∧ (free_ a✝).isFree
⊢ free_ a✝ ∈ vs ∧ free_ a✝ ∈ (free_ a✝).freeVarSet

case mp.bound_
X : String
vs : List Var
a✝ : ℕ
a1 : bound_ a✝ ∈ vs ∧ (bound_ a✝).isFree
⊢ bound_ a✝ ∈ vs ∧ bound_ a✝ ∈ (bound_ a✝).freeVarSet

State before:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).freeVarSet
Tactic:
case _ x =>
  simp only [Var.freeVarSet]
  simp
  cases a1
  case _ a1_left a1_right =>
    exact a1_left
State after:
no goals

State before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isFree
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
case _ i =>
  simp only [isFree] at a1
  cases a1
  case _ a1_left a1_right =>
    contradiction
State after:
no goals

State before:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).freeVarSet
Tactic:
simp only [Var.freeVarSet]
State after:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ {free_ x}

State before:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ {free_ x}
Tactic:
simp
State after:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs

State before:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs
Tactic:
cases a1
State after:
case intro
X : String
vs : List Var
x : String
left✝ : free_ x ∈ vs
right✝ : (free_ x).isFree
⊢ free_ x ∈ vs

State before:
X : String
vs : List Var
x : String
a1_left : free_ x ∈ vs
a1_right : (free_ x).isFree
⊢ free_ x ∈ vs
Tactic:
case _ a1_left a1_right =>
  exact a1_left
State after:
no goals

State before:
X : String
vs : List Var
x : String
a1_left : free_ x ∈ vs
a1_right : (free_ x).isFree
⊢ free_ x ∈ vs
Tactic:
exact a1_left
State after:
no goals

State before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isFree
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
simp only [isFree] at a1
State after:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet

State before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
cases a1
State after:
case intro
X : String
vs : List Var
i : ℕ
left✝ : bound_ i ∈ vs
right✝ : False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet

State before:
X : String
vs : List Var
i : ℕ
a1_left : bound_ i ∈ vs
a1_right : False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
case _ a1_left a1_right =>
  contradiction
State after:
no goals

State before:
X : String
vs : List Var
i : ℕ
a1_left : bound_ i ∈ vs
a1_right : False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
contradiction
State after:
no goals

State before:
case mpr
v : Var
X : String
vs : List Var
⊢ (∃ a ∈ vs, v ∈ a.freeVarSet) → v ∈ vs ∧ v.isFree
Tactic:
intro a1
State after:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
⊢ v ∈ vs ∧ v.isFree

State before:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
apply Exists.elim a1
State after:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
⊢ ∀ (a : Var), a ∈ vs ∧ v ∈ a.freeVarSet → v ∈ vs ∧ v.isFree

State before:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
⊢ ∀ (a : Var), a ∈ vs ∧ v ∈ a.freeVarSet → v ∈ vs ∧ v.isFree
Tactic:
intro u a2
State after:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
u : Var
a2 : u ∈ vs ∧ v ∈ u.freeVarSet
⊢ v ∈ vs ∧ v.isFree

State before:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
u : Var
a2 : u ∈ vs ∧ v ∈ u.freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
cases u
State after:
case mpr.free_
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
a✝ : String
a2 : free_ a✝ ∈ vs ∧ v ∈ (free_ a✝).freeVarSet
⊢ v ∈ vs ∧ v.isFree

case mpr.bound_
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
a✝ : ℕ
a2 : bound_ a✝ ∈ vs ∧ v ∈ (bound_ a✝).freeVarSet
⊢ v ∈ vs ∧ v.isFree

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ (free_ x).freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
case _ x =>
  simp only [Var.freeVarSet] at a2
  simp at a2
  cases a2
  case _ a2_left a2_right =>
    subst a2_right
    simp only [isFree]
    simp
    exact a2_left
State after:
no goals

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ (bound_ i).freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
case _ i =>
  simp only [Var.freeVarSet] at a2
  simp at a2
State after:
no goals

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ (free_ x).freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
simp only [Var.freeVarSet] at a2
State after:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ {free_ x}
⊢ v ∈ vs ∧ v.isFree

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ {free_ x}
⊢ v ∈ vs ∧ v.isFree
Tactic:
simp at a2
State after:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v = free_ x
⊢ v ∈ vs ∧ v.isFree

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v = free_ x
⊢ v ∈ vs ∧ v.isFree
Tactic:
cases a2
State after:
case intro
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
left✝ : free_ x ∈ vs
right✝ : v = free_ x
⊢ v ∈ vs ∧ v.isFree

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2_left : free_ x ∈ vs
a2_right : v = free_ x
⊢ v ∈ vs ∧ v.isFree
Tactic:
case _ a2_left a2_right =>
  subst a2_right
  simp only [isFree]
  simp
  exact a2_left
State after:
no goals

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2_left : free_ x ∈ vs
a2_right : v = free_ x
⊢ v ∈ vs ∧ v.isFree
Tactic:
subst a2_right
State after:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs ∧ (free_ x).isFree

State before:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs ∧ (free_ x).isFree
Tactic:
simp only [isFree]
State after:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs ∧ True

State before:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs ∧ True
Tactic:
simp
State after:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs

State before:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs
Tactic:
exact a2_left
State after:
no goals

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ (bound_ i).freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
simp only [Var.freeVarSet] at a2
State after:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ ∅
⊢ v ∈ vs ∧ v.isFree

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ ∅
⊢ v ∈ vs ∧ v.isFree
Tactic:
simp at a2
State after:
no goals

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

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

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

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

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

State before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ (occursIn v phi ∨ occursIn v psi) ∧ v.isFree ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet
Tactic:
simp
State after:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ (occursIn v phi ∨ occursIn v psi) ∧ v.isFree ↔ v ∈ phi.freeVarSet ∨ v ∈ psi.freeVarSet

State before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ (occursIn v phi ∨ occursIn v psi) ∧ v.isFree ↔ v ∈ phi.freeVarSet ∨ v ∈ psi.freeVarSet
Tactic:
tauto
State after:
no goals

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

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

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