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

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

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

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

case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Tactic:
. simp only [removeAssignment, hb, addAssignment, ite_true]
  simp only [hasAssignment, hb, ite_true] at h
  exact removePos_addPos_cancel h
State after:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment

State before:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Tactic:
. simp only [removeAssignment, hb, addAssignment, ite_true]
  simp only [hasAssignment, hb, ite_false] at h
  exact removeNeg_addNeg_cancel h
State after:
no goals

State before:
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Tactic:
simp only [removeAssignment, hb, addAssignment, ite_true]
State after:
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment

State before:
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment
Tactic:
simp only [hasAssignment, hb, ite_true] at h
State after:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.hasPosAssignment = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment

State before:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.hasPosAssignment = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment
Tactic:
exact removePos_addPos_cancel h
State after:
no goals

State before:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ removeAssignment b (addAssignment b assignment) = assignment
Tactic:
simp only [removeAssignment, hb, addAssignment, ite_true]
State after:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment

State before:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment
Tactic:
simp only [hasAssignment, hb, ite_false] at h
State after:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.hasNegAssignment = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment

State before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬assignment.hasNegAssignment = true
⊢ (if False then removePosAssignment else removeNegAssignment)
      ((if False then addPosAssignment else addNegAssignment) assignment) =
    assignment
Tactic:
exact removeNeg_addNeg_cancel h
State after:
no goals