internlm/Lean-Github huggingface dataset:
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
⊢ Array.push r acc = r ++ #[acc] ++ #[]
Tactic:
simp only [Array.ext_iff, Array.push_data, Array.append_data, Array.data_toArray, append_nil]
Proof state after:
no goals
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
h : delim ≠ []
⊢ splitOnListAux delim l #[] #[] h = #[toArray l]
Tactic:
unfold splitOnListAux
Proof state after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
h : delim ≠ []
⊢ (match _h₀ : l with
    | [] => Array.push #[] #[]
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push #[] head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray l]
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
h : delim ≠ []
⊢ (match _h₀ : l with
    | [] => Array.push #[] #[]
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push #[] head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray l]
Tactic:
split
Proof state after:
case h_1
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
h₁ : ¬delim <:+: []
⊢ Array.push #[] #[] = #[#[]]

case h_2
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head✝ : α
tail✝ : List α
h₁ : ¬delim <:+: head✝ :: tail✝
⊢ (match h : getRest (head✝ :: tail✝) delim with
    | none => splitOnListAux delim tail✝ (Array.push #[] head✝) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head✝ :: tail✝));
      splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray (head✝ :: tail✝)]
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
h₁ : ¬delim <:+: []
⊢ Array.push #[] #[] = #[#[]]
Tactic:
case h_1 =>
  simp only [Array.ext_iff, Array.push_data, Array.data_toArray, nil_append]
Proof state after:
no goals
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push #[] head) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
      splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail)]
Tactic:
case h_2 head tail =>
  split
  case h_1 heq =>
    rw [List.splitOnListAux_acc, List.splitOnListAux_nonmatching tail]
    . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.data_toArray, Array.append_eq_append,
        cons.injEq, Array.append_data, Array.push_data, nil_append, singleton_append, and_self]
    . intro contr
      apply h₁
      exact List.isInfix_cons contr
  case h_2 head tail heq =>
    simp only [List.eq_append_of_getRest heq, isInfix_append_left, not_true] at h₁
Proof state after:
no goals
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
h₁ : ¬delim <:+: []
⊢ Array.push #[] #[] = #[#[]]
Tactic:
simp only [Array.ext_iff, Array.push_data, Array.data_toArray, nil_append]
Proof state after:
no goals
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push #[] head) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
      splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail)]
Tactic:
split
Proof state after:
case h_1
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq✝ : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h = #[toArray (head :: tail)]

case h_2
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
rest✝ : List α
heq✝ : getRest (head :: tail) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail)]
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h = #[toArray (head :: tail)]
Tactic:
case h_1 heq =>
  rw [List.splitOnListAux_acc, List.splitOnListAux_nonmatching tail]
  . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.data_toArray, Array.append_eq_append,
      cons.injEq, Array.append_data, Array.push_data, nil_append, singleton_append, and_self]
  . intro contr
    apply h₁
    exact List.isInfix_cons contr
