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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂ → eval σ₁ φ = eval σ₂ φ
Tactic:
intro h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
⊢ eval σ₁ φ = eval σ₂ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
⊢ eval σ₁ φ = eval σ₂ φ
Tactic:
have := agreeOn_semVars h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
this : σ₁ ⊨ φ ↔ σ₂ ⊨ φ
⊢ eval σ₁ φ = eval σ₂ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
this : σ₁ ⊨ φ ↔ σ₂ ⊨ φ
⊢ eval σ₁ φ = eval σ₂ φ
Tactic:
dsimp only [SemanticEntails.entails, satisfies] at this
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
this : eval σ₁ φ = true ↔ eval σ₂ φ = true
⊢ eval σ₁ φ = eval σ₂ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
this : eval σ₁ φ = true ↔ eval σ₂ φ = true
⊢ eval σ₁ φ = eval σ₂ φ
Tactic:
aesop
State after:
no goals