Theorem: Assignment.addPos_of_addNeg_eq_both (LeanSAT/LRAT/Assignment.lean)

State before:
assignment : Assignment
⊢ assignment.addNegAssignment.addPosAssignment = both
Tactic:
rw [addPosAssignment, addNegAssignment]
State after:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => both
    | both => both
    | unassigned => pos) =
    both

State before:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => both
    | both => both
    | unassigned => pos) =
    both
Tactic:
cases assignment <;> simp
State after:
no goals