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

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

State before:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    assignment.hasPosAssignment
Tactic:
cases assignment <;> simp (config := { decide := true })
State after:
no goals