Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
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:
. have j1_lt_updatedUnits_size : j1.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
    simp only [insertUnit, Prod.mk.eta]
    split
    . exact j1.2
    . simp only [Array.size_push]
      exact Nat.lt_trans j1.2 (Nat.lt_succ_self units.size)
  have j2_lt_updatedUnits_size : j2.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
    simp only [insertUnit, Prod.mk.eta]
    split
    . exact j2.2
    . simp only [Array.size_push]
      exact Nat.lt_trans j2.2 (Nat.lt_succ_self units.size)
  refine Or.inr <| Or.inr <| ⟨⟨j1.1, j1_lt_updatedUnits_size⟩, ⟨j2.1, j2_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩
  simp only [insertUnit, Prod.mk.eta]
  constructor
  . split
    . exact h1
    . simp only [Array.get_push_lt units l j1.1 j1.2, h1]
  . constructor
    . split
      . exact h2
      . simp only [Array.get_push_lt units l j2.1 j2.2, h2]
    . constructor
      . split
        . exact h3
        . simp only
          by_cases i.1 = l.1.1
          . next i_eq_l =>
            simp only [i_eq_l]
            rw [Array.get_modify_at_idx l_in_bounds]
            simp only [← i_eq_l, h3, add_of_both_eq_both]
          . next i_ne_l => rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l), h3]
      . constructor
        . exact h4
        . intro k k_ne_j1 k_ne_j2
          by_cases k.1 < units.size
          . next k_in_bounds =>
            have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by
              intro k_eq_j1
              simp only [← k_eq_j1, not_true] at k_ne_j1
            have k_ne_j2 : ⟨k.1, k_in_bounds⟩ ≠ j2 := by
              intro k_eq_j2
              simp only [← k_eq_j2, not_true] at k_ne_j2
            split
            . exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
            . simp only [ne_eq]
              rw [Array.get_push]
              simp only [k_in_bounds, dite_true]
              exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
          . next k_not_lt_units_size =>
            split
            . next h =>
              exfalso
              have k_property := k.2
              simp only [insertUnit, h, Prod.mk.eta, ite_true] at k_property
              exact k_not_lt_units_size k_property
            . next h =>
              simp only
              have k_eq_units_size : k.1 = units.size := by
                have k_property := k.2
                simp only [insertUnit, h, 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
                . exfalso; exact k_not_lt_units_size k_lt_units_size
                . exact k_eq_units_size
              simp only [k_eq_units_size, Array.get_push_eq, ne_eq]
              intro l_eq_i
              simp [getElem!, l_eq_i, i_in_bounds, h3, has_of_both] at h
Proof state after:
no goals