internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.a.a
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)
hsize : c.clause.length = arr.size - 0
h :
  ∀ (i : Fin c.clause.length),
    let_fun idx_in_bounds := ⋯;
    c.clause.get i = arr[0 + ↑i]
n✝ : Nat
a✝ : Literal (PosFin n)
⊢ a✝ ∈ c.clause.get? n✝ ↔ a✝ ∈ arr.data.get? n✝
Tactic:
next i l =>
by_cases i_in_bounds : i < c.clause.length
. specialize h ⟨i, i_in_bounds⟩
  simp only at h
  have i_in_bounds' : i < arr.data.length := by
    dsimp; omega
  rw [List.get?_eq_get i_in_bounds, List.get?_eq_get i_in_bounds']
  simp only [h, Nat.zero_add, Array.getElem_eq_data_get, Option.mem_def, Option.some.injEq]
. have arr_data_length_le_i : arr.data.length ≤ i := by
    dsimp; omega
  simp only [Nat.not_lt, ← List.get?_eq_none] at i_in_bounds arr_data_length_le_i
  rw [i_in_bounds, arr_data_length_le_i]
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
idx : Nat
acc : Option (DefaultClause n)
idx_le_arr_size : idx ≤ arr.size
c' : DefaultClause n
hsize : c'.clause.length = arr.size - idx
i : Fin c'.clause.length
⊢ idx + ↑i < arr.size
Tactic:
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]
⊢ motive arr.size (some empty)
Tactic:
apply Exists.intro $ Nat.le_refl arr.size
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]
⊢ ∀ (c' : DefaultClause n),
    some empty = some c' →
      ∃ hsize,
        ∀ (i : Fin c'.clause.length),
          let_fun idx_in_bounds := ⋯;
          c'.clause.get i = arr[arr.size + ↑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]
⊢ ∀ (c' : DefaultClause n),
    some empty = some c' →
      ∃ hsize,
        ∀ (i : Fin c'.clause.length),
          let_fun idx_in_bounds := ⋯;
          c'.clause.get i = arr[arr.size + ↑i]
Tactic:
intro c' heq
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]
c' : DefaultClause n
heq : some empty = some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[arr.size + ↑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]
c' : DefaultClause n
heq : some empty = some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[arr.size + ↑i]
Tactic:
simp only [Option.some.injEq] at heq
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]
c' : DefaultClause n
heq : empty = c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[arr.size + ↑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]
c' : DefaultClause n
heq : empty = c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[arr.size + ↑i]
Tactic:
have hsize : List.length c'.clause = arr.size- arr.size := by
  simp [← heq, empty]
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]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[arr.size + ↑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]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[arr.size + ↑i]
Tactic:
apply Exists.intro hsize
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]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
⊢ ∀ (i : Fin c'.clause.length),
    let_fun idx_in_bounds := ⋯;
    c'.clause.get i = arr[arr.size + ↑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]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
⊢ ∀ (i : Fin c'.clause.length),
    let_fun idx_in_bounds := ⋯;
    c'.clause.get i = arr[arr.size + ↑i]
Tactic:
intro i
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]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
i : Fin c'.clause.length
⊢ let_fun idx_in_bounds := ⋯;
  c'.clause.get i = arr[arr.size + ↑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]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
i : Fin c'.clause.length
⊢ let_fun idx_in_bounds := ⋯;
  c'.clause.get i = arr[arr.size + ↑i]
Tactic:
simp only [← heq, empty, List.length_nil] at i
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]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
i✝ : Fin c'.clause.length
i : Fin 0
⊢ let_fun idx_in_bounds := ⋯;
  c'.clause.get i✝ = arr[arr.size + ↑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]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
i✝ : Fin c'.clause.length
i : Fin 0
⊢ let_fun idx_in_bounds := ⋯;
  c'.clause.get i✝ = arr[arr.size + ↑i✝]
Tactic:
exact Fin.elim0 i
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]
c' : DefaultClause n
heq : empty = c'
⊢ c'.clause.length = arr.size - arr.size
Tactic:
simp [← heq, empty]
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
acc : Option (DefaultClause n)
ih : motive (↑idx + 1) acc
⊢ motive (↑idx) (fold_fn arr[idx] acc)
Tactic:
rcases ih with ⟨idx_add_one_le_arr_size, 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
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]
⊢ motive (↑idx) (fold_fn arr[idx] acc)
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]
⊢ motive (↑idx) (fold_fn arr[idx] acc)
Tactic:
apply Exists.intro $ Nat.le_of_succ_le idx_add_one_le_arr_size
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),
    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]
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),
    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:
intro c' 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 : 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]