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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ σ₁ ⊨ φ → (fun M φ => ¬M ⊨ φ) σ₂ φ → ∃ x, σ₁ x ≠ σ₂ x ∧ x ∈ semVars φ
Tactic:
have ⟨φ', hMk⟩ := Quotient.exists_rep φ
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ → (fun M φ => ¬M ⊨ φ) σ₂ φ → ∃ x, σ₁ x ≠ σ₂ x ∧ x ∈ semVars φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ → (fun M φ => ¬M ⊨ φ) σ₂ φ → ∃ x, σ₁ x ≠ σ₂ x ∧ x ∈ semVars φ
Tactic:
dsimp
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ → ¬σ₂ ⊨ φ → ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ → ¬σ₂ ⊨ φ → ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars φ
Tactic:
rw [← hMk, satisfies_mk, satisfies_mk]
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ' → ¬σ₂ ⊨ φ' → ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ' → ¬σ₂ ⊨ φ' → ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧
Tactic:
intro h₁ h₂
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
⊢ ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
⊢ ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧
Tactic:
have ⟨x, τ, hNe, hτ, hτ'⟩ := PropForm.exists_flip h₁ h₂
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧
Tactic:
use x, hNe
State after:
case right
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ x ∈ semVars ⟦φ'⟧

State before:
case right
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ x ∈ semVars ⟦φ'⟧
Tactic:
simp only [mem_semVars]
State after:
case right
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ ∃ τ, τ ⊨ ⟦φ'⟧ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ ⟦φ'⟧

State before:
case right
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ ∃ τ, τ ⊨ ⟦φ'⟧ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ ⟦φ'⟧
Tactic:
use τ
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ τ ⊨ ⟦φ'⟧ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ ⟦φ'⟧

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ τ ⊨ ⟦φ'⟧ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ ⟦φ'⟧
Tactic:
rw [satisfies_mk, satisfies_mk]
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ τ ⊨ φ' ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ'

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ τ ⊨ φ' ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ'
Tactic:
exact ⟨hτ, hτ'⟩
State after:
no goals