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

State before:
assignment : Assignment
b : Bool
⊢ hasAssignment b (addAssignment b assignment) = true
Tactic:
rw [addAssignment, hasAssignment]
State after:
assignment : Assignment
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment)
      ((if b = true then addPosAssignment else addNegAssignment) assignment) =
    true

State before:
assignment : Assignment
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment)
      ((if b = true then addPosAssignment else addNegAssignment) assignment) =
    true
Tactic:
split
State after:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ assignment.addPosAssignment.hasPosAssignment = true

case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true

State before:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ assignment.addPosAssignment.hasPosAssignment = true

case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true
Tactic:
. rw [hasPosAssignment, addPosAssignment]
  cases assignment <;> simp
State after:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true

State before:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true
Tactic:
. rw [hasNegAssignment, addNegAssignment]
  cases assignment <;> simp
State after:
no goals

State before:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ assignment.addPosAssignment.hasPosAssignment = true
Tactic:
rw [hasPosAssignment, addPosAssignment]
State after:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    true

State before:
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    true
Tactic:
cases assignment <;> simp
State after:
no goals

State before:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true
Tactic:
rw [hasNegAssignment, addNegAssignment]
State after:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    true

State before:
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    true
Tactic:
cases assignment <;> simp
State after:
no goals