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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
⊢ agreeOn (↑xs)ᶜ (setMany τ xs τ') τ
Tactic:
apply agreeOn_setMany_of_disjoint
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
⊢ Disjoint (↑xs)ᶜ ↑xs

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
⊢ Disjoint (↑xs)ᶜ ↑xs
Tactic:
exact disjoint_compl_left
State after:
no goals