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

State before:
assignment : Assignment
b : Bool
⊢ hasAssignment b assignment = true ↔ hasAssignment b (addAssignment (decide ¬b = true) assignment) = true
Tactic:
by_cases hb : b <;> simp [hb, hasAssignment, addAssignment, hasPos_of_addNeg, hasNeg_of_addPos]
State after:
no goals