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 :
  (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]
Tactic:
split at heq
Proof state after:
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]

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]