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

State before:
assignment : Assignment
b : Bool
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment 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 → hasAssignment b assignment = true

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

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

case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
. simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
  cases assignment <;> decide
State after:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

State before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
. simp only [Bool.not_eq_true] at hb
  simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
  cases assignment <;> decide
State after:
no goals

State before:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
State after:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ assignment.removeNegAssignment.hasPosAssignment = true → assignment.hasPosAssignment = true

State before:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ assignment.removeNegAssignment.hasPosAssignment = true → assignment.hasPosAssignment = true
Tactic:
cases assignment <;> decide
State after:
no goals

State before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
simp only [Bool.not_eq_true] at hb
State after:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

State before:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
State after:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ ((if (!false) = true then removePosAssignment else removeNegAssignment) assignment).hasNegAssignment = true →
    assignment.hasNegAssignment = true

State before:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ ((if (!false) = true then removePosAssignment else removeNegAssignment) assignment).hasNegAssignment = true →
    assignment.hasNegAssignment = true
Tactic:
cases assignment <;> decide
State after:
no goals