internlm/Lean-Github huggingface dataset:
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof 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
Proof 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
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof 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]
Proof 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
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof 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]
Proof 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
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isBound ↔ v ∈ F.boundVarSet
Tactic:
induction F
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof state after:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isBound ↔ v ∈ vs.toFinset.biUnion Var.boundVarSet
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof state after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isBound ↔ v ∈ vs.toFinset.biUnion Var.boundVarSet
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isBound ↔ v ∈ vs.toFinset.biUnion Var.boundVarSet
Tactic:
simp
Proof state after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isBound ↔ ∃ a ∈ vs, v ∈ a.boundVarSet
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isBound ↔ ∃ a ∈ vs, v ∈ a.boundVarSet
Tactic:
constructor
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof state before:
case mp
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isBound → ∃ a ∈ vs, v ∈ a.boundVarSet
Tactic:
intro a1
Proof state after:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isBound
⊢ ∃ a ∈ vs, v ∈ a.boundVarSet
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isBound
⊢ v ∈ vs ∧ v ∈ v.boundVarSet
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof state before:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isBound
⊢ v ∈ vs ∧ v ∈ v.boundVarSet
Tactic:
cases v
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ False
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).boundVarSet
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof state after:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs ∧ bound_ i ∈ {bound_ i}
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof state before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs ∧ bound_ i ∈ {bound_ i}
Tactic:
simp
Proof state after:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof state before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs
Tactic:
cases a1
Proof state after:
case intro
X : String
vs : List Var
i : ℕ
left✝ : bound_ i ∈ vs
right✝ : (bound_ i).isBound
⊢ bound_ i ∈ vs
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof state before:
case mpr
v : Var
X : String
vs : List Var
⊢ (∃ a ∈ vs, v ∈ a.boundVarSet) → v ∈ vs ∧ v.isBound
Tactic:
intro a1
Proof state after:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
⊢ v ∈ vs ∧ v.isBound
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof state after:
X : String
vs : List Var
i : ℕ
a2_left : bound_ i ∈ vs
a1 : ∃ a ∈ vs, bound_ i ∈ a.boundVarSet
⊢ bound_ i ∈ vs ∧ True
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
X : String
vs : List Var
i : ℕ
a2_left : bound_ i ∈ vs
a1 : ∃ a ∈ vs, bound_ i ∈ a.boundVarSet
⊢ bound_ i ∈ vs
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof state after:
v : Var
phi : Formula
phi_ih : occursIn v phi ∧ v.isBound ↔ v ∈ phi.boundVarSet
⊢ occursIn v phi ∧ v.isBound ↔ v ∈ phi.boundVarSet
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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]
Proof 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
Theorem: LN.isBoundIn_iff_mem_boundVarSet
Proof 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
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet'
Proof state before:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isFree ↔ v ∈ F.freeVarSet'
Tactic:
simp only [freeVarSet']
Proof state after:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isFree ↔ v ∈ Finset.filter isFree F.varSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet'
Proof state before:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isFree ↔ v ∈ Finset.filter isFree F.varSet
Tactic:
simp
Proof state after:
v : Var
F : Formula
⊢ v.isFree → (occursIn v F ↔ v ∈ F.varSet)
Theorem: LN.isFreeIn_iff_mem_freeVarSet'
Proof state before:
v : Var
F : Formula
⊢ v.isFree → (occursIn v F ↔ v ∈ F.varSet)
Tactic:
intro _
Proof state after:
v : Var
F : Formula
a✝ : v.isFree
⊢ occursIn v F ↔ v ∈ F.varSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet'
Proof state before:
v : Var
F : Formula
a✝ : v.isFree
⊢ occursIn v F ↔ v ∈ F.varSet
Tactic:
exact occursIn_iff_mem_varSet v F
Proof state after:
no goals
Theorem: LN.isBoundIn_iff_mem_boundVarSet'
Proof state before:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isBound ↔ v ∈ F.boundVarSet'
Tactic:
simp only [boundVarSet']
Proof state after:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isBound ↔ v ∈ Finset.filter isBound F.varSet
Theorem: LN.isBoundIn_iff_mem_boundVarSet'
Proof state before:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isBound ↔ v ∈ Finset.filter isBound F.varSet
Tactic:
simp
Proof state after:
v : Var
F : Formula
⊢ v.isBound → (occursIn v F ↔ v ∈ F.varSet)
Theorem: LN.isBoundIn_iff_mem_boundVarSet'
Proof state before:
v : Var
F : Formula
⊢ v.isBound → (occursIn v F ↔ v ∈ F.varSet)
Tactic:
intro _
Proof state after:
v : Var
F : Formula
a✝ : v.isBound
⊢ occursIn v F ↔ v ∈ F.varSet
Theorem: LN.isBoundIn_iff_mem_boundVarSet'
Proof state before:
v : Var
F : Formula
a✝ : v.isBound
⊢ occursIn v F ↔ v ∈ F.varSet
Tactic:
exact occursIn_iff_mem_varSet v F
Proof state after:
no goals
Theorem: LN.IsFreeIffExistsString
Proof state before:
v : Var
⊢ v.isFree ↔ ∃ x, v = free_ x
Tactic:
cases v
Proof state after:
case free_
a✝ : String
⊢ (free_ a✝).isFree ↔ ∃ x, free_ a✝ = free_ x

case bound_
a✝ : ℕ
⊢ (bound_ a✝).isFree ↔ ∃ x, bound_ a✝ = free_ x
Theorem: LN.IsFreeIffExistsString
Proof state before:
x : String
⊢ (free_ x).isFree ↔ ∃ x_1, free_ x = free_ x_1
Tactic:
case free_ x =>
  simp only [isFree]
  simp
Proof state after:
no goals
Theorem: LN.IsFreeIffExistsString
Proof state before:
i : ℕ
⊢ (bound_ i).isFree ↔ ∃ x, bound_ i = free_ x
Tactic:
case bound_ i =>
  simp only [isFree]
  simp
Proof state after:
no goals
Theorem: LN.IsFreeIffExistsString
Proof state before:
x : String
⊢ (free_ x).isFree ↔ ∃ x_1, free_ x = free_ x_1
Tactic:
simp only [isFree]
Proof state after:
x : String
⊢ True ↔ ∃ x_1, free_ x = free_ x_1
Theorem: LN.IsFreeIffExistsString
Proof state before:
x : String
⊢ True ↔ ∃ x_1, free_ x = free_ x_1
Tactic:
simp
Proof state after:
no goals
Theorem: LN.IsFreeIffExistsString
Proof state before:
i : ℕ
⊢ (bound_ i).isFree ↔ ∃ x, bound_ i = free_ x
Tactic:
simp only [isFree]
Proof state after:
i : ℕ
⊢ False ↔ ∃ x, False
Theorem: LN.IsFreeIffExistsString
Proof state before:
i : ℕ
⊢ False ↔ ∃ x, False
Tactic:
simp
Proof state after:
no goals