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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v : ν
τ' : PropAssignment ν
⊢ setMany τ {v} τ' = set τ v (τ' v)
Tactic:
ext v
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ setMany τ {v✝} τ' v = set τ v✝ (τ' v✝) v

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ setMany τ {v✝} τ' v = set τ v✝ (τ' v✝) v
Tactic:
simp [setMany, set]
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ (if v = v✝ then τ' v else τ v) = if v = v✝ then τ' v✝ else τ v

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