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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
⊢ agreeOn (↑xs) (setMany τ xs τ') τ'
Tactic:
intro v hv
State after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
hv : v ∈ ↑xs
⊢ setMany τ xs τ' v = τ' v

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
hv : v ∈ ↑xs
⊢ setMany τ xs τ' v = τ' v
Tactic:
simp at hv
State after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
hv : v ∈ xs
⊢ setMany τ xs τ' v = τ' v

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
hv : v ∈ xs
⊢ setMany τ xs τ' v = τ' v
Tactic:
simp [setMany, hv]
State after:
no goals