Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
case inr.inl.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k : Fin derivedLits.length
left✝² : (derivedLits.get k).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝¹ :
  (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] =
    addAssignment (derivedLits.get k).snd f.assignments[↑⟨li.fst.val, ⋯⟩]
left✝ : ¬hasAssignment (derivedLits.get k).snd f.assignments[↑⟨li.fst.val, ⋯⟩] = true
h3 : ∀ (k_1 : Fin derivedLits.length), k_1 ≠ k → (derivedLits.get k_1).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
⊢ False
Tactic:
by_cases k.1 = i.1
Proof state after:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k : Fin derivedLits.length
left✝² : (derivedLits.get k).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝¹ :
  (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] =
    addAssignment (derivedLits.get k).snd f.assignments[↑⟨li.fst.val, ⋯⟩]
left✝ : ¬hasAssignment (derivedLits.get k).snd f.assignments[↑⟨li.fst.val, ⋯⟩] = true
h3 : ∀ (k_1 : Fin derivedLits.length), k_1 ≠ k → (derivedLits.get k_1).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
h✝ : ↑k = ↑i
⊢ False

case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k : Fin derivedLits.length
left✝² : (derivedLits.get k).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝¹ :
  (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] =
    addAssignment (derivedLits.get k).snd f.assignments[↑⟨li.fst.val, ⋯⟩]
left✝ : ¬hasAssignment (derivedLits.get k).snd f.assignments[↑⟨li.fst.val, ⋯⟩] = true
h3 : ∀ (k_1 : Fin derivedLits.length), k_1 ≠ k → (derivedLits.get k_1).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
h✝ : ¬↑k = ↑i
⊢ False