internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
acc : Option (DefaultClause n)
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
ih :
  ∀ (c' : DefaultClause n),
    acc = some c' →
      ∃ hsize,
        ∀ (i : Fin c'.clause.length),
          let_fun idx_in_bounds := ⋯;
          c'.clause.get i = arr[↑idx + 1 + ↑i]
c' : DefaultClause n
heq : fold_fn arr[idx] acc = some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
simp only [Fin.getElem_fin, fold_fn] at heq
Proof state after:
case intro
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
acc : Option (DefaultClause n)
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
ih :
  ∀ (c' : DefaultClause n),
    acc = some c' →
      ∃ hsize,
        ∀ (i : Fin c'.clause.length),
          let_fun idx_in_bounds := ⋯;
          c'.clause.get i = arr[↑idx + 1 + ↑i]
c' : DefaultClause n
heq :
  (match acc with
    | none => none
    | some acc => acc.insert arr[↑idx]) =
    some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.h_2
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝¹ : Option (DefaultClause n)
acc✝ : DefaultClause n
ih :
  ∀ (c' : DefaultClause n),
    some acc✝ = some c' →
      ∃ hsize,
        ∀ (i : Fin c'.clause.length),
          let_fun idx_in_bounds := ⋯;
          c'.clause.get i = arr[↑idx + 1 + ↑i]
heq : acc✝.insert arr[↑idx] = some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
. next acc =>
  specialize ih acc rfl
  rcases ih with ⟨hsize, ih⟩
  simp only at ih
  simp only [insert] at heq
  split at heq
  . exact False.elim heq
  . split at heq
    . next h_dup =>
      exfalso simp only [List.contains] at h_dup
      rcases List.get_of_mem $ List.mem_of_elem_eq_true h_dup with ⟨j, hj⟩
      specialize ih j
      rw [hj] at ih
      have idx_add_one_add_j_in_bounds : idx.1 + 1 + j.1 < arr.size := by
        omega
      have idx_ne_idx_add_one_add_j_in_bounds : idx.1 ≠ idx.1 + 1 + j.1 := by
        omega
      exact arrNodup idx ⟨idx.1 + 1 + j.1, idx_add_one_add_j_in_bounds⟩ idx_ne_idx_add_one_add_j_in_bounds ih
    . simp only [Option.some.injEq] at heq
      have hsize' : c'.clause.length = arr.size - idx.1 := by
        simp only [← heq, List.length_cons, hsize]
        rw [Nat.succ_eq_add_one, Nat.sub_add_eq, Nat.sub_add_cancel]
        apply Nat.le_sub_of_add_le
        rw [Nat.add_comm]
        exact idx_add_one_le_arr_size
      apply Exists.intro hsize'
      intro i
      simp only
      have lhs_rw : c'.clause = arr[idx.1] :: acc.clause := by rw [← heq]
      simp only [List.get_of_eq lhs_rw]
      by_cases i.1 = 0
      . next i_eq_zero =>
        simp only [List.length_cons, i_eq_zero, List.get, Nat.add_zero]
      . next i_ne_zero =>
        rcases Nat.exists_eq_succ_of_ne_zero i_ne_zero with ⟨j, hj⟩
        simp only [List.length_cons, hj, List.get, Nat.succ_eq_add_one]
        simp only [Nat.add_comm j 1, ← Nat.add_assoc]
        exact ih ⟨j, by omega⟩
Proof state after:
no goals
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.h_1
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
ih :
  ∀ (c' : DefaultClause n),
    none = some c' →
      ∃ hsize,
        ∀ (i : Fin c'.clause.length),
          let_fun idx_in_bounds := ⋯;
          c'.clause.get i = arr[↑idx + 1 + ↑i]
heq : none = some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
simp only at heq
Proof state after:
no goals
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.h_2
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝¹ : Option (DefaultClause n)
acc✝ : DefaultClause n
ih :
  ∀ (c' : DefaultClause n),
    some acc✝ = some c' →
      ∃ hsize,
        ∀ (i : Fin c'.clause.length),
          let_fun idx_in_bounds := ⋯;
          c'.clause.get i = arr[↑idx + 1 + ↑i]
heq : acc✝.insert arr[↑idx] = some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
next acc =>
specialize ih acc rfl
rcases ih with ⟨hsize, ih⟩
simp only at ih
simp only [insert] at heq
split at heq
. exact False.elim heq
. split at heq
  . next h_dup =>
    exfalso simp only [List.contains] at h_dup
    rcases List.get_of_mem $ List.mem_of_elem_eq_true h_dup with ⟨j, hj⟩
    specialize ih j
    rw [hj] at ih
    have idx_add_one_add_j_in_bounds : idx.1 + 1 + j.1 < arr.size := by
      omega
    have idx_ne_idx_add_one_add_j_in_bounds : idx.1 ≠ idx.1 + 1 + j.1 := by
      omega
    exact arrNodup idx ⟨idx.1 + 1 + j.1, idx_add_one_add_j_in_bounds⟩ idx_ne_idx_add_one_add_j_in_bounds ih
  . simp only [Option.some.injEq] at heq
    have hsize' : c'.clause.length = arr.size - idx.1 := by
      simp only [← heq, List.length_cons, hsize]
      rw [Nat.succ_eq_add_one, Nat.sub_add_eq, Nat.sub_add_cancel]
      apply Nat.le_sub_of_add_le
      rw [Nat.add_comm]
      exact idx_add_one_le_arr_size
    apply Exists.intro hsize'
    intro i
    simp only
    have lhs_rw : c'.clause = arr[idx.1] :: acc.clause := by rw [← heq]
    simp only [List.get_of_eq lhs_rw]
    by_cases i.1 = 0
    . next i_eq_zero =>
      simp only [List.length_cons, i_eq_zero, List.get, Nat.add_zero]
    . next i_ne_zero =>
      rcases Nat.exists_eq_succ_of_ne_zero i_ne_zero with ⟨j, hj⟩
      simp only [List.length_cons, hj, List.get, Nat.succ_eq_add_one]
      simp only [Nat.add_comm j 1, ← Nat.add_assoc]
      exact ih ⟨j, by omega⟩
Proof state after:
no goals
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
ih :
  ∀ (c' : DefaultClause n),
    some acc = some c' →
      ∃ hsize,
        ∀ (i : Fin c'.clause.length),
          let_fun idx_in_bounds := ⋯;
          c'.clause.get i = arr[↑idx + 1 + ↑i]
heq : acc.insert arr[↑idx] = some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
specialize ih acc rfl
Proof state after:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
heq : acc.insert arr[↑idx] = some c'
ih :
  ∃ hsize,
    ∀ (i : Fin acc.clause.length),
      let_fun idx_in_bounds := ⋯;
      acc.clause.get i = arr[↑idx + 1 + ↑i]
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
heq : acc.insert arr[↑idx] = some c'
ih :
  ∃ hsize,
    ∀ (i : Fin acc.clause.length),
      let_fun idx_in_bounds := ⋯;
      acc.clause.get i = arr[↑idx + 1 + ↑i]
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
rcases ih with ⟨hsize, ih⟩
Proof state after:
case intro
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
heq : acc.insert arr[↑idx] = some c'
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih :
  ∀ (i : Fin acc.clause.length),
    let_fun idx_in_bounds := ⋯;
    acc.clause.get i = arr[↑idx + 1 + ↑i]
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
heq : acc.insert arr[↑idx] = some c'
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih :
  ∀ (i : Fin acc.clause.length),
    let_fun idx_in_bounds := ⋯;
    acc.clause.get i = arr[↑idx + 1 + ↑i]
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
simp only at ih
Proof state after:
case intro
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
heq : acc.insert arr[↑idx] = some c'
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
heq : acc.insert arr[↑idx] = some c'
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
simp only [insert] at heq
Proof state after:
case intro
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
heq :
  (if h : acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true then none
    else
      if h : acc.clause.contains arr[↑idx] = true then some acc
      else some { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ }) =
    some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.isFalse
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
h✝ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
heq :
  (if h : acc.clause.contains arr[↑idx] = true then some acc
    else some { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ }) =
    some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
. split at heq
  . next h_dup =>
    exfalso simp only [List.contains] at h_dup
    rcases List.get_of_mem $ List.mem_of_elem_eq_true h_dup with ⟨j, hj⟩
    specialize ih j
    rw [hj] at ih
    have idx_add_one_add_j_in_bounds : idx.1 + 1 + j.1 < arr.size := by
      omega
    have idx_ne_idx_add_one_add_j_in_bounds : idx.1 ≠ idx.1 + 1 + j.1 := by
      omega
    exact arrNodup idx ⟨idx.1 + 1 + j.1, idx_add_one_add_j_in_bounds⟩ idx_ne_idx_add_one_add_j_in_bounds ih
  . simp only [Option.some.injEq] at heq
    have hsize' : c'.clause.length = arr.size - idx.1 := by
      simp only [← heq, List.length_cons, hsize]
      rw [Nat.succ_eq_add_one, Nat.sub_add_eq, Nat.sub_add_cancel]
      apply Nat.le_sub_of_add_le
      rw [Nat.add_comm]
      exact idx_add_one_le_arr_size
    apply Exists.intro hsize'
    intro i
    simp only
    have lhs_rw : c'.clause = arr[idx.1] :: acc.clause := by rw [← heq]
    simp only [List.get_of_eq lhs_rw]
    by_cases i.1 = 0
    . next i_eq_zero =>
      simp only [List.length_cons, i_eq_zero, List.get, Nat.add_zero]
    . next i_ne_zero =>
      rcases Nat.exists_eq_succ_of_ne_zero i_ne_zero with ⟨j, hj⟩
      simp only [List.length_cons, hj, List.get, Nat.succ_eq_add_one]
      simp only [Nat.add_comm j 1, ← Nat.add_assoc]
      exact ih ⟨j, by omega⟩
Proof state after:
no goals