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

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

case not_
v : Var
a✝ : Formula
a_ih✝ : occursIn v a✝ ∧ v.isBound ↔ v ∈ a✝.boundVarSet
⊢ occursIn v a✝.not_ ∧ v.isBound ↔ v ∈ a✝.not_.boundVarSet

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

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

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

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

State before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ∧ v.isBound ↔ v ∈ phi.boundVarSet
⊢ occursIn v (forall_ a✝ phi) ∧ v.isBound ↔ v ∈ (forall_ a✝ phi).boundVarSet
Tactic:
case forall_ _ phi phi_ih =>
  simp only [Formula.boundVarSet]
  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.isBound ↔ v ∈ (pred_ X vs).boundVarSet
Tactic:
simp only [Formula.boundVarSet]
State after:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isBound ↔ v ∈ vs.toFinset.biUnion Var.boundVarSet

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

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

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

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

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

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

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

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

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

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

State before:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isBound
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).boundVarSet
Tactic:
simp only [Var.isBound] at a1
State after:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ False
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).boundVarSet

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

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

State before:
X : String
vs : List Var
x : String
a1_left : free_ x ∈ vs
a1_right : False
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).boundVarSet
Tactic:
contradiction
State after:
no goals

State before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).boundVarSet
Tactic:
simp only [Var.boundVarSet]
State after:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs ∧ bound_ i ∈ {bound_ i}

State before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs ∧ bound_ i ∈ {bound_ i}
Tactic:
simp
State after:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs

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

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

State before:
X : String
vs : List Var
i : ℕ
a1_left : bound_ i ∈ vs
a1_right : (bound_ i).isBound
⊢ bound_ i ∈ vs
Tactic:
exact a1_left
State after:
no goals

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

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

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

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

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

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ (free_ x).boundVarSet
⊢ v ∈ vs ∧ v.isBound
Tactic:
case _ x =>
  simp only [Var.boundVarSet] at a2
  simp at a2
State after:
no goals

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

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

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ ∅
⊢ v ∈ vs ∧ v.isBound
Tactic:
simp at a2
State after:
no goals

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

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ {bound_ i}
⊢ v ∈ vs ∧ v.isBound
Tactic:
simp at a2
State after:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v = bound_ i
⊢ v ∈ vs ∧ v.isBound

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v = bound_ i
⊢ v ∈ vs ∧ v.isBound
Tactic:
cases a2
State after:
case intro
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
i : ℕ
left✝ : bound_ i ∈ vs
right✝ : v = bound_ i
⊢ v ∈ vs ∧ v.isBound

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
i : ℕ
a2_left : bound_ i ∈ vs
a2_right : v = bound_ i
⊢ v ∈ vs ∧ v.isBound
Tactic:
case _ a2_left a2_right =>
  subst a2_right
  simp only [isBound]
  simp
  exact a2_left
State after:
no goals

State before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
i : ℕ
a2_left : bound_ i ∈ vs
a2_right : v = bound_ i
⊢ v ∈ vs ∧ v.isBound
Tactic:
subst a2_right
State after:
X : String
vs : List Var
i : ℕ
a2_left : bound_ i ∈ vs
a1 : ∃ a ∈ vs, bound_ i ∈ a.boundVarSet
⊢ bound_ i ∈ vs ∧ (bound_ i).isBound

State before:
X : String
vs : List Var
i : ℕ
a2_left : bound_ i ∈ vs
a1 : ∃ a ∈ vs, bound_ i ∈ a.boundVarSet
⊢ bound_ i ∈ vs ∧ (bound_ i).isBound
Tactic:
simp only [isBound]
State after:
X : String
vs : List Var
i : ℕ
a2_left : bound_ i ∈ vs
a1 : ∃ a ∈ vs, bound_ i ∈ a.boundVarSet
⊢ bound_ i ∈ vs ∧ True

State before:
X : String
vs : List Var
i : ℕ
a2_left : bound_ i ∈ vs
a1 : ∃ a ∈ vs, bound_ i ∈ a.boundVarSet
⊢ bound_ i ∈ vs ∧ True
Tactic:
simp
State after:
X : String
vs : List Var
i : ℕ
a2_left : bound_ i ∈ vs
a1 : ∃ a ∈ vs, bound_ i ∈ a.boundVarSet
⊢ bound_ i ∈ vs

State before:
X : String
vs : List Var
i : ℕ
a2_left : bound_ i ∈ vs
a1 : ∃ a ∈ vs, bound_ i ∈ a.boundVarSet
⊢ bound_ i ∈ vs
Tactic:
exact a2_left
State after:
no goals

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

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

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

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

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

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

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

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

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

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