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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (biImpl φ₁ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
rw [biImpl_eq_impls]
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars ((φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) ⊆ semVars φ₁ ∪ semVars φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars ((φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
apply subset_trans (semVars_conj _ _)
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ∪ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ∪ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
apply Finset.union_subset
State after:
case hs
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂

case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂

State before:
case hs
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂

case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
. apply semVars_impl
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
. rw [Finset.union_comm]
  apply semVars_impl
State after:
no goals

State before:
case hs
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
apply semVars_impl
State after:
no goals

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
rw [Finset.union_comm]
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₂ ∪ semVars φ₁

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₂ ∪ semVars φ₁
Tactic:
apply semVars_impl
State after:
no goals