Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success (LeanSAT/LRAT/Formula/RupAddSound.lean)

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < assignments.size
Tactic:
rw [assignments_size]
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < n

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < n
Tactic:
exact i.2.2
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < insertUnit_res.snd.fst.size
Tactic:
rw [insertUnit_preserves_size, assignments_size]
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < n

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < n
Tactic:
exact j.2.2
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
⊢ let insertUnit_res := insertUnit (units, assignments, foundContradiction) l;
  (foundContradiction = true → ∃ i, assignments[i.val] = both) →
    insertUnit_res.snd.snd = true → ∃ j, insertUnit_res.snd.fst[j.val] = both
Tactic:
intro insertUnit_res h insertUnit_success
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success : insertUnit_res.snd.snd = true
⊢ ∃ j, insertUnit_res.snd.fst[j.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success : insertUnit_res.snd.snd = true
⊢ ∃ j, insertUnit_res.snd.fst[j.val] = both
Tactic:
simp only [insertUnit_res] at *
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success : (insertUnit (units, assignments, foundContradiction) l).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success : (insertUnit (units, assignments, foundContradiction) l).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
simp only [insertUnit, Prod.mk.eta] at insertUnit_success
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
have l_in_bounds : l.1.1 < assignments.size := by rw [assignments_size]; exact l.1.2.2
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
l_in_bounds : l.fst.val < assignments.size
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
l_in_bounds : l.fst.val < assignments.size
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
split at insertUnit_success
State after:
case isTrue
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

case isFalse
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

State before:
case isTrue
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

case isFalse
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
. next hl =>
  simp only [insertUnit, hl, Prod.mk.eta, ite_true]
  exact h insertUnit_success
State after:
case isFalse
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

State before:
case isFalse
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
. next hl =>
  simp only [Bool.or_eq_true] at insertUnit_success
  rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
  . simp only [insertUnit, hl, Prod.mk.eta, ite_false]
    rcases h foundContradiction_eq_true with ⟨i, h⟩
    have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
    apply Exists.intro i
    by_cases l.1.1 = i.1
    . next l_eq_i =>
      simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
      exact add_of_both_eq_both l.2
    . next l_ne_i =>
      rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
      exact h
  . apply Exists.intro l.1
    simp only [insertUnit, hl, Prod.mk.eta, ite_false, Array.get_modify_at_idx l_in_bounds]
    simp only [getElem!, l_in_bounds, dite_true] at assignments_l_ne_unassigned
    by_cases l.2
    . next l_eq_true =>
      rw [l_eq_true]
      simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
        Bool.not_eq_true] at hl
      split at hl <;> simp_all (config := { decide := true })
    . next l_eq_false =>
      simp only [Bool.not_eq_true] at l_eq_false
      rw [l_eq_false]
      simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
        Bool.not_eq_true] at hl
      split at hl <;> simp_all (config := { decide := true })
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ l.fst.val < assignments.size
Tactic:
rw [assignments_size]
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ l.fst.val < n

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ l.fst.val < n
Tactic:
exact l.1.2.2
State after:
no goals

State before:
case isTrue
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
next hl =>
simp only [insertUnit, hl, Prod.mk.eta, ite_true]
exact h insertUnit_success
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
simp only [insertUnit, hl, Prod.mk.eta, ite_true]
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, assignments[j.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, assignments[j.val] = both
Tactic:
exact h insertUnit_success
State after:
no goals

State before:
case isFalse
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
next hl =>
simp only [Bool.or_eq_true] at insertUnit_success
rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
. simp only [insertUnit, hl, Prod.mk.eta, ite_false]
  rcases h foundContradiction_eq_true with ⟨i, h⟩
  have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
  apply Exists.intro i
  by_cases l.1.1 = i.1
  . next l_eq_i =>
    simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
    exact add_of_both_eq_both l.2
  . next l_ne_i =>
    rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
    exact h
. apply Exists.intro l.1
  simp only [insertUnit, hl, Prod.mk.eta, ite_false, Array.get_modify_at_idx l_in_bounds]
  simp only [getElem!, l_in_bounds, dite_true] at assignments_l_ne_unassigned
  by_cases l.2
  . next l_eq_true =>
    rw [l_eq_true]
    simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
      Bool.not_eq_true] at hl
    split at hl <;> simp_all (config := { decide := true })
  . next l_eq_false =>
    simp only [Bool.not_eq_true] at l_eq_false
    rw [l_eq_false]
    simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
      Bool.not_eq_true] at hl
    split at hl <;> simp_all (config := { decide := true })
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
simp only [Bool.or_eq_true] at insertUnit_success
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : foundContradiction = true ∨ (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : foundContradiction = true ∨ (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
State after:
case inl
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

State before:
case inl
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
. simp only [insertUnit, hl, Prod.mk.eta, ite_false]
  rcases h foundContradiction_eq_true with ⟨i, h⟩
  have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
  apply Exists.intro i
  by_cases l.1.1 = i.1
  . next l_eq_i =>
    simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
    exact add_of_both_eq_both l.2
  . next l_ne_i =>
    rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
    exact h
State after:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

State before:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
. apply Exists.intro l.1
  simp only [insertUnit, hl, Prod.mk.eta, ite_false, Array.get_modify_at_idx l_in_bounds]
  simp only [getElem!, l_in_bounds, dite_true] at assignments_l_ne_unassigned
  by_cases l.2
  . next l_eq_true =>
    rw [l_eq_true]
    simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
      Bool.not_eq_true] at hl
    split at hl <;> simp_all (config := { decide := true })
  . next l_eq_false =>
    simp only [Bool.not_eq_true] at l_eq_false
    rw [l_eq_false]
    simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
      Bool.not_eq_true] at hl
    split at hl <;> simp_all (config := { decide := true })
