-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem remove_add_cancel {assignment : Assignment} {b : Bool} (h : ¬(hasAssignment b assignment)) :
  removeAssignment b (addAssignment b assignment) = assignment

Proof state:
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]

Result:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ (if false = true then removePosAssignment else removeNegAssignment)
      ((if false = true then addPosAssignment else addNegAssignment) assignment) =
    assignment

Proof state:
case neg
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : ¬b = true
⊢ (if false = true then removePosAssignment else removeNegAssignment)
      ((if false = true then addPosAssignment else addNegAssignment) assignment) =
    assignment

Tactic:
simp only [hasAssignment, hb, ite_false] at h

Result:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬(if false = true then hasPosAssignment else hasNegAssignment) assignment = true
⊢ (if false = true then removePosAssignment else removeNegAssignment)
      ((if false = true then addPosAssignment else addNegAssignment) assignment) =
    assignment

Proof state:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
h : ¬(if false = true then hasPosAssignment else hasNegAssignment) assignment = true
⊢ (if false = true then removePosAssignment else removeNegAssignment)
      ((if false = true then addPosAssignment else addNegAssignment) assignment) =
    assignment

Tactic:
exact removeNeg_addNeg_cancel h

Result:
no goals

Proof state:
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

Result:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.hasPosAssignment = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment

Proof state:
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
⊢ removeAssignment b (addAssignment b assignment) = assignment

Tactic:
by_cases hb : b

Result:
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

Proof state:
case pos
assignment : Assignment
b : Bool
hb : b = true
h : ¬assignment.hasPosAssignment = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment

Tactic:
exact removePos_addPos_cancel h

Result:
no goals

Proof state:
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]

Result:
case pos
assignment : Assignment
b : Bool
h : ¬hasAssignment b assignment = true
hb : b = true
⊢ assignment.addPosAssignment.removePosAssignment = assignment