Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case inr.inl.intro.intro.intro.intro.intro.intro
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
⊢ ((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

case inr.inr.intro.intro.intro.intro.intro.intro.intro
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
j1 j2 : Fin units.size
i_gt_zero : ↑i > 0
h1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
h2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
h3 : assignments[↑i] = both
h4 : assignments0[↑i] = unassigned
h5 : ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
⊢ ((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:
. by_cases hasAssignment l.2 assignments[l.1.1]!
  . next h5 =>
    apply Or.inr ∘ Or.inl
    have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
      simp only [insertUnit, h5, Prod.mk.eta, ite_true]
      exact j.2
    refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
    simp only [insertUnit, h5, Prod.mk.eta, ite_true]
    refine ⟨h1,h2,h3,?_⟩
    intro k k_ne_j
    have k_size : k.1 < units.size := by
      have k_property := k.2
      simp only [insertUnit, h5, Prod.mk.eta, ite_true] at k_property
      exact k_property
    have k_ne_j : { val := k.val, isLt := k_size } ≠ j := by
      intro k_eq_j
      simp only [← Fin.val_eq_of_eq k_eq_j, not_true] at k_ne_j
    exact h4 ⟨k.1, k_size⟩ k_ne_j
  . next h5 =>
    by_cases i.1 = l.1.1
    . next i_eq_l =>
      apply Or.inr ∘ Or.inr
      have units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).1.size := by
        simp only [insertUnit, Prod.mk.eta]
        split
        . contradiction
        . simp only [Array.size_push, Nat.lt_succ_self]
      let mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).1.size :=
        ⟨units.size, units_size_lt_updatedUnits_size⟩
      have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
        simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.size_push]
        exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size)
      match hb : b, hl : l.2 with
      | true, true =>
        exfalso
        have assignments_i_rw : assignments[i.1]! = assignments[i.1] := by
          simp only [getElem!, i_in_bounds, ↓reduceDite, Array.get_eq_getElem]
        rw [hl, ← i_eq_l, assignments_i_rw, h2] at h5
        exact h5 (has_of_add _ true)
      | true, false =>
        refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩
        simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.get_push_eq, ne_eq]
        constructor
        . rw [Array.get_push_lt units l j.1 j.2, h1]
        . constructor
          . simp only [i_eq_l, ← hl]
            apply Prod.mk.eta
          . constructor
            . simp only [i_eq_l]
              rw [Array.get_modify_at_idx l_in_bounds]
              simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
              apply addNeg_of_addPos_eq_both
            . constructor
              . match h : assignments0[i.val]'_ with
                | unassigned => rfl
                | pos => simp (config := {decide := true}) [h] at h3
                | neg =>
                  simp only [addAssignment, addPosAssignment, h, ite_true] at h2
                  simp only [i_eq_l] at h2
                  simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasNegAssignment] at h5
                | both => simp (config := {decide := true}) only [h] at h3
              . intro k k_ne_j k_ne_l
                rw [Array.get_push]
                by_cases h : k.1 < units.size
                . simp only [h, dite_true]
                  have k_ne_j : ⟨k.1, h⟩ ≠ j := by
                    intro k_eq_j
                    simp only [← k_eq_j, not_true] at k_ne_j
                  exact h4 ⟨k.1, h⟩ k_ne_j
                . exfalso
                  have k_property := k.2
                  simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.size_push] at k_property
                  rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                  . exact h k_lt_units_size
                  . simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
                    exact k_ne_l rfl
      | false, true =>
        refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩
        simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.get_push_eq, ne_eq]
        constructor
        . simp only [i_eq_l, ← hl]
          apply Prod.mk.eta
        . constructor
          . rw [Array.get_push_lt units l j.1 j.2, h1]
          . constructor
            . simp only [i_eq_l]
              rw [Array.get_modify_at_idx l_in_bounds]
              simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
              apply addPos_of_addNeg_eq_both
            . constructor
              . match h : assignments0[i.val]'_ with
                | unassigned => rfl
                | pos =>
                  simp only [addAssignment, h, ite_false, addNegAssignment] at h2
                  simp only [i_eq_l] at h2
                  simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasPosAssignment] at h5
                | neg  => simp (config := {decide := true}) only [h] at h3
                | both => simp (config := {decide := true}) only [h] at h3
              . intro k k_ne_l k_ne_j
                rw [Array.get_push]
                by_cases h : k.1 < units.size
                . simp only [h, dite_true]
                  have k_ne_j : ⟨k.1, h⟩ ≠ j := by
                    intro k_eq_j
                    simp only [← k_eq_j, not_true] at k_ne_j
                  exact h4 ⟨k.1, h⟩ k_ne_j
                . exfalso
                  have k_property := k.2
                  simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.size_push] at k_property
                  rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                  . exact h k_lt_units_size
                  . simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
                    exact k_ne_l rfl
      | false, false =>
        exfalso
        have assignments_i_rw : assignments[i.1]! = assignments[i.1] := by
          simp [getElem!, i_in_bounds]
        rw [hl, ← i_eq_l, assignments_i_rw, h2] at h5
        exact h5 (has_of_add _ false)
    . next i_ne_l =>
      apply Or.inr ∘ Or.inl
      have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
        simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.size_push]
        exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size)
      refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
      simp only [insertUnit, h5, Prod.mk.eta, ite_false]
      constructor
      . rw [Array.get_push_lt units l j.1 j.2, h1]
      . constructor
        . rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l), h2]
        . constructor
          . exact h3
          . intro k k_ne_j
            rw [Array.get_push]
            by_cases h : k.val < units.size
            . simp only [h, dite_true]
              have k_ne_j : ⟨k.1, h⟩ ≠ j := by
                intro k_eq_j
                simp only [← Fin.val_eq_of_eq k_eq_j, not_true] at k_ne_j
              exact h4 ⟨k.1, h⟩ k_ne_j
            . simp only [h, dite_false]
              exact Ne.symm i_ne_l
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro
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
j1 j2 : Fin units.size
i_gt_zero : ↑i > 0
h1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
h2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
h3 : assignments[↑i] = both
h4 : assignments0[↑i] = unassigned
h5 : ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
⊢ ((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