State after:
no goals

State before:
case inl
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
simp only [insertUnit, hl, Prod.mk.eta, ite_false]
State after:
case inl
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both

State before:
case inl
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both
Tactic:
rcases h foundContradiction_eq_true with ⟨i, h⟩
State after:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both

State before:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both
Tactic:
have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
State after:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both

State before:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both
Tactic:
apply Exists.intro i
State after:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both

State before:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
by_cases l.1.1 = i.1
State after:
case pos
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both

case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both

State before:
case pos
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both

case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
. next l_eq_i =>
  simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
  exact add_of_both_eq_both l.2
State after:
case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both

State before:
case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
. next l_ne_i =>
  rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
  exact h
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ i.val < assignments.size
Tactic:
rw [assignments_size]
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ i.val < n

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ i.val < n
Tactic:
exact i.2.2
State after:
no goals

State before:
case pos
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
next l_eq_i =>
simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
exact add_of_both_eq_both l.2
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_eq_i : l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_eq_i : l.fst.val = i.val
⊢ addAssignment l.snd both = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_eq_i : l.fst.val = i.val
⊢ addAssignment l.snd both = both
Tactic:
exact add_of_both_eq_both l.2
State after:
no goals

State before:
case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
next l_ne_i =>
rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
exact h
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_ne_i : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_ne_i : ¬l.fst.val = i.val
⊢ assignments[i.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_ne_i : ¬l.fst.val = i.val
⊢ assignments[i.val] = both
Tactic:
exact h
State after:
no goals

State before:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
apply Exists.intro l.1
State after:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ (insertUnit (units, assignments, foundContradiction) l).snd.fst[l.fst.val] = both

State before:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ (insertUnit (units, assignments, foundContradiction) l).snd.fst[l.fst.val] = both
Tactic:
simp only [insertUnit, hl, Prod.mk.eta, ite_false, Array.get_modify_at_idx l_in_bounds]
State after:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

State before:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
simp only [getElem!, l_in_bounds, dite_true] at assignments_l_ne_unassigned
State after:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

State before:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
by_cases l.2
State after:
case pos
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

State before:
case pos
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
. next l_eq_true =>
  rw [l_eq_true]
  simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
    Bool.not_eq_true] at hl
  split at hl <;> simp_all (config := { decide := true })
State after:
case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

State before:
case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
. next l_eq_false =>
  simp only [Bool.not_eq_true] at l_eq_false
  rw [l_eq_false]
  simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
    Bool.not_eq_true] at hl
  split at hl <;> simp_all (config := { decide := true })
State after:
no goals

State before:
case pos
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
next l_eq_true =>
rw [l_eq_true]
simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
  Bool.not_eq_true] at hl
split at hl <;> simp_all (config := { decide := true })
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
rw [l_eq_true]
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
⊢ addAssignment true assignments[l.fst.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
⊢ addAssignment true assignments[l.fst.val] = both
Tactic:
simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
  Bool.not_eq_true] at hl
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
hl :
  (match assignments.get ⟨l.fst.val, ⋯⟩ with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment true assignments[l.fst.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
hl :
  (match assignments.get ⟨l.fst.val, ⋯⟩ with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment true assignments[l.fst.val] = both
Tactic:
split at hl <;> simp_all (config := { decide := true })
State after:
no goals

State before:
case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
next l_eq_false =>
simp only [Bool.not_eq_true] at l_eq_false
rw [l_eq_false]
simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
  Bool.not_eq_true] at hl
split at hl <;> simp_all (config := { decide := true })
State after:
no goals

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
simp only [Bool.not_eq_true] at l_eq_false
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment l.snd assignments[l.fst.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
rw [l_eq_false]
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment false assignments[l.fst.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment false assignments[l.fst.val] = both
Tactic:
simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
  Bool.not_eq_true] at hl
State after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
hl :
  (match assignments.get ⟨l.fst.val, ⋯⟩ with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment false assignments[l.fst.val] = both

State before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
hl :
  (match assignments.get ⟨l.fst.val, ⋯⟩ with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment false assignments[l.fst.val] = both
Tactic:
split at hl <;> simp_all (config := { decide := true })
State after:
no goals