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