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

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

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

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