-- 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:
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 =
    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
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 : List.length acc.clause = arr.size - (↑idx + 1)
ih : ∀ (i : Fin (List.length acc.clause)), List.get acc.clause i = arr[↑idx + 1 + ↑i]
heq :
  (if h : List.contains acc.clause (arr[↑idx].fst, !arr[↑idx].snd) = true then none
    else
      if h : List.contains acc.clause arr[↑idx] = true then some acc
      else some { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ }) =
    some c'
⊢ ∃ hsize,
    ∀ (i : Fin (List.length c'.clause)),
      let_fun idx_in_bounds := ⋯;
      List.get c'.clause i = arr[↑idx + ↑i]

Tactic:
split at heq

Result:
case intro.isTrue
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
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 : List.length acc.clause = arr.size - (↑idx + 1)
ih : ∀ (i : Fin (List.length acc.clause)), List.get acc.clause i = arr[↑idx + 1 + ↑i]
h✝ : List.contains acc.clause (arr[↑idx].fst, !arr[↑idx].snd) = true
heq : none = some c'
⊢ ∃ hsize,
    ∀ (i : Fin (List.length c'.clause)),
      let_fun idx_in_bounds := ⋯;
      List.get c'.clause i = arr[↑idx + ↑i]

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 =
    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
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 : List.length acc.clause = arr.size - (↑idx + 1)
ih : ∀ (i : Fin (List.length acc.clause)), List.get acc.clause i = arr[↑idx + 1 + ↑i]
h✝ : ¬List.contains acc.clause (arr[↑idx].fst, !arr[↑idx].snd) = true
heq :
  (if h : List.contains acc.clause arr[↑idx] = true then some acc
    else some { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ }) =
    some c'
⊢ ∃ hsize,
    ∀ (i : Fin (List.length c'.clause)),
      let_fun idx_in_bounds := ⋯;
      List.get c'.clause i = arr[↑idx + ↑i]

Proof state:
case intro.isTrue
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
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 : List.length acc.clause = arr.size - (↑idx + 1)
ih : ∀ (i : Fin (List.length acc.clause)), List.get acc.clause i = arr[↑idx + 1 + ↑i]
h✝ : List.contains acc.clause (arr[↑idx].fst, !arr[↑idx].snd) = true
heq : none = some c'
⊢ ∃ hsize,
    ∀ (i : Fin (List.length c'.clause)),
      let_fun idx_in_bounds := ⋯;
      List.get c'.clause i = arr[↑idx + ↑i]

Tactic:
simp at heq

Result:
no goals

Proof state:
case intro.isFalse.isTrue
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
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 : List.length acc.clause = arr.size - (↑idx + 1)
ih : ∀ (i : Fin (List.length acc.clause)), List.get acc.clause i = arr[↑idx + 1 + ↑i]
h✝¹ : ¬List.contains acc.clause (arr[↑idx].fst, !arr[↑idx].snd) = true
h✝ : List.contains acc.clause arr[↑idx] = true
heq : some acc = some c'
⊢ ∃ hsize,
    ∀ (i : Fin (List.length c'.clause)),
      let_fun idx_in_bounds := ⋯;
      List.get c'.clause i = arr[↑idx + ↑i]

Tactic:
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

Result:
no goals