Theorem: LeanSAT.Model.PropFun.semVars_mk (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
⊢ semVars ⟦φ⟧ ⊆ PropForm.vars φ
Tactic:
have := semVars'_subset_vars φ
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
this : LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(PropForm.vars φ)
⊢ semVars ⟦φ⟧ ⊆ PropForm.vars φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
this : LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(PropForm.vars φ)
⊢ semVars ⟦φ⟧ ⊆ PropForm.vars φ
Tactic:
unfold semVars
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
this : LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(PropForm.vars φ)
⊢ Set.Finite.toFinset ⋯ ⊆ PropForm.vars φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
this : LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(PropForm.vars φ)
⊢ Set.Finite.toFinset ⋯ ⊆ PropForm.vars φ
Tactic:
simp [this]
State after:
no goals