Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
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)
h :
  ∀ (i : Fin n),
    (assignments[↑i] = assignments0[↑i] ∧ ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i) ∨
      (∃ j b i_gt_zero,
          units[↑j] = (⟨↑i, ⋯⟩, b) ∧
            assignments[↑i] = addAssignment b assignments0[↑i] ∧
              hasAssignment b assignments0[↑i] = false ∧ ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i) ∨
        ∃ j1 j2 i_gt_zero,
          units[↑j1] = (⟨↑i, ⋯⟩, true) ∧
            units[↑j2] = (⟨↑i, ⋯⟩, false) ∧
              assignments[↑i] = both ∧
                assignments0[↑i] = unassigned ∧ ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
⊢ let update_res := insertUnit (units, assignments, foundContradiction) l;
  let_fun update_res_size := ⋯;
  insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Tactic:
simp only [insertUnit_invariant, Fin.getElem_fin, ne_eq, Bool.not_eq_true]
Proof state after:
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)
h :
  ∀ (i : Fin n),
    (assignments[↑i] = assignments0[↑i] ∧ ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i) ∨
      (∃ j b i_gt_zero,
          units[↑j] = (⟨↑i, ⋯⟩, b) ∧
            assignments[↑i] = addAssignment b assignments0[↑i] ∧
              hasAssignment b assignments0[↑i] = false ∧ ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i) ∨
        ∃ j1 j2 i_gt_zero,
          units[↑j1] = (⟨↑i, ⋯⟩, true) ∧
            units[↑j2] = (⟨↑i, ⋯⟩, false) ∧
              assignments[↑i] = both ∧
                assignments0[↑i] = unassigned ∧ ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
⊢ ∀ (i : Fin n),
    ((insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = assignments0[↑i] ∧
        ∀ (j : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
          ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑j].fst.val = ↑i) ∨
      (∃ j b i_gt_zero,
          (insertUnit (units, assignments, foundContradiction) l).fst[↑j] = (⟨↑i, ⋯⟩, b) ∧
            (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = addAssignment b assignments0[↑i] ∧
              hasAssignment b assignments0[↑i] = false ∧
                ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                  ¬k = j → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i) ∨
        ∃ j1 j2 i_gt_zero,
          (insertUnit (units, assignments, foundContradiction) l).fst[↑j1] = (⟨↑i, ⋯⟩, true) ∧
            (insertUnit (units, assignments, foundContradiction) l).fst[↑j2] = (⟨↑i, ⋯⟩, false) ∧
              (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = both ∧
                assignments0[↑i] = unassigned ∧
                  ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                    ¬k = j1 → ¬k = j2 → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i