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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂ → (σ₁ ⊨ φ ↔ σ₂ ⊨ φ)
Tactic:
suffices ∀ {σ₁ σ₂}, σ₁.agreeOn φ.semVars σ₂ → σ₁ ⊨ φ → σ₂ ⊨ φ from
  fun h => ⟨this h, this h.symm⟩
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ ∀ {σ₁ σ₂ : PropAssignment ν}, PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂ → σ₁ ⊨ φ → σ₂ ⊨ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ ∀ {σ₁ σ₂ : PropAssignment ν}, PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂ → σ₁ ⊨ φ → σ₂ ⊨ φ
Tactic:
intro σ₁ σ₂ h h₁
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
⊢ σ₂ ⊨ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
⊢ σ₂ ⊨ φ
Tactic:
by_contra h₂
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
⊢ False

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
⊢ False
Tactic:
have ⟨x, hNe, hMem⟩ := exists_semVar h₁ h₂
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
x : ν
hNe : σ₁ x ≠ σ₂ x
hMem : x ∈ semVars φ
⊢ False

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
x : ν
hNe : σ₁ x ≠ σ₂ x
hMem : x ∈ semVars φ
⊢ False
Tactic:
exact hNe (h x hMem)
State after:
no goals