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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
⊢ semVars φᶜ = semVars φ
Tactic:
ext x
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ x ∈ semVars φᶜ ↔ x ∈ semVars φ

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ x ∈ semVars φᶜ ↔ x ∈ semVars φ
Tactic:
simp only [mem_semVars]
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ) ↔ ∃ τ, τ ⊨ φ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ) ↔ ∃ τ, τ ⊨ φ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
constructor <;> {
  intro ⟨τ, hτ, hτ'⟩
  simp only [satisfies_neg, not_not] at hτ hτ' ⊢
  let τ' := τ.set x (!τ x)
  have : (!τ' x) = τ x := by
    simp only [τ', τ.set_get x, Bool.not_not]
  refine ⟨τ', hτ', ?_⟩
  rw [τ.set_set, this, τ.set_same]
  exact hτ
}
State after:
no goals

State before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ) → ∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ
Tactic:
intro ⟨τ, hτ, hτ'⟩
State after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ ∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ

State before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ ∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ
Tactic:
simp only [satisfies_neg, not_not] at hτ hτ' ⊢
State after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ

State before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
let τ' := τ.set x (!τ x)
State after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ

State before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
have : (!τ' x) = τ x := by
  simp only [τ', τ.set_get x, Bool.not_not]
State after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ

State before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
refine ⟨τ', hτ', ?_⟩
State after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ (PropAssignment.set τ' x !τ' x) ⊨ φ

State before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ (PropAssignment.set τ' x !τ' x) ⊨ φ
Tactic:
rw [τ.set_set, this, τ.set_same]
State after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ τ ⊨ φ

State before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ τ ⊨ φ
Tactic:
exact hτ
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
⊢ (!τ' x) = τ x
Tactic:
simp only [τ', τ.set_get x, Bool.not_not]
State after:
no goals