Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := f'.assignments[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧ ∀ (j : Fin derivedLits_arr.size), ↑j ≥ 0 → derivedLits_arr[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        ↑j ≥ 0 ∧
          derivedLits_arr[j] = (⟨↑i, ⋯⟩, b) ∧
            assignments_i = addAssignment b fassignments_i ∧
              ¬hasAssignment b fassignments_i = true ∧
                ∀ (k : Fin derivedLits_arr.size), ↑k ≥ 0 → k ≠ j → derivedLits_arr[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        ↑j1 ≥ 0 ∧
          ↑j2 ≥ 0 ∧
            derivedLits_arr[j1] = (⟨↑i, ⋯⟩, true) ∧
              derivedLits_arr[j2] = (⟨↑i, ⋯⟩, false) ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin derivedLits_arr.size), ↑k ≥ 0 → k ≠ j1 → k ≠ j2 → derivedLits_arr[k].fst.val ≠ ↑i
Tactic:
. apply Or.inr ∘ Or.inr
  have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by
    simp only [derivedLits_arr_def, Array.size_mk]
    exact j1.2
  have j2_lt_derivedLits_arr_size : j2.1 < derivedLits_arr.size := by
    simp only [derivedLits_arr_def, Array.size_mk]
    exact j2.2
  have i_gt_zero : i.1 > 0 := by rw [← j1_eq_i]; exact (List.get derivedLits j1).1.2.1
  refine ⟨⟨j1.1, j1_lt_derivedLits_arr_size⟩,
          ⟨j2.1, j2_lt_derivedLits_arr_size⟩,
          i_gt_zero, Nat.zero_le j1.1, Nat.zero_le j2.1, ?_⟩
  constructor
  . simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get, ← j1_eq_i]
    rw [← j1_eq_true]
    rfl
  . constructor
    . simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get, ← j2_eq_i]
      rw [← j2_eq_false]
      rfl
    . apply And.intro h1 ∘ And.intro h2
      intro k _ k_ne_j1 k_ne_j2
      have k_in_bounds : k < derivedLits.length := by
        have k_property := k.2
        simp only [derivedLits_arr_def, Array.size_mk] at k_property
        exact k_property
      have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by
        apply Fin.ne_of_val_ne
        simp only
        exact Fin.val_ne_of_ne k_ne_j1
      have k_ne_j2 : ⟨k.1, k_in_bounds⟩ ≠ j2 := by
        apply Fin.ne_of_val_ne
        simp only
        exact Fin.val_ne_of_ne k_ne_j2
      simp only [Fin.getElem_fin, Array.getElem_eq_data_get, ne_eq, derivedLits_arr_def]
      exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
Proof state after:
no goals