internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
rcases Array.foldl_induction motive h_base h_inductive with ⟨_, h⟩
Proof state after:
case 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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
w✝ : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
h :
  f.derivedLits_invariant f_assignments_size
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst w✝
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
case 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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
w✝ : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
h :
  f.derivedLits_invariant f_assignments_size
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst w✝
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
exact h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ motive 0 (f.assignments, [], false, false)
Tactic:
apply Exists.intro f_assignments_size
Proof state after:
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ f.derivedLits_invariant f_assignments_size (f.assignments, [], false, false).fst f_assignments_size
    (f.assignments, [], false, false).snd.fst
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ f.derivedLits_invariant f_assignments_size (f.assignments, [], false, false).fst f_assignments_size
    (f.assignments, [], false, false).snd.fst
Tactic:
intro i
Proof state after:
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (f.assignments, [], false, false).fst[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧
      ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i) ∨
    (∃ j,
        ((f.assignments, [], false, false).snd.fst.get j).fst.val = ↑i ∧
          assignments_i = addAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i ∧
            ¬hasAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i = true ∧
              ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                k ≠ j → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        ((f.assignments, [], false, false).snd.fst.get j1).fst.val = ↑i ∧
          ((f.assignments, [], false, false).snd.fst.get j2).fst.val = ↑i ∧
            ((f.assignments, [], false, false).snd.fst.get j1).snd = true ∧
              ((f.assignments, [], false, false).snd.fst.get j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                      k ≠ j1 → k ≠ j2 → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (f.assignments, [], false, false).fst[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧
      ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i) ∨
    (∃ j,
        ((f.assignments, [], false, false).snd.fst.get j).fst.val = ↑i ∧
          assignments_i = addAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i ∧
            ¬hasAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i = true ∧
              ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                k ≠ j → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        ((f.assignments, [], false, false).snd.fst.get j1).fst.val = ↑i ∧
          ((f.assignments, [], false, false).snd.fst.get j2).fst.val = ↑i ∧
            ((f.assignments, [], false, false).snd.fst.get j1).snd = true ∧
              ((f.assignments, [], false, false).snd.fst.get j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                      k ≠ j1 → k ≠ j2 → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i
Tactic:
apply Or.inl
Proof state after:
case h
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i] ∧
    ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
case h
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i] ∧
    ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Tactic:
constructor
Proof state after:
case h.left
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i]

case h.right
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
case h.left
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i]

case h.right
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Tactic:
. rfl
Proof state after:
case h.right
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
case h.right
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Tactic:
. intro l l_in_nil
  simp only [List.find?, List.not_mem_nil] at l_in_nil
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
case h.left
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i]
Tactic:
rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
case h.right
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Tactic:
intro l l_in_nil
Proof state after:
case h.right
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
l : Literal (PosFin n)
l_in_nil : l ∈ (f.assignments, [], false, false).snd.fst
⊢ l.fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
case h.right
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
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
l : Literal (PosFin n)
l_in_nil : l ∈ (f.assignments, [], false, false).snd.fst
⊢ l.fst.val ≠ ↑i
Tactic:
simp only [List.find?, List.not_mem_nil] at l_in_nil
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
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
⊢ derivedLits_arr[i] ≠ derivedLits_arr[j]
Tactic:
intro li_eq_lj
Proof state after:
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]
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
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]
⊢ False
Tactic:
let li := derivedLits_arr[i]
Proof state after:
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]
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
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]
⊢ False
Tactic:
have li_in_derivedLits : li ∈ derivedLits := by
  have derivedLits_rw : derivedLits = (Array.mk derivedLits).data := by simp only
  simp only [derivedLits_arr_def, li]
  conv => rhs; rw [derivedLits_rw]
  apply Array.getElem_mem_data
Proof state after:
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
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
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
⊢ False
Tactic:
have i_in_bounds : i.1 < derivedLits.length := by
  have i_property := i.2
  simp only [derivedLits_arr_def, Array.size_mk] at i_property
  exact i_property
Proof state after:
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
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
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
⊢ False
Tactic:
have j_in_bounds : j.1 < derivedLits.length := by
  have j_property := j.2
  simp only [derivedLits_arr_def, Array.size_mk] at j_property
  exact j_property
Proof state after:
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
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
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 ∈ derivedLits
Tactic:
have derivedLits_rw : derivedLits = (Array.mk derivedLits).data := by simp only
Proof state after:
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]
derivedLits_rw : derivedLits = { data := derivedLits }.data
⊢ li ∈ derivedLits