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

State before:
assignment : Assignment
b : Bool
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
by_cases hb : b
State after:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true

case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true

State before:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true

case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
. have h := not_hasPos_of_removePos assignment
  simp [hb, h, removeAssignment, hasAssignment]
State after:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true

State before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
. have h := not_hasNeg_of_removeNeg assignment
  simp [hb, h, removeAssignment, hasAssignment]
State after:
no goals

State before:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
have h := not_hasPos_of_removePos assignment
State after:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.removePosAssignment.hasPosAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true

State before:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.removePosAssignment.hasPosAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
simp [hb, h, removeAssignment, hasAssignment]
State after:
no goals

State before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
have h := not_hasNeg_of_removeNeg assignment
State after:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.removeNegAssignment.hasNegAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true

State before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.removeNegAssignment.hasNegAssignment = true
⊢ ¬hasAssignment b (removeAssignment b assignment) = true
Tactic:
simp [hb, h, removeAssignment, hasAssignment]
State after:
no goals