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

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

State before:
assignment : Assignment
h : ¬assignment.hasNegAssignment = true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => unassigned
    | both => pos
    | unassigned => unassigned) =
    assignment
Tactic:
rw [hasNegAssignment] at h
State after:
assignment : Assignment
h :
  ¬(match assignment with
      | pos => false
      | neg => true
      | both => true
      | unassigned => false) =
      true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => unassigned
    | both => pos
    | unassigned => unassigned) =
    assignment

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