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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⊔ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
intro x
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ x ∈ semVars (φ₁ ⊔ φ₂) → x ∈ semVars φ₁ ∪ semVars φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ x ∈ semVars (φ₁ ⊔ φ₂) → x ∈ semVars φ₁ ∪ semVars φ₂
Tactic:
simp only [Finset.mem_union, mem_semVars]
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φ₁ ⊔ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁ ⊔ φ₂) →
    (∃ τ, τ ⊨ φ₁ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁) ∨ ∃ τ, τ ⊨ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φ₁ ⊔ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁ ⊔ φ₂) →
    (∃ τ, τ ⊨ φ₁ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁) ∨ ∃ τ, τ ⊨ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂
Tactic:
aesop
State after:
no goals