-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
theorem ofArray_eq (arr : Array (Literal (PosFin n)))
    (arrNodup : ∀ i : Fin arr.size, ∀ j : Fin arr.size, i.1 ≠ j.1 → arr[i] ≠ arr[j])
    (c : DefaultClause n) :
    ofArray arr = some c → toList c = Array.toList arr

Proof state:
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 =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin (List.length c'.clause)),
              let_fun idx_in_bounds := ⋯;
              List.get c'.clause i = arr[idx + ↑i]
c' : DefaultClause n
heq : empty = c'
hsize : List.length c'.clause = arr.size - arr.size
i : Fin (List.length c'.clause)
⊢ let_fun idx_in_bounds := ⋯;
  List.get c'.clause i = arr[arr.size + ↑i]

Tactic:
simp only [← heq, empty, List.length_nil] at i

Result:
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 =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin (List.length c'.clause)),
              let_fun idx_in_bounds := ⋯;
              List.get c'.clause i = arr[idx + ↑i]
c' : DefaultClause n
heq : empty = c'
hsize : List.length c'.clause = arr.size - arr.size
i✝ : Fin (List.length c'.clause)
i : Fin 0
⊢ let_fun idx_in_bounds := ⋯;
  List.get c'.clause i✝ = arr[arr.size + ↑i✝]

Proof state:
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 =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin (List.length c'.clause)),
              let_fun idx_in_bounds := ⋯;
              List.get c'.clause i = arr[idx + ↑i]
⊢ motive arr.size (some empty)

Tactic:
apply Exists.intro <| Nat.le_refl arr.size

Result:
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 =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin (List.length c'.clause)),
              let_fun idx_in_bounds := ⋯;
              List.get c'.clause i = arr[idx + ↑i]
⊢ ∀ (c' : DefaultClause n),
    some empty = some c' →
      ∃ hsize,
        ∀ (i : Fin (List.length c'.clause)),
          let_fun idx_in_bounds := ⋯;
          List.get c'.clause i = arr[arr.size + ↑i]

Proof state:
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 =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin (List.length c'.clause)),
              let_fun idx_in_bounds := ⋯;
              List.get c'.clause 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 : List.length c.clause = arr.size - 0
h :
  ∀ (i : Fin (List.length c.clause)),
    let_fun idx_in_bounds := ⋯;
    List.get c.clause i = arr[0 + ↑i]
i : Nat
l : Literal (PosFin n)
⊢ l ∈ c.clause[i]? ↔ l ∈ arr.toList[i]?

Tactic:
by_cases i_in_bounds : i < c.clause.length

Result:
case pos
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 =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin (List.length c'.clause)),
              let_fun idx_in_bounds := ⋯;
              List.get c'.clause 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 : List.length c.clause = arr.size - 0
h :
  ∀ (i : Fin (List.length c.clause)),
    let_fun idx_in_bounds := ⋯;
    List.get c.clause i = arr[0 + ↑i]
i : Nat
l : Literal (PosFin n)
i_in_bounds : i < List.length c.clause
⊢ l ∈ c.clause[i]? ↔ l ∈ arr.toList[i]?

case neg
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 =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin (List.length c'.clause)),
              let_fun idx_in_bounds := ⋯;
              List.get c'.clause 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 : List.length c.clause = arr.size - 0
h :
  ∀ (i : Fin (List.length c.clause)),
    let_fun idx_in_bounds := ⋯;
    List.get c.clause i = arr[0 + ↑i]
i : Nat
l : Literal (PosFin n)
i_in_bounds : ¬i < List.length c.clause
⊢ l ∈ c.clause[i]? ↔ l ∈ arr.toList[i]?