Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case left
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (units.push l)[↑j] = (⟨↑i, ⋯⟩, b)

case right
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[↑i] = addAssignment b assignments0[↑i] ∧
    hasAssignment b assignments0[↑i] = false ∧
      ∀
        (k :
          Fin
            (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
                else
                  (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                    foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
        ¬k = ⟨↑j, j_lt_updatedUnits_size⟩ → ¬(units.push l)[↑k].fst.val = ↑i
Tactic:
. rw [Array.get_push_lt units l j.1 j.2, h1]
Proof state after:
case right
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[↑i] = addAssignment b assignments0[↑i] ∧
    hasAssignment b assignments0[↑i] = false ∧
      ∀
        (k :
          Fin
            (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
                else
                  (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                    foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
        ¬k = ⟨↑j, j_lt_updatedUnits_size⟩ → ¬(units.push l)[↑k].fst.val = ↑i