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

State before:
assignment : Assignment
lacks_pos : ¬assignment.hasPosAssignment = true
lacks_neg : ¬assignment.hasNegAssignment = true
⊢ assignment = unassigned
Tactic:
simp only [hasPosAssignment, Bool.not_eq_true] at lacks_pos
State after:
assignment : Assignment
lacks_neg : ¬assignment.hasNegAssignment = true
lacks_pos :
  (match assignment with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ assignment = unassigned

State before:
assignment : Assignment
lacks_neg : ¬assignment.hasNegAssignment = true
lacks_pos :
  (match assignment with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ assignment = unassigned
Tactic:
split at lacks_pos <;> simp_all (config := { decide := true })
State after:
no goals