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
⊢ c.clause = arr.data
Tactic:
have h_inductive (idx : Fin arr.size) (acc : Option (DefaultClause n)) (ih : motive (idx.1 + 1) acc) :
  motive idx.1 (fold_fn arr[idx] acc) := by
  rcases ih with ⟨idx_add_one_le_arr_size, ih⟩
  apply Exists.intro $ Nat.le_of_succ_le idx_add_one_le_arr_size
  intro c' heq
  simp only [Fin.getElem_fin, fold_fn] at heq
  split at heq
  . simp only at heq
  . 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:
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
h_inductive :
  ∀ (idx : Fin arr.size) (acc : Option (DefaultClause n)), motive (↑idx + 1) acc → motive (↑idx) (fold_fn arr[idx] acc)
⊢ c.clause = arr.data