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
⊢ ∀ (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
Tactic:
intro i
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