Theorem: LeanSAT.Model.PropForm.eval_set_of_not_mem_vars (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
⊢ x ∉ vars φ → eval (PropAssignment.set τ x b) φ = eval τ φ
Tactic:
intro hNMem
State after:
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ eval (PropAssignment.set τ x b) φ = eval τ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ eval (PropAssignment.set τ x b) φ = eval τ φ
Tactic:
apply eval_of_agreeOn_vars
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ PropAssignment.agreeOn (↑(vars φ)) (PropAssignment.set τ x b) τ

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ PropAssignment.agreeOn (↑(vars φ)) (PropAssignment.set τ x b) τ
Tactic:
intro y hY
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
y : ν
hY : y ∈ ↑(vars φ)
⊢ PropAssignment.set τ x b y = τ y

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
y : ν
hY : y ∈ ↑(vars φ)
⊢ PropAssignment.set τ x b y = τ y
Tactic:
have : y ≠ x := fun h => hNMem (h ▸ hY)
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
y : ν
hY : y ∈ ↑(vars φ)
this : y ≠ x
⊢ PropAssignment.set τ x b y = τ y

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
y : ν
hY : y ∈ ↑(vars φ)
this : y ≠ x
⊢ PropAssignment.set τ x b y = τ y
Tactic:
simp [PropAssignment.set, this]
State after:
no goals