Theorem: LeanSAT.Model.PropFun.semVars_conj (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, satisfies_conj, not_and_or]
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ (∃ τ, (τ ⊨ φ₁ ∧ τ ⊨ φ₂) ∧ (¬(PropAssignment.set τ x !τ 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) ⊨ φ₁) ∨ ∃ τ, τ ⊨ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂
Tactic:
aesop
State after:
no goals