internlm/Lean-Github huggingface dataset:
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
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₂
Tactic:
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:
α : 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:
simp only [cons_append, append_assoc] at heq
Proof state after:
no goals
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
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₂
Tactic:
split
Proof state after:
case 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
head : α
tail : List α
heq : head✝ :: tail✝ ++ delim ++ rest = head :: tail
heq✝ : getRest (head✝ :: tail✝ ++ delim ++ rest) delim = none
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h₂ =
    #[toArray (head✝ :: tail✝)] ++ splitOnListAux delim rest #[] #[] h₂

case 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
rest✝ : List α
heq✝ : getRest (head✝ :: tail✝ ++ delim ++ rest) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head✝ :: tail✝ ++ delim ++ rest));
    splitOnListAux delim rest✝ #[] (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
head : α
tail : List α
heq : head✝ :: tail✝ ++ delim ++ rest = head :: tail
heq₂ : getRest (head✝ :: tail✝ ++ delim ++ rest) delim = none
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h₂ =
    #[toArray (head✝ :: tail✝)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
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]
Proof state after:
no goals
Theorem: List.splitOnListAux_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
⊢ (let_fun x := (_ : sizeOf rest₂ < sizeOf (hd :: tl ++ delim ++ rest));
    splitOnListAux delim rest₂ #[] (Array.push #[] #[]) h₂) =
    #[toArray (hd :: tl)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
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:
α : 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
heq₂ : getRest (head✝ :: tail✝ ++ delim ++ rest) delim = none
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h₂ =
    #[toArray (head✝ :: tail✝)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
injection heq
Proof state after:
α : 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₂ : getRest (head✝ :: tail✝ ++ delim ++ rest) delim = none
head_eq✝ : head✝ = head
tail_eq✝ : List.append (List.append tail✝ delim) rest = tail
⊢ splitOnListAux delim tail (Array.push #[] head) #[] 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
head : α
tail : List α
heq₂ : getRest (head✝ :: tail✝ ++ delim ++ rest) delim = none
head_eq✝ : head✝ = head
tail_eq✝ : List.append (List.append tail✝ delim) rest = tail
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h₂ =
    #[toArray (head✝ :: tail✝)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
subst_vars
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
⊢ splitOnListAux delim (List.append (List.append tail delim) rest) (Array.push #[] head) #[] 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 ≠ []
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
⊢ splitOnListAux delim (List.append (List.append tail delim) rest) (Array.push #[] head) #[] h₂ =
    #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
conv => left; rw [List.splitOnListAux_acc]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
⊢ Array.modifyHead (Array.append (Array.push #[] head))
      (splitOnListAux delim (List.append (List.append tail delim) rest) #[] #[] 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 ≠ []
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
⊢ Array.modifyHead (Array.append (Array.push #[] head))
      (splitOnListAux delim (List.append (List.append tail delim) rest) #[] #[] h₂) =
    #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
simp only [List.append_eq, append_assoc]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
⊢ Array.modifyHead (Array.append (Array.push #[] head)) (splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] 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 ≠ []
tail : List α
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ delim ++ rest) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
⊢ Array.modifyHead (Array.append (Array.push #[] head)) (splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] h₂) =
    #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
simp only [append_assoc] at ih
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
tail : List α
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
⊢ Array.modifyHead (Array.append (Array.push #[] head)) (splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] 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 ≠ []
tail : List α
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
⊢ Array.modifyHead (Array.append (Array.push #[] head)) (splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] h₂) =
    #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
rw [ih]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
tail : List α
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
⊢ Array.modifyHead (Array.append (Array.push #[] head)) (#[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂) =
    #[toArray (head :: tail)] ++ splitOnListAux delim rest #[] #[] h₂

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

α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
tail : List α
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
⊢ ¬delim <:+: tail ++ dropLast delim
Tactic:
. 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]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
tail : List α
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
⊢ ¬delim <:+: tail ++ dropLast delim
Theorem: List.splitOnListAux_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
tail : List α
head : α
h₁ : ¬delim <:+: head :: tail ++ dropLast delim
heq₂ : getRest (head :: tail ++ delim ++ rest) delim = none
ih :
  ¬delim <:+: tail ++ dropLast delim →
    splitOnListAux delim (tail ++ (delim ++ rest)) #[] #[] h₂ = #[toArray tail] ++ splitOnListAux delim rest #[] #[] h₂
⊢ ¬delim <:+: tail ++ dropLast delim
Tactic:
. intro h
  apply h₁
  simp only [cons_append, h, isInfix_cons]
Proof state after:
no goals
Theorem: List.splitOnListAux_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
⊢ (let_fun x := (_ : sizeOf rest₂ < sizeOf (hd :: tl ++ delim ++ rest));
    splitOnListAux delim rest₂ #[] (Array.push #[] #[]) h₂) =
    #[toArray (hd :: tl)] ++ splitOnListAux delim rest #[] #[] h₂
Tactic:
exfalso
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
⊢ False
Theorem: List.splitOnListAux_progress
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
⊢ False
Tactic:
apply h₁
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
⊢ delim <:+: hd :: tl ++ dropLast delim
Theorem: List.splitOnListAux_progress
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
⊢ delim <:+: hd :: tl ++ dropLast delim
Tactic:
apply List.isInfix_of_isPrefix
Proof state after:
case h.h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
⊢ delim <+: hd :: tl ++ dropLast delim
Theorem: List.splitOnListAux_progress
Proof state before:
case h.h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
⊢ delim <+: hd :: tl ++ dropLast delim
Tactic:
have h₃ := congr_arg (List.take (List.length delim)) (List.eq_append_of_getRest heq₂)
Proof state after:
case h.h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
h₃ : take (length delim) (hd :: tl ++ delim ++ rest) = take (length delim) (delim ++ rest₂)
⊢ delim <+: hd :: tl ++ dropLast delim