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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ : Finset ν
τ₁ : PropAssignment ν
xs₂ : Finset ν
τ₂ : PropAssignment ν
⊢ setMany (setMany τ xs₁ τ₁) xs₂ τ₂ = setMany τ (xs₁ ∪ xs₂) (setMany τ₁ xs₂ τ₂)
Tactic:
ext v
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ : Finset ν
τ₁ : PropAssignment ν
xs₂ : Finset ν
τ₂ : PropAssignment ν
v : ν
⊢ setMany (setMany τ xs₁ τ₁) xs₂ τ₂ v = setMany τ (xs₁ ∪ xs₂) (setMany τ₁ xs₂ τ₂) v

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ : Finset ν
τ₁ : PropAssignment ν
xs₂ : Finset ν
τ₂ : PropAssignment ν
v : ν
⊢ setMany (setMany τ xs₁ τ₁) xs₂ τ₂ v = setMany τ (xs₁ ∪ xs₂) (setMany τ₁ xs₂ τ₂) v
Tactic:
simp [setMany]
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ : Finset ν
τ₁ : PropAssignment ν
xs₂ : Finset ν
τ₂ : PropAssignment ν
v : ν
⊢ (if v ∈ xs₂ then τ₂ v else if v ∈ xs₁ then τ₁ v else τ v) =
    if v ∈ xs₁ ∨ v ∈ xs₂ then if v ∈ xs₂ then τ₂ v else τ₁ v else τ v

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