Theorem: List.splitOnListAux_progress (One.lean)

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]
State after:
no goals

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]
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₂

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]
State after:
no goals

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
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₂

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
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₂

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
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₂

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]
State after:
no goals

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]
State after:
no goals

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
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₂

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
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₂

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]
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₂

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]
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₂

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
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₂

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]
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

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]
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

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]
State after:
no goals

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

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₁
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

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

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₂)
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

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₂
h₃ : take (length delim) (hd :: tl ++ delim ++ rest) = take (length delim) (delim ++ rest₂)
⊢ delim <+: hd :: tl ++ dropLast delim
Tactic:
rw [List.take_append_of_le_length] at h₃
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) = take (length delim) (delim ++ rest₂)
⊢ delim <+: hd :: tl ++ dropLast delim

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)

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₂
h₃ : take (length delim) (hd :: tl ++ delim) = take (length delim) (delim ++ rest₂)
⊢ delim <+: hd :: tl ++ dropLast delim

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
simp at h₃
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)) = delim
⊢ delim <+: hd :: tl ++ dropLast delim

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ delim <+: hd :: tl ++ dropLast delim

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
conv => left; rw [← h₃]
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)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+: hd :: tl ++ dropLast delim

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+: hd :: tl ++ dropLast delim

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
simp only [length_take, length_cons, length_append, min_le_iff, ge_iff_le, cons_append]
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)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+: hd :: (tl ++ dropLast delim)

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+: hd :: (tl ++ dropLast delim)

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
apply List.isPrefix_take.1
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)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+:
    take (length (take (length delim) (hd :: (tl ++ delim)))) (hd :: (tl ++ dropLast delim))

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+:
    take (length (take (length delim) (hd :: (tl ++ delim)))) (hd :: (tl ++ dropLast delim))

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
simp only [length_take, length_cons, length_append, min_le_iff, ge_iff_le]
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)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+:
    take (min (length delim) (Nat.succ (length tl + length delim))) (hd :: (tl ++ dropLast delim))

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+:
    take (min (length delim) (Nat.succ (length tl + length delim))) (hd :: (tl ++ dropLast delim))

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
rw [min_eq_left]
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)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+: take (length delim) (hd :: (tl ++ dropLast delim))

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)) = delim
⊢ length delim ≤ Nat.succ (length tl + length delim)

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+: take (length delim) (hd :: (tl ++ dropLast delim))

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)) = delim
⊢ length delim ≤ Nat.succ (length tl + length delim)

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
. 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]
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)) = delim
⊢ length delim ≤ Nat.succ (length tl + length delim)

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ length delim ≤ Nat.succ (length tl + length delim)

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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
. 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]
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₂)
⊢ length delim ≤ length (hd :: tl ++ delim)

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₂
h₃ : take (length delim) (hd :: tl ++ delim ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
. 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]
State after:
no goals

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) = take (length delim) (hd :: (tl ++ dropLast delim))
Tactic:
rw [← List.cons_append, ← List.cons_append,
List.take_append_eq_append_take, List.take_append_eq_append_take]
State after:
α : 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)) = delim
⊢ take (length delim) (hd :: tl) ++ take (length delim - length (hd :: tl)) delim =
    take (length delim) (hd :: tl) ++ take (length delim - length (hd :: tl)) (dropLast delim)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ take (length delim) (hd :: tl) ++ take (length delim - length (hd :: tl)) delim =
    take (length delim) (hd :: tl) ++ take (length delim - length (hd :: tl)) (dropLast delim)
Tactic:
rw [List.dropLast_eq_take, List.take_take, min_eq_left]
State after:
α : 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)) = delim
⊢ length delim - length (hd :: tl) ≤ Nat.pred (length delim)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ length delim - length (hd :: tl) ≤ Nat.pred (length delim)
Tactic:
simp only [length_cons, tsub_le_iff_right, ge_iff_le]
State after:
α : 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)) = delim
⊢ length delim ≤ Nat.pred (length delim) + Nat.succ (length tl)

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ length delim ≤ Nat.pred (length delim) + Nat.succ (length tl)
Tactic:
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]
State after:
no goals

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ length delim ≤ Nat.pred (length delim) + 1
Tactic:
simp only [Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, le_refl, Nat.le_add_of_sub_le]
State after:
no goals

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₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ Nat.pred (length delim) + 1 ≤ Nat.pred (length delim) + Nat.succ (length tl)
Tactic:
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]
State after:
no goals