Theorem: LeanSAT.Model.PropAssignment.set_setMany_comm (LeanSAT/Model/PropAssn.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
b : Bool
h : v ∉ xs
⊢ set (setMany τ xs τ') v b = setMany (set τ v b) xs τ'
Tactic:
ext v
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ set (setMany τ xs τ') v✝ b v = setMany (set τ v✝ b) xs τ' v

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ set (setMany τ xs τ') v✝ b v = setMany (set τ v✝ b) xs τ' v
Tactic:
simp [setMany, set]
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ (if v = v✝ then b else if v ∈ xs then τ' v else τ v) = if v ∈ xs then τ' v else if v = v✝ then b else τ v

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ (if v = v✝ then b else if v ∈ xs then τ' v else τ v) = if v ∈ xs then τ' v else if v = v✝ then b else τ v
Tactic:
aesop
State after:
no goals