Proof state after:
no goals
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
head✝ : DecidableEq α
h : delim ≠ []
head : α
tail✝ : List α
h₁ : ¬delim <:+: head :: tail✝
tail : List α
heq : getRest (head :: tail✝) delim = some tail
⊢ (let_fun x := (_ : sizeOf tail < sizeOf (head :: tail✝));
    splitOnListAux delim tail #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail✝)]
Tactic:
case h_2 head tail heq =>
  simp only [List.eq_append_of_getRest heq, isInfix_append_left, not_true] at h₁
Proof state after:
no goals
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h = #[toArray (head :: tail)]
Tactic:
rw [List.splitOnListAux_acc, List.splitOnListAux_nonmatching tail]
Proof state after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ Array.modifyHead (Array.append (Array.push #[] head)) #[toArray tail] = #[toArray (head :: tail)]

case h₁
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ ¬delim <:+: tail
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ Array.modifyHead (Array.append (Array.push #[] head)) #[toArray tail] = #[toArray (head :: tail)]

case h₁
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ ¬delim <:+: tail
Tactic:
. simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.data_toArray, Array.append_eq_append,
    cons.injEq, Array.append_data, Array.push_data, nil_append, singleton_append, and_self]
Proof state after:
case h₁
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ ¬delim <:+: tail
Theorem: List.splitOnListAux_nonmatching
Proof state before:
case h₁
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ ¬delim <:+: tail
Tactic:
. intro contr
  apply h₁
  exact List.isInfix_cons contr
Proof state after:
no goals
Theorem: List.splitOnListAux_nonmatching
Proof state before:
α : Type u_1
delim : List α
head✝ : DecidableEq α
h : delim ≠ []
head : α
tail✝ : List α
h₁ : ¬delim <:+: head :: tail✝
tail : List α
heq : getRest (head :: tail✝) delim = some tail
⊢ (let_fun x := (_ : sizeOf tail < sizeOf (head :: tail✝));
    splitOnListAux delim tail #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail✝)]
Tactic:
simp only [List.eq_append_of_getRest heq, isInfix_append_left, not_true] at h₁
Proof state after:
no goals
Theorem: List.splitOnList_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
⊢ splitOnList delim l = [l]
Tactic:
unfold List.splitOnList
Proof state after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
⊢ (match delim with
    | [] => [l]
    | head :: tail =>
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l #[] #[] (_ : ¬head :: tail = [])))) =
    [l]
Theorem: List.splitOnList_nonmatching
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
⊢ (match delim with
    | [] => [l]
    | head :: tail =>
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l #[] #[] (_ : ¬head :: tail = [])))) =
    [l]
Tactic:
cases delim with
| nil => simp only
| cons => 
  simp only
  rw [List.splitOnListAux_nonmatching]
  . simp only [Array.toList_eq, Array.map_data, map, Array.data_toArray]
  . exact h₁
Proof state after:
no goals
Theorem: List.splitOnList_nonmatching
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l : List α
h₁ : ¬[] <:+: l
⊢ (match [] with
    | [] => [l]
    | head :: tail =>
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l #[] #[] (_ : ¬head :: tail = [])))) =
    [l]
Tactic:
simp only
Proof state after:
no goals
Theorem: List.splitOnList_nonmatching
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ (match head✝ :: tail✝ with
    | [] => [l]
    | head :: tail =>
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l #[] #[] (_ : ¬head :: tail = [])))) =
    [l]
Tactic:
simp only
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ Array.toList (Array.map Array.toList (splitOnListAux (head✝ :: tail✝) l #[] #[] (_ : ¬head✝ :: tail✝ = []))) = [l]
Theorem: List.splitOnList_nonmatching
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ Array.toList (Array.map Array.toList (splitOnListAux (head✝ :: tail✝) l #[] #[] (_ : ¬head✝ :: tail✝ = []))) = [l]
Tactic:
rw [List.splitOnListAux_nonmatching]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ Array.toList (Array.map Array.toList #[toArray l]) = [l]

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ ¬head✝ :: tail✝ <:+: l
Theorem: List.splitOnList_nonmatching
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ Array.toList (Array.map Array.toList #[toArray l]) = [l]

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ ¬head✝ :: tail✝ <:+: l
Tactic:
. simp only [Array.toList_eq, Array.map_data, map, Array.data_toArray]
Proof state after:
case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ ¬head✝ :: tail✝ <:+: l
Theorem: List.splitOnList_nonmatching
Proof state before:
case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ ¬head✝ :: tail✝ <:+: l
Tactic:
. exact h₁
Proof state after:
no goals
Theorem: List.isPrefix_take
Proof state before:
α : Type u_1
delim l : List α
⊢ delim <+: take (length delim) l ↔ delim <+: l
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
delim l : List α
⊢ delim <+: take (length delim) l → delim <+: l

case mpr
α : Type u_1
delim l : List α
⊢ delim <+: l → delim <+: take (length delim) l
Theorem: List.isPrefix_take
Proof state before:
case mp
α : Type u_1
delim l : List α
⊢ delim <+: take (length delim) l → delim <+: l

case mpr
α : Type u_1
delim l : List α
⊢ delim <+: l → delim <+: take (length delim) l
Tactic:
. intro ⟨t, heq⟩
  replace heq := congr_arg (take (length delim)) heq
  simp only [take_left, take_take, min_self] at heq
  rw [heq]
  simp only [take_isPrefix]
Proof state after:
case mpr
α : Type u_1
delim l : List α
⊢ delim <+: l → delim <+: take (length delim) l
Theorem: List.isPrefix_take
Proof state before:
case mpr
α : Type u_1
delim l : List α
⊢ delim <+: l → delim <+: take (length delim) l
Tactic:
. intro ⟨t, heq⟩
  subst l
  simp only [take_left, isPrefix_self]
Proof state after:
no goals
Theorem: List.dropLast_take'
Proof state before:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
cases h: decide (n < length l) with
| true => 
  simp only [decide_eq_true_eq] at h
  simp only [List.dropLast_take h, Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, min_eq_left (le_of_lt h)]
| false =>
  simp only [decide_eq_false_iff_not, not_lt] at h
  rw [List.take_length_le h]
  simp only [dropLast_eq_take, Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, min_le_iff, h, min_eq_right]
Proof state after:
no goals
Theorem: List.dropLast_take'
Proof state before:
case true
n : ℕ
α✝ : Type u_1
l : List α✝
h : decide (n < length l) = true
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
simp only [decide_eq_true_eq] at h
Proof state after:
case true
n : ℕ
α✝ : Type u_1
l : List α✝
h : n < length l
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Theorem: List.dropLast_take'
Proof state before:
case true
n : ℕ
α✝ : Type u_1
l : List α✝
h : n < length l
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
simp only [List.dropLast_take h, Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, min_eq_left (le_of_lt h)]
Proof state after:
no goals
Theorem: List.dropLast_take'
Proof state before:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : decide (n < length l) = false
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
simp only [decide_eq_false_iff_not, not_lt] at h
Proof state after:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : length l ≤ n
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Theorem: List.dropLast_take'
Proof state before:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : length l ≤ n
⊢ dropLast (take n l) = take (min n (length l) - 1) l
Tactic:
rw [List.take_length_le h]
Proof state after:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : length l ≤ n
⊢ dropLast l = take (min n (length l) - 1) l
Theorem: List.dropLast_take'
Proof state before:
case false
n : ℕ
α✝ : Type u_1
l : List α✝
h : length l ≤ n
⊢ dropLast l = take (min n (length l) - 1) l
Tactic:
simp only [dropLast_eq_take, Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, min_le_iff, h, min_eq_right]
Proof state after:
no goals
Theorem: List.isPrefix_of_append_isPrefix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
⊢ l₂ <+: l₃
Tactic:
have ⟨t, heq⟩ := h
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
t : List α✝
heq : l₁ ++ l₂ ++ t = l₁ ++ l₃
⊢ l₂ <+: l₃
Theorem: List.isPrefix_of_append_isPrefix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
t : List α✝
heq : l₁ ++ l₂ ++ t = l₁ ++ l₃
⊢ l₂ <+: l₃
Tactic:
simp only [append_assoc, append_cancel_left_eq] at heq
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
t : List α✝
heq : l₂ ++ t = l₃
⊢ l₂ <+: l₃
Theorem: List.isPrefix_of_append_isPrefix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ ++ l₂ <+: l₁ ++ l₃
t : List α✝
heq : l₂ ++ t = l₃
⊢ l₂ <+: l₃
Tactic:
exact ⟨t, heq⟩
Proof state after:
no goals
Theorem: List.splitOnListAux_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim front rest : List α
h₁ : ¬delim <:+: front ++ dropLast delim
h₂ : delim ≠ []
⊢ splitOnListAux delim (front ++ delim ++ rest) #[] #[] h₂ = #[toArray front] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
induction front with
| nil =>
  rw [nil_append, splitOnListAux_delim]
  simp only [Array.ext_iff, Array.append_data, Array.data_toArray, nil_append, singleton_append]
| cons head tail ih =>
  conv => left; unfold splitOnListAux
  split
  case h_1 heq =>
    simp only [cons_append, append_assoc] at heq
  case h_2 head tail heq =>
    split
    case h_1 heq₂ =>
      injection heq; subst_vars
      conv => left; rw [List.splitOnListAux_acc]
      simp only [List.append_eq, append_assoc]
      simp only [append_assoc] at ih
      rw [ih]
      . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.append_data, Array.data_toArray,
          singleton_append, Array.append_eq_append, cons.injEq, Array.push_data, nil_append, and_self]
      . intro h
        apply h₁
        simp only [cons_append, h, isInfix_cons]
    case h_2 hd tl rest₂ heq₂ =>
      exfalso; apply h₁
      apply List.isInfix_of_isPrefix
      have h₃ := congr_arg (List.take (List.length delim)) (List.eq_append_of_getRest heq₂)
      rw [List.take_append_of_le_length] at h₃
      simp at h₃
      conv => left; rw [← h₃]
      simp only [length_take, length_cons, length_append, min_le_iff, ge_iff_le, cons_append]
      apply List.isPrefix_take.1
      simp only [length_take, length_cons, length_append, min_le_iff, ge_iff_le]
      rw [min_eq_left]
      . have h₄: take (length delim) (hd :: (tl ++ delim)) = take (length delim) (hd :: (tl ++ delim.dropLast)) := by
          rw [← List.cons_append, ← List.cons_append,
          List.take_append_eq_append_take, List.take_append_eq_append_take]
          rw [List.dropLast_eq_take, List.take_take, min_eq_left]
          simp only [length_cons, tsub_le_iff_right, ge_iff_le]
          calc
            length delim ≤  Nat.pred (length delim) + 1 := by simp only [Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, le_refl, Nat.le_add_of_sub_le]
            _ ≤  Nat.pred (length delim) + Nat.succ (length tl) := by simp only [Nat.succ_eq_add_one, add_le_add_iff_left, le_add_iff_nonneg_left, zero_le, ge_iff_le,
              nonpos_iff_eq_zero]
        rw [h₄]
        simp only [isPrefix_self]
      . simp only [Nat.succ_eq_add_one, Nat.le_add_one_iff, le_add_iff_nonneg_left, zero_le, ge_iff_le,
          nonpos_iff_eq_zero, true_or]
      . simp only [cons_append, length_cons, length_append, le_add_iff_nonneg_left, zero_le, ge_iff_le,
          nonpos_iff_eq_zero, Nat.le_succ_of_le]
Proof state after:
no goals
Theorem: List.splitOnListAux_progress
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
h₁ : ¬delim <:+: [] ++ dropLast delim
⊢ splitOnListAux delim ([] ++ delim ++ rest) #[] #[] h₂ = #[#[]] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
rw [nil_append, splitOnListAux_delim]
Proof state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
h₁ : ¬delim <:+: [] ++ dropLast delim
⊢ #[] ++ #[#[]] ++ splitOnListAux delim rest #[] #[] h₂ = #[#[]] ++ splitOnListAux delim rest #[] #[] h₂
Theorem: List.splitOnListAux_progress
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
h₁ : ¬delim <:+: [] ++ dropLast delim
⊢ #[] ++ #[#[]] ++ splitOnListAux delim rest #[] #[] h₂ = #[#[]] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
simp only [Array.ext_iff, Array.append_data, Array.data_toArray, nil_append, singleton_append]
Proof state after:
no goals
Theorem: List.splitOnListAux_progress
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
head : α
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
⊢ splitOnListAux delim (head :: tail ++ delim ++ rest) #[] #[] h₂ =
    #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
conv => left; unfold splitOnListAux
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
head : α
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
⊢ (match _h₀ : head :: tail ++ delim ++ rest with
    | [] => Array.push #[] #[]
    | head_1 :: tail_1 =>
      match h : getRest (head :: tail ++ delim ++ rest) delim with
      | none => splitOnListAux delim tail_1 (Array.push #[] head_1) #[] h₂
      | some rest_1 =>
        let_fun x := (_ : sizeOf rest_1 < sizeOf (head :: tail ++ delim ++ rest));
        splitOnListAux delim rest_1 #[] (Array.push #[] #[]) h₂) =
    #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂
Theorem: List.splitOnListAux_progress
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
head : α
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
⊢ (match _h₀ : head :: tail ++ delim ++ rest with
    | [] => Array.push #[] #[]
    | head_1 :: tail_1 =>
      match h : getRest (head :: tail ++ delim ++ rest) delim with
      | none => splitOnListAux delim tail_1 (Array.push #[] head_1) #[] h₂
      | some rest_1 =>
        let_fun x := (_ : sizeOf rest_1 < sizeOf (head :: tail ++ delim ++ rest));
        splitOnListAux delim rest_1 #[] (Array.push #[] #[]) h₂) =
    #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
split
Proof state after:
case cons.h_1
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
head : α
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq✝ : head :: tail ++ delim ++ rest = []
⊢ Array.push #[] #[] = #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂

case cons.h_2
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
head : α
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
head✝ : α
tail✝ : List α
heq✝ : head :: tail ++ delim ++ rest = head✝ :: tail✝
⊢ (match h : getRest (head :: tail ++ delim ++ rest) delim with
    | none => splitOnListAux delim tail✝ (Array.push #[] head✝) #[] h₂
    | some rest_1 =>
      let_fun x := (_ : sizeOf rest_1 < sizeOf (head :: tail ++ delim ++ rest));
      splitOnListAux delim rest_1 #[] (Array.push #[] #[]) h₂) =
    #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂
Theorem: List.splitOnListAux_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
head : α
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq : head :: tail ++ delim ++ rest = []
⊢ Array.push #[] #[] = #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
case h_1 heq =>
  simp only [cons_append, append_assoc] at heq
Proof state after:
no goals