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:
simp only [boundVarSet']
State after:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isBound ↔ v ∈ Finset.filter isBound F.varSet

State before:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isBound ↔ v ∈ Finset.filter isBound F.varSet
Tactic:
simp
State after:
v : Var
F : Formula
⊢ v.isBound → (occursIn v F ↔ v ∈ F.varSet)

State before:
v : Var
F : Formula
⊢ v.isBound → (occursIn v F ↔ v ∈ F.varSet)
Tactic:
intro _
State after:
v : Var
F : Formula
a✝ : v.isBound
⊢ occursIn v F ↔ v ∈ F.varSet

State before:
v : Var
F : Formula
a✝ : v.isBound
⊢ occursIn v F ↔ v ∈ F.varSet
Tactic:
exact occursIn_iff_mem_varSet v F
State after:
no goals